The volume on the unit torus

Mathlib states its results on Fourier series on the unit torus UnitAddTorus d = (ℝ / ℤ)^d, such as UnitAddTorus.orthonormal_mFourier and the definition of UnitAddTorus.mFourierCoeff, for a file-local measure: the product of the Haar probability measures AddCircle.haarAddCircle on the circle factors. This file records that this product is the global volume on the torus, so that those results can be read for volume.

Main results

• An instance stating that the volume on the unit circle UnitAddCircle is a probability measure.
• TauCeti.UnitAddTorus.volume_eq_pi_haarAddCircle: the volume on the unit torus is the product of the Haar probability measures on its circle factors.
• TauCeti.UnitAddTorus.mFourierCoeff_eq_integral_volume: the Fourier coefficients on the unit torus are integrals for the volume.

instance TauCeti.instIsProbabilityMeasureUnitAddCircleVolume_tauCeti : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

The volume on the unit circle ℝ / ℤ is a probability measure.

theorem TauCeti.UnitAddTorus.volume_eq_pi_haarAddCircle {d : Type u_1} [Fintype d] : MeasureTheory.volume = MeasureTheory.Measure.pi fun (x : d) => AddCircle.haarAddCircle

The volume on the unit torus is the product of the Haar probability measures on its circle factors.

theorem TauCeti.UnitAddTorus.mFourierCoeff_eq_integral_volume {d : Type u_1} [Fintype d] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : UnitAddTorus d → E) (n : d → ℤ) : UnitAddTorus.mFourierCoeff f n = ∫ (z : UnitAddTorus d), (UnitAddTorus.mFourier (-n)) z • f z

The Fourier coefficients of f are integrals for the volume of the torus. Mathlib defines mFourierCoeff using the Haar probability measure on each circle factor; this is the volume.