theorem helperForTheorem_5_5_1_hasSum_fourier_series_toLp (f : C(AddCircle 1, ℂ)) : HasSum (fun (n : ℤ) => fourierCoeff (⇑f) n • fourierLp 2 n) ((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f)

Helper for Theorem 5.5.1: the Fourier series of f viewed in L² has the expected coefficient formula and sums to toLp f.

theorem helperForTheorem_5_5_1_tendsto_symmetricIntegerWindows : Filter.Tendsto (fun (N : ℕ) => Finset.Icc (-↑N) ↑N) Filter.atTop Filter.atTop

Helper for Theorem 5.5.1: symmetric integer windows [-N, N] tend to atTop in Finset ℤ.

theorem helperForTheorem_5_5_1_tendsto_partialSums_in_Lp (f : C(AddCircle 1, ℂ)) : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (⇑f) n • fourierLp 2 n) Filter.atTop (nhds ((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f))

Helper for Theorem 5.5.1: symmetric Fourier partial sums converge to toLp f in L².

theorem helperForTheorem_5_5_1_normError_tendsto_zero (f : C(AddCircle 1, ℂ)) : Filter.Tendsto (fun (N : ℕ) => ‖(ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f - ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (⇑f) n • fourierLp 2 n‖) Filter.atTop (nhds 0)

Helper for Theorem 5.5.1: the L² norm of the Fourier approximation error tends to 0.

theorem fourier_series_tendsto_in_L2 (f : C(AddCircle 1, ℂ)) : Filter.Tendsto (fun (N : ℕ) => ‖(ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f - ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (⇑f) n • fourierLp 2 n‖) Filter.atTop (nhds 0)

Theorem 5.5.1 (Fourier theorem): for every f ∈ C(ℝ/ℤ; ℂ), the symmetric Fourier partial sums ∑_{n=-N}^{N} \hat f(n) e_n converge to f in the L² metric, i.e. lim_{N→∞} ‖f - ∑_{n=-N}^{N} \hat f(n)e_n‖₂ = 0.

theorem helperForTheorem_5_5_3_summable_fourierCoeff (f : C(AddCircle 1, ℂ)) (habs : Summable fun (n : ℤ) => ‖fourierCoeff (⇑f) n‖) : Summable fun (n : ℤ) => fourierCoeff (⇑f) n

Helper for Theorem 5.5.3: absolute summability of Fourier coefficients implies summability of the coefficients themselves.

theorem helperForTheorem_5_5_3_tendsto_symmetricPartialSums (f : C(AddCircle 1, ℂ)) (hcoeff : Summable fun (n : ℤ) => fourierCoeff (⇑f) n) : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (⇑f) n • fourier n) Filter.atTop (nhds f)

Helper for Theorem 5.5.3: summable Fourier coefficients force symmetric Fourier partial sums to converge to f in C(ℝ/ℤ; ℂ).

theorem helperForTheorem_5_5_3_normError_tendsto_zero (f : C(AddCircle 1, ℂ)) (hpartial : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (⇑f) n • fourier n) Filter.atTop (nhds f)) : Filter.Tendsto (fun (N : ℕ) => ‖f - ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (⇑f) n • fourier n‖) Filter.atTop (nhds 0)

Helper for Theorem 5.5.3: convergence of symmetric partial sums to f implies convergence of the sup-norm error to 0.

theorem fourier_series_tendsto_uniform_of_summable_fourierCoefficients (f : C(AddCircle 1, ℂ)) (habs : Summable fun (n : ℤ) => ‖fourierCoeff (⇑f) n‖) : Filter.Tendsto (fun (N : ℕ) => ‖f - ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeff (⇑f) n • fourier n‖) Filter.atTop (nhds 0)

Theorem 5.5.3: let f ∈ C(ℝ/ℤ; ℂ). If ∑_{n∈ℤ} ‖\hat f(n)‖ converges, then the symmetric Fourier partial sums ∑_{n=-N}^{N} \hat f(n)e_n converge uniformly to f, i.e. lim_{N→∞} ‖f - ∑_{n=-N}^{N} \hat f(n)e_n‖∞ = 0 (with ‖·‖ the sup norm on C(ℝ/ℤ; ℂ)).

theorem helperForTheorem_5_5_4_hasSum_sq_fourierCoeff_toLp (f : C(AddCircle 1, ℂ)) : HasSum (fun (n : ℤ) => ‖fourierCoeff (⇑f) n‖ ^ 2) (∫ (t : AddCircle 1), ‖↑↑((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f) t‖ ^ 2 ∂AddCircle.haarAddCircle)

Helper for Theorem 5.5.4: Parseval's HasSum identity for toLp f, with Fourier coefficients rewritten in terms of the original continuous map f.

theorem helperForTheorem_5_5_4_normSq_toLp_eq_integral_normSq (f : C(AddCircle 1, ℂ)) : ‖(ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f‖ ^ 2 = ∫ (t : AddCircle 1), ‖↑↑((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f) t‖ ^ 2 ∂AddCircle.haarAddCircle

Helper for Theorem 5.5.4: for toLp f, the square of the L² norm equals the integral of the pointwise squared norm.

theorem helperForTheorem_5_5_4_tsum_sq_fourierCoeff_eq_normSq (f : C(AddCircle 1, ℂ)) : ∑' (n : ℤ), ‖fourierCoeff (⇑f) n‖ ^ 2 = ‖(ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f‖ ^ 2

Helper for Theorem 5.5.4: the Parseval tsum identity for continuous maps on AddCircle 1.

theorem helperForTheorem_5_5_4_summable_sq_fourierCoeff (f : C(AddCircle 1, ℂ)) : Summable fun (n : ℤ) => ‖fourierCoeff (⇑f) n‖ ^ 2

Helper for Theorem 5.5.4: summability of squared Fourier coefficients for continuous maps on AddCircle 1.

theorem continuousMap_norm_sq_eq_tsum_sq_fourierCoeff (f : C(AddCircle 1, ℂ)) : (Summable fun (n : ℤ) => ‖fourierCoeff (⇑f) n‖ ^ 2) ∧ ‖(ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f‖ ^ 2 = ∑' (n : ℤ), ‖fourierCoeff (⇑f) n‖ ^ 2

Theorem 5.5.4 (Plancherel / Parseval): for any f ∈ C(ℝ/ℤ; ℂ), the series ∑_{n∈ℤ} |\hat f(n)|^2 converges and the L² norm identity ‖f‖₂^2 = ∑_{n=-∞}^{∞} |\hat f(n)|^2 holds.