theorem fourierCharacter_formula_continuous_periodic (n : ℤ) : (Continuous fun (x : ℝ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x)) ∧ Function.Periodic (fun (x : ℝ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x)) 1

The exponential mode x ↦ exp(2π i n x) is continuous and 1-periodic on ℝ.

noncomputable def fourierCharacter (n : ℤ) : C(AddCircle 1, ℂ)

Definition 5.3.1 (Characters): for every integer n, define e_n ∈ C(ℝ/ℤ; ℂ) by e_n(x) = exp(2π i n x).

Equations

• fourierCharacter n = fourier n

theorem fourierCharacter_apply (n : ℤ) (x : ℝ) : (fourierCharacter n) ↑x = Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x)

Evaluation formula for the character e_n.

theorem fourierCharacter_orthonormal_system (n m : ℤ) : (inner ℂ (fourierLp 2 n) (fourierLp 2 m) = if n = m then 1 else 0) ∧ ‖fourierLp 2 n‖ = 1

Lemma 5.3.5 (Characters are an orthonormal system): for integers n, m, the Fourier characters satisfy ⟪e_n, e_m⟫ = 1 when n = m and 0 otherwise, and ‖e_n‖_2 = 1, where e_k is viewed in L² as fourierLp (T := 1) (p := 2) k.

def IsTrigonometricPolynomial (f : C(AddCircle 1, ℂ)) : Prop

Definition 5.3.2 (Trigonometric polynomials): a function f ∈ C(ℝ/ℤ; ℂ) is a trigonometric polynomial if f = ∑_{n=-N}^{N} c_n e_n for some integer bound N ≥ 0 and coefficients c_n ∈ ℂ.

Equations

• IsTrigonometricPolynomial f = ∃ (N : ℕ) (c : ℤ → ℂ), f = ∑ n ∈ Finset.Icc (-↑N) ↑N, c n • fourierCharacter n

theorem helperForCorollary_5_3_6_inner_on_support (s : Finset ℤ) (c : ℤ → ℂ) {n : ℤ} (hn : n ∈ s) : inner ℂ (fourierLp 2 n) (∑ k ∈ s, c k • fourierLp 2 k) = c n

Helper for Corollary 5.3.6: coefficient extraction on a finite support set.

theorem helperForCorollary_5_3_6_inner_off_support (s : Finset ℤ) (c : ℤ → ℂ) {n : ℤ} (hn : n ∉ s) : inner ℂ (fourierLp 2 n) (∑ k ∈ s, c k • fourierLp 2 k) = 0

Helper for Corollary 5.3.6: coefficient vanishing outside a finite support set.

theorem helperForCorollary_5_3_6_normSq_finite_sum (s : Finset ℤ) (c : ℤ → ℂ) : ‖∑ k ∈ s, c k • fourierLp 2 k‖ ^ 2 = ∑ k ∈ s, ‖c k‖ ^ 2

Helper for Corollary 5.3.6: finite Parseval identity for a finite Fourier sum.

theorem trigonometricPolynomial_fourierCoefficients_and_normSq (N : ℕ) (c : ℤ → ℂ) : have f := ∑ n ∈ Finset.Icc (-↑N) ↑N, c n • fourierLp 2 n; (∀ n ∈ Finset.Icc (-↑N) ↑N, inner ℂ (fourierLp 2 n) f = c n) ∧ (∀ n ∉ Finset.Icc (-↑N) ↑N, inner ℂ (fourierLp 2 n) f = 0) ∧ ‖f‖ ^ 2 = ∑ n ∈ Finset.Icc (-↑N) ↑N, ‖c n‖ ^ 2

Corollary 5.3.6: for a trigonometric polynomial f = ∑_{n=-N}^{N} c_n e_n, the Fourier coefficient at each n in the support interval is c_n, the coefficients outside that interval vanish, and ‖f‖_2^2 = ∑_{n=-N}^{N} |c_n|^2.

noncomputable def fourierTransform (f : C(AddCircle 1, ℂ)) : ℤ → ℂ

Definition 5.3.7 (Fourier transform): for f ∈ C(ℝ/ℤ; ℂ), its Fourier transform is the function ℤ → ℂ sending n to the n-th Fourier coefficient ∫ x in (0 : ℝ)..1, f x * exp (-2π i n x).

Equations

• fourierTransform f = fourierCoeff ⇑f

noncomputable def fourierSeriesOnAddCircle (f : C(AddCircle 1, ℂ)) : ℤ → C(AddCircle 1, ℂ)

For f ∈ C(ℝ/ℤ; ℂ), the Fourier series term family is n ↦ \hat f(n) e_n.

Equations

• fourierSeriesOnAddCircle f n = fourierTransform f n • fourierCharacter n

def fourierSeries_inversion_plancherel_onAddCircle (f : C(AddCircle 1, ℂ)) : Prop

Definition 5.3.8 (Fourier inversion, Fourier series, and Plancherel formula): for f ∈ C(ℝ/ℤ; ℂ), the Fourier series is the formal family n ↦ \hat f(n) e_n; if f is a trigonometric polynomial, then f equals a finite sum of these Fourier-series terms; and in the same finite case one has the Parseval/Plancherel identity.

Equations

• One or more equations did not get rendered due to their size.

theorem fourierTransform_eq_inner_fourierLp_toLp (f : C(AddCircle 1, ℂ)) (n : ℤ) : fourierTransform f n = inner ℂ (fourierLp 2 n) ((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f)

Bridge fourierTransform to the L² inner product with Fourier modes.

theorem trigonometricPolynomial_fourierInversion (f : C(AddCircle 1, ℂ)) (hf : IsTrigonometricPolynomial f) : ∃ (s : Finset ℤ), (∀ n ∉ s, fourierTransform f n = 0) ∧ f = ∑ n ∈ s, fourierSeriesOnAddCircle f n

If f is a trigonometric polynomial, then f equals a finite sum of its Fourier-series terms (Fourier inversion in the finite case).

theorem trigonometricPolynomial_plancherel_formula (f : C(AddCircle 1, ℂ)) (hf : IsTrigonometricPolynomial f) : ∃ (s : Finset ℤ), (∀ n ∉ s, fourierTransform f n = 0) ∧ ∫ (x : AddCircle 1), ‖f x‖ ^ 2 ∂AddCircle.haarAddCircle = ∑ n ∈ s, ‖fourierTransform f n‖ ^ 2

If f is a trigonometric polynomial, then the finite Parseval/Plancherel identity holds: the L² norm identity on AddCircle equals a finite sum of squared Fourier coefficients.