The Isoperimetric Inequality

This file formalises basic properties of classical Fourier series needed on the way to the isoperimetric inequality. In particular we prove:

• Parseval's theorem – Parsevals_thm
• Wirtinger's inequality – Wirtingers_inequality

Main results

Parseval's theorem (Parsevals_thm)

Given a Fourier series f(x) = a₀/2 + ∑_{n≥1} (aₙ cos(nx) + bₙ sin(nx)), under suitable integrability and summability hypotheses,

(1/π) ∫_{-π}^{π} f(x)² dx = (1/2) a₀² + ∑_{n≥1} (aₙ² + bₙ²).

Wirtinger's inequality (Wirtingers_inequality)

Given the same Fourier series, the Parseval identity applied to the derivative series yields

(1/π) ∫_{-π}^{π} (f'(x))² dx = ∑_{n≥1} n² (aₙ² + bₙ²).

This is the continuous analogue of the discrete Wirtinger inequality, and reflects that differentiation weights each Fourier mode by its frequency n.

Notation

Throughout, a : ℕ → ℝ and b : ℕ → ℝ are the cosine and sine Fourier coefficients, and the series is indexed over ℕ+ (positive natural numbers).

def fourierSeries (a b : ℕ → ℝ) (x : ℝ) : ℝ

The classical Fourier series as a function of x: f(x) = a₀/2 + ∑_{n=1}^∞ (aₙ cos(nx) + bₙ sin(nx)).

Equations

• fourierSeries a b x = 1 / 2 * a 0 + ∑' (n : ℕ+), (a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x))

def fourierPartialSum (a b : ℕ → ℝ) (x : ℝ) (N : ℕ) : ℝ

The N-th partial sum of the Fourier series: S_N(x) = a₀/2 + ∑_{n=1}^N (aₙ cos(nx) + bₙ sin(nx)).

Equations

• fourierPartialSum a b x N = 1 / 2 * a 0 + ∑ n ∈ Finset.range N, (a (n + 1) * Real.cos ((↑n + 1) * x) + b (n + 1) * Real.sin ((↑n + 1) * x))

def fourierSum (a b : ℕ → ℝ) (x : ℝ) : ℝ

The oscillatory sum part of the Fourier series (without the constant term): S(x) = ∑_{n=1}^∞ (aₙ cos(nx) + bₙ sin(nx)).

Equations

• fourierSum a b x = ∑' (n : ℕ+), (a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x))

theorem fourierSeries_eq (a b : ℕ → ℝ) (x : ℝ) : fourierSeries a b x = 1 / 2 * a 0 + fourierSum a b x

The Fourier series decomposes as f(x) = a₀/2 + S(x), where S(x) is the oscillatory sum part.

theorem fourierSeries_sq (a b : ℕ → ℝ) (x : ℝ) : fourierSeries a b x ^ 2 = a 0 ^ 2 / 4 + a 0 * ∑' (n : ℕ+), (a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x)) + (∑' (n : ℕ+), (a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x))) ^ 2

Expansion of (f(x))² as (a₀/2)² + a₀·S(x) + S(x)², where S(x) = fourierSum a b x.

