Multivariate Fourier series

In this file we define the Fourier series of an L² function on the d-dimensional unit circle, and show that it converges to the function in the L² norm. We also prove uniform convergence of the Fourier series if f is continuous and the sequence of its Fourier coefficients is summable.

@[implicit_reducible]

noncomputable def instMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

In this file we normalise the measure on ℝ / ℤ to have total volume 1.

theorem instIsAddHaarMeasureUnitAddCircleVolume : MeasureTheory.volume.IsAddHaarMeasure

The measure on ℝ / ℤ is a Haar measure.

theorem instIsProbabilityMeasureUnitAddCircleVolume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

The measure on ℝ / ℤ is a probability measure.

@[reducible, inline]

abbrev UnitAddTorus (d : Type u_1) : Type u_1

The product of finitely many copies of the unit circle, indexed by d.

noncomputable def UnitAddTorus.mFourier {d : Type u_1} [Fintype d] (n : d → ℤ) : C(UnitAddTorus d, ℂ)

Exponential monomials in d variables.

theorem UnitAddTorus.mFourier_neg {d : Type u_1} [Fintype d] {n : d → ℤ} {x : UnitAddTorus d} : (mFourier (-n)) x = (starRingEnd ℂ) ((mFourier n) x)

theorem UnitAddTorus.mFourier_add {d : Type u_1} [Fintype d] {n : d → ℤ} {x : UnitAddTorus d} {m : d → ℤ} : (mFourier (m + n)) x = (mFourier m) x * (mFourier n) x

theorem UnitAddTorus.mFourier_zero {d : Type u_1} [Fintype d] : mFourier 0 = 1

theorem UnitAddTorus.mFourier_norm {d : Type u_1} [Fintype d] {n : d → ℤ} : ‖mFourier n‖ = 1

theorem UnitAddTorus.mFourier_single {d : Type u_1} [Fintype d] [DecidableEq d] (z : d → AddCircle 1) (i : d) : (mFourier (Pi.single i 1)) z = (fourier 1) (z i)

noncomputable def UnitAddTorus.mFourierSubalgebra (d : Type u_2) [Fintype d] : StarSubalgebra ℂ C(UnitAddTorus d, ℂ)

The star subalgebra of C(UnitAddTorus d, ℂ) generated by mFourier n for n ∈ ℤᵈ.

theorem UnitAddTorus.mFourierSubalgebra_coe {d : Type u_1} [Fintype d] : Subalgebra.toSubmodule (mFourierSubalgebra d).toSubalgebra = Submodule.span ℂ (Set.range mFourier)

The star subalgebra of C(UnitAddTorus d, ℂ) generated by mFourier n for n ∈ ℤᵈ is in fact the linear span of these functions.

theorem UnitAddTorus.mFourierSubalgebra_separatesPoints {d : Type u_1} [Fintype d] : (mFourierSubalgebra d).SeparatesPoints

The subalgebra of C(UnitAddTorus d, ℂ) generated by mFourier n for n ∈ ℤᵈ separates points.

theorem UnitAddTorus.mFourierSubalgebra_closure_eq_top {d : Type u_1} [Fintype d] : (mFourierSubalgebra d).topologicalClosure = ⊤

The subalgebra of C(UnitAddTorus d, ℂ) generated by mFourier n for n : d → ℤ is dense.

theorem UnitAddTorus.span_mFourier_closure_eq_top {d : Type u_1} [Fintype d] : (Submodule.span ℂ (Set.range mFourier)).topologicalClosure = ⊤

The linear span of the monomials mFourier n is dense in C(UnitAddTorus d, ℂ).

