Fourier coefficients and Parseval on the unit torus and its Euclidean cell.

@[instance_reducible]

noncomputable def avInfraTorusFourierMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• avInfraTorusFourierMeasureSpace1 = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem avInfraTorusFourierMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraTorusFourierIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Torus.TorusL2 (d : ℕ) : AddSubgroup (UnitAddTorus (Fin d) →ₘ[MeasureTheory.volume] ℂ)

The L² space on the unit torus.

Equations

• AVenhance.Infra.Torus.TorusL2 d = MeasureTheory.Lp ℂ 2 MeasureTheory.volume

noncomputable def AVenhance.Infra.Torus.periodicL2Representative {d : ℕ} (f : ↥(TorusL2 d)) : Homogenization.Vec d → ℂ

The periodic Euclidean representative of an L² torus function.

Equations

• AVenhance.Infra.Torus.periodicL2Representative f = AVenhance.Infra.Torus.fromUnitTorus fun (x : UnitAddTorus (Fin d)) => ↑↑f x

noncomputable def AVenhance.Infra.Torus.periodicL2FourierCoeff {d : ℕ} (f : ↥(TorusL2 d)) (k : Fin d → ℤ) : ℂ

The kth Fourier coefficient of a torus L² function, using Mathlib's mFourierCoeff.

Equations

• AVenhance.Infra.Torus.periodicL2FourierCoeff f k = UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin d)) => ↑↑f x) k

theorem AVenhance.Infra.Torus.hasSum_sq_periodicL2FourierCoeff {d : ℕ} (f : ↥(TorusL2 d)) : HasSum (fun (k : Fin d → ℤ) => ‖periodicL2FourierCoeff f k‖ ^ 2) (∫ (x : Homogenization.Vec d) in unitCell d, ‖periodicL2Representative f x‖ ^ 2)

Parseval's identity for a periodic L² function, integrated over the Euclidean unit cell.