theorem expand_square (a b : ℕ → ℝ) (x : ℝ) (hc : Summable fun (n : ℕ+) => a ↑n * Real.cos (↑↑n * x)) (hs : Summable fun (n : ℕ+) => b ↑n * Real.sin (↑↑n * x)) : (∑' (n : ℕ+), (a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x))) ^ 2 = (∑' (n : ℕ+), a ↑n * Real.cos (↑↑n * x)) ^ 2 + (2 * ∑' (n : ℕ+), a ↑n * Real.cos (↑↑n * x)) * ∑' (n : ℕ+), b ↑n * Real.sin (↑↑n * x) + (∑' (n : ℕ+), b ↑n * Real.sin (↑↑n * x)) ^ 2

Expands (∑ aₙ cos(nx) + bₙ sin(nx))² into (∑ aₙ cos)² + 2·(∑ aₙ cos)(∑ bₙ sin) + (∑ bₙ sin)² using linearity of the infinite sum.

theorem expand_sin_sq (b : ℕ → ℝ) (x : ℝ) (hs : Summable fun (n : ℕ+) => b ↑n * Real.sin (↑↑n * x)) (hprod : Summable fun (z : ℕ+ × ℕ+) => b ↑z.1 * Real.sin (↑↑z.1 * x) * (b ↑z.2 * Real.sin (↑↑z.2 * x))) (hinner : ∀ (n : ℕ+), Summable fun (m : ℕ+) => b ↑n * Real.sin (↑↑n * x) * (b ↑m * Real.sin (↑↑m * x))) : (∑' (n : ℕ+), b ↑n * Real.sin (↑↑n * x)) ^ 2 = ∑' (n : ℕ+) (m : ℕ+), b ↑n * b ↑m * Real.sin (↑↑n * x) * Real.sin (↑↑m * x)

Expands the square of the sine partial sum into a double sum: (∑ bₙ sin(nx))² = ∑ₙ ∑ₘ bₙ bₘ sin(nx) sin(mx).

theorem expand_cos_sq (a : ℕ → ℝ) (x : ℝ) (hs1 : Summable fun (n : ℕ+) => a ↑n * Real.cos (↑↑n * x)) (hprod1 : Summable fun (z : ℕ+ × ℕ+) => a ↑z.1 * Real.cos (↑↑z.1 * x) * (a ↑z.2 * Real.cos (↑↑z.2 * x))) (hinner : ∀ (n : ℕ+), Summable fun (m : ℕ+) => a ↑n * Real.cos (↑↑n * x) * (a ↑m * Real.cos (↑↑m * x))) : (∑' (n : ℕ+), a ↑n * Real.cos (↑↑n * x)) ^ 2 = ∑' (n : ℕ+) (m : ℕ+), a ↑n * a ↑m * Real.cos (↑↑n * x) * Real.cos (↑↑m * x)

Expands the square of the cosine partial sum into a double sum: (∑ aₙ cos(nx))² = ∑ₙ ∑ₘ aₙ aₘ cos(nx) cos(mx).

theorem fourier_series_sq_expanded (a b : ℕ → ℝ) (x : ℝ) (hc : Summable fun (n : ℕ+) => a ↑n * Real.cos (↑↑n * x)) (hs : Summable fun (n : ℕ+) => b ↑n * Real.sin (↑↑n * x)) (hprod_cos : Summable fun (z : ℕ+ × ℕ+) => a ↑z.1 * Real.cos (↑↑z.1 * x) * (a ↑z.2 * Real.cos (↑↑z.2 * x))) (hinner_cos : ∀ (n : ℕ+), Summable fun (m : ℕ+) => a ↑n * Real.cos (↑↑n * x) * (a ↑m * Real.cos (↑↑m * x))) (hprod_sin : Summable fun (z : ℕ+ × ℕ+) => b ↑z.1 * Real.sin (↑↑z.1 * x) * (b ↑z.2 * Real.sin (↑↑z.2 * x))) (hinner_sin : ∀ (n : ℕ+), Summable fun (m : ℕ+) => b ↑n * Real.sin (↑↑n * x) * (b ↑m * Real.sin (↑↑m * x))) : fourierSeries a b x ^ 2 = a 0 ^ 2 / 4 + a 0 * ∑' (n : ℕ+), (a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x)) + (∑' (n : ℕ+) (m : ℕ+), a ↑n * a ↑m * Real.cos (↑↑n * x) * Real.cos (↑↑m * x) + (2 * ∑' (n : ℕ+), a ↑n * Real.cos (↑↑n * x)) * ∑' (n : ℕ+), b ↑n * Real.sin (↑↑n * x) + ∑' (n : ℕ+) (m : ℕ+), b ↑n * b ↑m * Real.sin (↑↑n * x) * Real.sin (↑↑m * x))

Full expansion of (f(x))² into a constant term, cross terms, and double sums, combining fourierSeries_sq, expand_square, expand_cos_sq, and expand_sin_sq.

theorem integration_of_const (a : ℕ → ℝ) : ∫ (_x : ℝ) in -Real.pi..Real.pi, 1 / 4 * a 0 ^ 2 = 1 / 2 * a 0 ^ 2 * Real.pi

∫_{-π}^{π} (1/4) a₀² dx = (1/2) a₀² π.

theorem integration_of_cos_sin (a b : ℕ → ℝ) (hF_int : ∀ (n : ℕ+), IntervalIntegrable (fun (x : ℝ) => a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x)) MeasureTheory.volume (-Real.pi) Real.pi) (hF_sum : Summable fun (n : ℕ+) => ∫ (x : ℝ) in -Real.pi..Real.pi, ‖a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x)‖) : ∫ (x : ℝ) in -Real.pi..Real.pi, a 0 * fourierSum a b x = 0

The cross term integrates to zero over [-π, π]: ∫_{-π}^{π} a₀ · (∑_{n≥1} aₙ cos(nx) + bₙ sin(nx)) dx = 0.

theorem integration_cos_cos_zero (n m : ℕ+) (h : n ≠ m) : ∫ (x : ℝ) in -Real.pi..Real.pi, Real.cos (↑↑n * x) * Real.cos (↑↑m * x) = 0

Orthogonality of cosines: ∫_{-π}^{π} cos(nx) cos(mx) dx = 0 for n ≠ m.

theorem integration_sin_sin_zero (n m : ℕ+) (h : n ≠ m) : ∫ (x : ℝ) in -Real.pi..Real.pi, Real.sin (↑↑n * x) * Real.sin (↑↑m * x) = 0

Orthogonality of sines: ∫_{-π}^{π} sin(nx) sin(mx) dx = 0 for n ≠ m.

theorem integration_sin_cos_zero (n m : ℕ+) (h : n ≠ m) : ∫ (x : ℝ) in -Real.pi..Real.pi, Real.cos (↑↑n * x) * Real.sin (↑↑m * x) = 0

Cross orthogonality: ∫_{-π}^{π} cos(nx) sin(mx) dx = 0 for n ≠ m.

theorem integration_cos_cos_pi (n m : ℕ+) (h : n = m) : ∫ (x : ℝ) in -Real.pi..Real.pi, Real.cos (↑↑n * x) * Real.cos (↑↑m * x) = Real.pi

Self-orthogonality of cosines: ∫_{-π}^{π} cos(nx) cos(mx) dx = π when n = m.

theorem integration_sin_sin_pi (n m : ℕ+) (h : n = m) : ∫ (x : ℝ) in -Real.pi..Real.pi, Real.sin (↑↑n * x) * Real.sin (↑↑m * x) = Real.pi

Self-orthogonality of sines: ∫_{-π}^{π} sin(nx) sin(mx) dx = π when n = m.

theorem Parsevals_thm (a b : ℕ → ℝ) (hfS_int : IntervalIntegrable (fun (x : ℝ) => a 0 * fourierSum a b x) MeasureTheory.volume (-Real.pi) Real.pi) (hfSq_int : IntervalIntegrable (fun (x : ℝ) => fourierSum a b x ^ 2) MeasureTheory.volume (-Real.pi) Real.pi) (hF_int : ∀ (n : ℕ+), IntervalIntegrable (fun (x : ℝ) => a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x)) MeasureTheory.volume (-Real.pi) Real.pi) (hF_sum : Summable fun (n : ℕ+) => ∫ (x : ℝ) in -Real.pi..Real.pi, ‖a ↑n * Real.cos (↑↑n * x) + b ↑n * Real.sin (↑↑n * x)‖) (h_int_sq : ∫ (x : ℝ) in -Real.pi..Real.pi, fourierSum a b x ^ 2 = Real.pi * ∑' (n : ℕ+), (a ↑n ^ 2 + b ↑n ^ 2)) : 1 / Real.pi * ∫ (x : ℝ) in -Real.pi..Real.pi, fourierSeries a b x ^ 2 = 1 / 2 * a 0 ^ 2 + ∑' (n : ℕ+), (a ↑n ^ 2 + b ↑n ^ 2)

Parseval's theorem: Given square-integrability and suitable summability hypotheses, (1/π) ∫_{-π}^{π} f(x)² dx = (1/2) a₀² + ∑_{n≥1} (aₙ² + bₙ²).

theorem term_bound (a b : ℕ → ℝ) (n : ℕ) (x : ℝ) : ‖a (n + 1) * Real.cos ((↑n + 1) * x) + b (n + 1) * Real.sin ((↑n + 1) * x)‖ ≤ ‖a (n + 1)‖ + ‖b (n + 1)‖

Each Fourier term is bounded in norm: ‖aₙ cos(nx) + bₙ sin(nx)‖ ≤ ‖aₙ‖ + ‖bₙ‖ for all x : ℝ.

theorem fourierSeries_uniformlyConvergence (a b : ℕ → ℝ) (hsumab : Summable fun (n : ℕ) => ‖a n‖ + ‖b n‖) : TendstoUniformly (fun (N : ℕ) (x : ℝ) => fourierPartialSum a b x N) (fourierSeries a b) Filter.atTop

Weierstrass M-test for Fourier series: If ∑ (‖aₙ‖ + ‖bₙ‖) converges, then the Fourier partial sums converge uniformly to fourierSeries a b on all of ℝ.

theorem fourierSeries_continuous (a b : ℕ → ℝ) (hsumab : Summable fun (n : ℕ) => ‖a n‖ + ‖b n‖) : Continuous (fourierSeries a b)

If ∑ (‖aₙ‖ + ‖bₙ‖) converges, then the Fourier series fourierSeries a b is continuous on all of ℝ.

theorem fourierSeries_integrable (a b : ℕ → ℝ) (hsumab : Summable fun (n : ℕ) => ‖a n‖ + ‖b n‖) : IntervalIntegrable (fourierSeries a b) MeasureTheory.volume (-Real.pi) Real.pi

The Fourier series f(x) = (1/2)a₀ + ∑ (aₙ cos nx + bₙ sin nx) is integrable on [-π, π] whenever ∑ (‖aₙ‖ + ‖bₙ‖) converges.

noncomputable def fourierDeriv (a b : ℕ → ℝ) (x : ℝ) : ℝ

The formal derivative series: d/dx [aₙ cos nx + bₙ sin nx] = -n aₙ sin nx + n bₙ cos nx.

Equations

• fourierDeriv a b x = ∑' (n : ℕ), (-↑n * a n * Real.sin (↑n * x) + ↑n * b n * Real.cos (↑n * x))

theorem fourierDeriv_summable (a b : ℕ → ℝ) (hab' : Summable fun (n : ℕ) => ↑n * (‖a n‖ + ‖b n‖)) (x : ℝ) : Summable fun (n : ℕ) => -↑n * a n * Real.sin (↑n * x) + ↑n * b n * Real.cos (↑n * x)

If ∑ n * (‖aₙ‖ + ‖bₙ‖) converges, then the derivative series is summable at each x.

theorem fourierDeriv_uniformConvergence (a b : ℕ → ℝ) (hab' : Summable fun (n : ℕ) => ↑n * (‖a n‖ + ‖b n‖)) : TendstoUniformly (fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, (-↑n * a n * Real.sin (↑n * x) + ↑n * b n * Real.cos (↑n * x))) (fourierDeriv a b) Filter.atTop

If ∑ n * (‖aₙ‖ + ‖bₙ‖) converges, the partial sums of the derivative series converge uniformly to fourierDeriv a b (Weierstrass M-test applied to the derivative).

theorem hasDerivAt_term (a b : ℕ → ℝ) (n : ℕ) (x : ℝ) : HasDerivAt (fun (x : ℝ) => a n * Real.cos (↑n * x) + b n * Real.sin (↑n * x)) (-↑n * a n * Real.sin (↑n * x) + ↑n * b n * Real.cos (↑n * x)) x

Each Fourier term is differentiable: d/dx [aₙ cos(nx) + bₙ sin(nx)] = -n aₙ sin(nx) + n bₙ cos(nx).

theorem hasDerivAt_partialSum (a b : ℕ → ℝ) (N : ℕ) (x : ℝ) : HasDerivAt (fun (x : ℝ) => fourierPartialSum a b x N) (∑ n ∈ Finset.range N, (-↑(n + 1) * a (n + 1) * Real.sin (↑(n + 1) * x) + ↑(n + 1) * b (n + 1) * Real.cos (↑(n + 1) * x))) x

The N-th partial sum is differentiable, with derivative equal to the partial sum of term-wise derivatives.

theorem fourierSeries_hasDerivAt (a b : ℕ → ℝ) (hab' : Summable fun (n : ℕ) => ↑n * (‖a n‖ + ‖b n‖)) (hab : Summable fun (n : ℕ) => ‖a n‖ + ‖b n‖) (x : ℝ) : HasDerivAt (fourierSeries a b) (fourierDeriv a b x) x

Term-by-term differentiation: HasDerivAt (fourierSeries a b) (fourierDeriv a b x) x whenever ∑ n * (‖aₙ‖ + ‖bₙ‖) and ∑ (‖aₙ‖ + ‖bₙ‖) both converge.

theorem fourierSeries_differentiable (a b : ℕ → ℝ) (hab' : Summable fun (n : ℕ) => ↑n * (‖a n‖ + ‖b n‖)) (hab : Summable fun (n : ℕ) => ‖a n‖ + ‖b n‖) : Differentiable ℝ (fourierSeries a b)

If ∑ n * (‖aₙ‖ + ‖bₙ‖) and ∑ (‖aₙ‖ + ‖bₙ‖) both converge, then the Fourier series fourierSeries a b is differentiable on all of ℝ, with derivative fourierDeriv a b.

theorem FourierSerise_derivative (a b : ℕ → ℝ) (hab' : Summable fun (n : ℕ) => ↑n * (‖a n‖ + ‖b n‖)) (hab : Summable fun (n : ℕ) => ‖a n‖ + ‖b n‖) (x : ℝ) : deriv (fourierSeries a b) x = ∑' (n : ℕ+), (-a ↑n * ↑↑n * Real.sin (↑↑n * x) + b ↑n * ↑↑n * Real.cos (↑↑n * x))

The derivative of the Fourier series equals the ℕ⁺-indexed derivative series.

theorem Wirtingers_inequality (a b : ℕ → ℝ) (h_int_sq : ∫ (x : ℝ) in -Real.pi..Real.pi, deriv (fourierSeries a b) x ^ 2 = Real.pi * ∑' (n : ℕ+), ↑↑n ^ 2 * (a ↑n ^ 2 + b ↑n ^ 2)) : 1 / Real.pi * ∫ (x : ℝ) in -Real.pi..Real.pi, deriv (fourierSeries a b) x ^ 2 = ∑' (n : ℕ+), ↑↑n ^ 2 * (a ↑n ^ 2 + b ↑n ^ 2)

Wirtinger's inequality: (1/pi) * int (f'(x))^2 = sum n^2 * (a n^2 + b n^2). The integral formula h_int_sq is the Parseval identity for the derivative series, mirroring the h_int_sq hypothesis in Parsevals_thm.