noncomputable def UnitAddTorus.measurableEquivPiIoc {ι : Type u_2} (b : ι → ℝ) : UnitAddTorus ι ≃ᵐ { x : ι → ℝ // ∀ (i : ι), x i ∈ Set.Ioc (b i) (b i + 1) }

The measurable equivalence between UnitAddTorus and a product of Ioc intervals.

theorem UnitAddTorus.coe_measurableEquivPiIoc {ι : Type u_2} (b : ι → ℝ) : ⇑(measurableEquivPiIoc b) = fun (x : UnitAddTorus ι) => ⟨fun (i : ι) => ↑((AddCircle.equivIoc 1 (b i)) (x i)), ⋯⟩

@[simp]

theorem UnitAddTorus.coe_measurableEquivPiIoc_apply {ι : Type u_2} (b : ι → ℝ) (x : UnitAddTorus ι) : (measurableEquivPiIoc b) x = ⟨fun (i : ι) => ↑((AddCircle.equivIoc 1 (b i)) (x i)), ⋯⟩

theorem UnitAddTorus.coe_symm_measurableEquivPiIoc {ι : Type u_2} (b : ι → ℝ) : ⇑(measurableEquivPiIoc b).symm = fun (x : { x : ι → ℝ // ∀ (i : ι), x i ∈ Set.Ioc (b i) (b i + 1) }) (i : ι) => ↑(↑x i)

@[simp]

theorem UnitAddTorus.coe_symm_measurableEquivPiIoc_apply {ι : Type u_2} (b : ι → ℝ) (y : { x : ι → ℝ // ∀ (i : ι), x i ∈ Set.Ioc (b i) (b i + 1) }) : (measurableEquivPiIoc b).symm y = fun (i : ι) => ↑(↑y i)

theorem UnitAddTorus.measurePreserving_equivPiIoc {d : Type u_1} [Fintype d] (a : d → ℝ) : MeasureTheory.MeasurePreserving (⇑(measurableEquivPiIoc a)) MeasureTheory.volume (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)

The equivalence measurableEquivPiIoc is measure preserving.

theorem UnitAddTorus.lintegral_preimage {d : Type u_1} [Fintype d] (f : UnitAddTorus d → ENNReal) (a : d → ℝ) : ∫⁻ (x : UnitAddTorus d), f x = ∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Set.Ioc (a i) (a i + 1)}, f fun (i : d) => ↑(x i)

theorem UnitAddTorus.integral_preimage {d : Type u_1} [Fintype d] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : UnitAddTorus d → E) (a : d → ℝ) : ∫ (x : UnitAddTorus d), f x = ∫ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Set.Ioc (a i) (a i + 1)}, f fun (i : d) => ↑(x i)

@[reducible, inline]

noncomputable abbrev UnitAddTorus.mFourierLp {d : Type u_1} [Fintype d] (p : ENNReal) [Fact (1 ≤ p)] (n : d → ℤ) : ↥(MeasureTheory.Lp ℂ p MeasureTheory.volume)

The family of monomials mFourier n, parametrized by n : ℤᵈ and considered as elements of the Lp space of functions UnitAddTorus d → ℂ.

theorem UnitAddTorus.coeFn_mFourierLp {d : Type u_1} [Fintype d] (p : ENNReal) [Fact (1 ≤ p)] (n : d → ℤ) : ↑↑(mFourierLp p n) =ᵐ[MeasureTheory.volume] ⇑(mFourier n)

instance UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp {d : Type u_1} [Fintype d] {p : ENNReal} [Fact (1 ≤ p)] : ContinuousSMul ℂ ↥(MeasureTheory.Lp ℂ p MeasureTheory.volume)

theorem UnitAddTorus.span_mFourierLp_closure_eq_top {d : Type u_1} [Fintype d] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : (Submodule.span ℂ (Set.range (mFourierLp p))).topologicalClosure = ⊤

For each 1 ≤ p < ∞, the linear span of the monomials mFourier n is dense in the Lᵖ space of functions on UnitAddTorus d.

theorem UnitAddTorus.orthonormal_mFourier {d : Type u_1} [Fintype d] : Orthonormal ℂ (mFourierLp 2)

The monomials mFourierLp 2 n are an orthonormal set in L².

noncomputable def UnitAddTorus.mFourierCoeff {d : Type u_1} [Fintype d] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : UnitAddTorus d → E) (n : d → ℤ) : E

The n-th Fourier coefficient of a function UnitAddTorus d → E, for E a complete normed ℂ-vector space, defined as the integral over UnitAddTorus d of mFourier (-n) t • f t.

theorem UnitAddTorus.mFourierCoeff_eq_integral {d : Type u_1} [Fintype d] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : UnitAddTorus d → E) (n : d → ℤ) (a : d → ℝ) : mFourierCoeff f n = ∫ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Set.Ioc (a i) (a i + 1)}, ((mFourier (-n)) fun (i : d) => ↑(x i)) • f fun (i : d) => ↑(x i)

