3D Torus Foundations

This file establishes the 3D Torus as a formal measure space.

@[reducible, inline]

abbrev Torus3 : Type

The 3D Torus is defined as (ℝ/ℤ)³.

Equations

• Torus3 = UnitAddTorus (Fin 3)

instance instMeasureSpaceTorus3 : MeasureTheory.MeasureSpace Torus3

Standard volume on Torus3.

Equations

• instMeasureSpaceTorus3 = { toMeasurableSpace := MeasurableSpace.pi, volume := MeasureTheory.Measure.pi fun (x : Fin 3) => MeasureTheory.volume }

instance instIsProbabilityMeasureTorus3Volume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

instance instFactLeENNRealOfNat_navierStokes : Fact (1 ≤ 2)

def torusMon (k : Fin 3 → ℤ) : C(Torus3, ℂ)

Fourier monomials on the 3D Torus.

Equations

• torusMon k = UnitAddTorus.mFourier k

theorem orthonormal_torusMon : Orthonormal ℂ fun (k : Fin 3 → ℤ) => (ContinuousMap.toLp 2 MeasureTheory.volume ℂ) (torusMon k)

Orthnormality of Fourier monomials in L²(Torus3).

def torusFourierCoeff (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (k : Fin 3 → ℤ) : ℂ

Definition of Fourier coefficients for L² functions on Torus3.

Equations

• torusFourierCoeff f k = ↑(UnitAddTorus.mFourierBasis.repr f) k