Finite spectral support for the H⁻¹ ergodic split

These helpers sit above the shared torus Fourier API. They do not define a new Fourier transform or integration convention.

@[instance_reducible]

noncomputable def AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneSpectralMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

• AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneSpectralMeasureSpace1 = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneSpectralMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneSpectralIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.memLp_torusFunction_two_of_cellL2 {d : ℕ} {h : Homogenization.Vec d → ℂ} (hh : MeasureTheory.MemLp h (ENNReal.ofReal 2) (MeasureTheory.volume.restrict (Torus.unitCell d))) : MeasureTheory.MemLp (torusFunction h) (ENNReal.ofReal 2) MeasureTheory.volume

Move an L² function on a Euclidean unit cell to the normalized torus using the existing product-cell measure-preserving equivalence.

theorem AVenhance.Infra.Ergodic.HMinusOneSpectral.periodicToTorusL2_fourierCoeff_eq_smooth {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) (k : Fin d → ℤ) : UnitAddTorus.mFourierCoeff (↑↑(Torus.periodicToTorusL2 f hf)) k = Torus.smoothFourierCoeff f k

theorem AVenhance.Infra.Ergodic.HMinusOneSpectral.smoothFourierCoeff_le_gradientCoeff_of_largeFrequency {d : ℕ} (hd : 0 < d) {φ : Homogenization.Vec d → ℂ} (hφ : ContDiff ℝ 1 φ) (hφper : Torus.IsZdPeriodic φ) (M : ℝ) (hMpos : 0 < M) (q : Fin d → ℤ) (hM : M ≤ ‖q‖) : ‖Torus.smoothFourierCoeff φ q‖ ≤ (∑ i : Fin d, ‖Torus.smoothFourierCoeff (Torus.coordDeriv i φ) q‖ ^ 2) ^ (1 / 2) / (2 * Real.pi * M)

theorem AVenhance.Infra.Ergodic.torusPairing_le_of_fourierGap {d : ℕ} (hd : 0 < d) (h : UnitAddTorus (Fin d) → ℂ) (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) {φ : Homogenization.Vec d → ℂ} (hφ : ContDiff ℝ 1 φ) (hφper : Torus.IsZdPeriodic φ) (M : ℝ) (hM : 0 < M) (hgap : ∀ (q : Fin d → ℤ), ‖q‖ < M → UnitAddTorus.mFourierCoeff h q = 0) : ‖∫ (x : UnitAddTorus (Fin d)), star (h x) * Torus.periodicToTorus φ x‖ ≤ (2 * Real.pi * M)⁻¹ * (∫ (x : UnitAddTorus (Fin d)), ‖h x‖ ^ 2) ^ (1 / 2) * (∑ i : Fin d, ∫ (x : Homogenization.Vec d) in Torus.unitCell d, ‖Torus.coordDeriv i φ x‖ ^ 2) ^ (1 / 2)

A Fourier gap in an L² function gives the sharp reciprocal-frequency bound when paired with a smooth periodic test. The proof uses the torus Hilbert basis, Parseval for the test gradient, and the existing derivative multiplier identity.

theorem AVenhance.Infra.Ergodic.HMinusOneSpectral.integrable_mul_continuousMap {d : ℕ} {g : UnitTorus d → ℂ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (F : C(UnitTorus d, ℂ)) : MeasureTheory.Integrable (fun (x : UnitTorus d) => g x * F x) MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.HMinusOneSpectral.mFourierCoeff_zero_eq_integral_local {d : ℕ} (G : UnitTorus d → ℂ) : UnitAddTorus.mFourierCoeff G 0 = ∫ (x : UnitTorus d), G x

theorem AVenhance.Infra.Ergodic.HMinusOneSpectral.mFourierCoeff_mul_character_shift {d : ℕ} (G : UnitTorus d → ℂ) (q k : Fin d → ℤ) : ∫ (x : UnitAddTorus (Fin d)), (UnitAddTorus.mFourier (-q)) x * ((UnitAddTorus.mFourier k) x * G x) = UnitAddTorus.mFourierCoeff G (q - k)

theorem AVenhance.Infra.Ergodic.mFourierCoeff_mul_eq_zero_of_finiteSupport_fast {d N : ℕ} (hN : 0 < N) (S : Finset (Fin d → ℤ)) (a : (Fin d → ℤ) → ℂ) (P : C(UnitTorus d, ℂ)) (G : UnitTorus d → ℂ) (hP : ∀ (x : UnitTorus d), P x = ∑ k ∈ S, a k * (UnitAddTorus.mFourier k) x) (M : ℝ) (hS : ∀ k ∈ S, ‖k‖ ≤ M) (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hGmean : ∫ (x : UnitTorus d), G x = 0) (hGfast : ∀ (i : Fin d) (x : UnitTorus d), G (x + fastTorusShift N i) = G x) (q : Fin d → ℤ) (hq : ‖q‖ < ↑N - M) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin d)) => P x * G x) q = 0

A finite Fourier polynomial times a mean-zero N⁻¹ℤᵈ-periodic function has no Fourier coefficient below the gap between the fast lattice and the polynomial support. The finite expansion premise is the interface consumed by the symmetric cutoff realFourierProjection.