The Fourier coefficients of a function on UnitAddTorus d can be computed as integrals over ∏ i, (aᵢ, aᵢ + 1], for any a : d → ℝ.

noncomputable def UnitAddTorus.mFourierBasis {d : Type u_1} [Fintype d] : HilbertBasis (d → ℤ) ℂ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

We define mFourierBasis to be a ℤᵈ-indexed Hilbert basis for the L² space of functions on UnitAddTorus d, which by definition is an isometric isomorphism from L²(UnitAddTorus d) to ℓ²(ℤᵈ, ℂ).

@[simp]

theorem UnitAddTorus.coe_mFourierBasis {d : Type u_1} [Fintype d] : ⇑mFourierBasis = mFourierLp 2

The elements of the Hilbert basis mFourierBasis are the functions mFourierLp 2, i.e. the monomials mFourier n on UnitAddTorus d considered as elements of L².

theorem UnitAddTorus.mFourierBasis_repr {d : Type u_1} [Fintype d] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (i : d → ℤ) : ↑(mFourierBasis.repr f) i = mFourierCoeff (↑↑f) i

Under the isometric isomorphism mFourierBasis from L²(UnitAddTorus d) to ℓ²(ℤᵈ, ℂ), the i-th coefficient is mFourierCoeff f i.

theorem UnitAddTorus.hasSum_mFourier_series_L2 {d : Type u_1} [Fintype d] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasSum (fun (i : d → ℤ) => mFourierCoeff (↑↑f) i • mFourierLp 2 i) f

The Fourier series of an L2 function f sums to f in the L² norm.

theorem UnitAddTorus.hasSum_prod_mFourierCoeff {d : Type u_1} [Fintype d] (f g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasSum (fun (i : d → ℤ) => (starRingEnd ℂ) (mFourierCoeff (↑↑f) i) * mFourierCoeff (↑↑g) i) (∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑f t) * ↑↑g t)

Parseval's identity for inner products: for L² functions f, g on UnitAddTorus d, the inner product of the Fourier coefficients of f and g is the inner product of f and g.

theorem UnitAddTorus.hasSum_sq_mFourierCoeff {d : Type u_1} [Fintype d] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasSum (fun (i : d → ℤ) => ‖mFourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : UnitAddTorus d), ‖↑↑f t‖ ^ 2)

Parseval's identity for norms: for an L² function f on UnitAddTorus d, the sum of the squared norms of the Fourier coefficients equals the L² norm of f.

theorem UnitAddTorus.mFourierCoeff_toLp {d : Type u_1} [Fintype d] (f : C(UnitAddTorus d, ℂ)) (n : d → ℤ) : mFourierCoeff (↑↑((ContinuousMap.toLp 2 MeasureTheory.volume ℂ) f)) n = mFourierCoeff (⇑f) n

theorem UnitAddTorus.hasSum_mFourier_series_of_summable {d : Type u_1} [Fintype d] {f : C(UnitAddTorus d, ℂ)} (h : Summable (mFourierCoeff ⇑f)) : HasSum (fun (i : d → ℤ) => mFourierCoeff (⇑f) i • mFourier i) f

If the sequence of Fourier coefficients of f is summable, then the Fourier series converges uniformly to f.

theorem UnitAddTorus.hasSum_mFourier_series_apply_of_summable {d : Type u_1} [Fintype d] {f : C(UnitAddTorus d, ℂ)} (h : Summable (mFourierCoeff ⇑f)) (x : UnitAddTorus d) : HasSum (fun (i : d → ℤ) => mFourierCoeff (⇑f) i • (mFourier i) x) (f x)

If the sequence of Fourier coefficients of f is summable, then the Fourier series of f converges everywhere pointwise to f.