Fourier coefficient bounds for the basic ergodic estimate

@[instance_reducible]

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

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

Equations

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

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

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

theorem AVenhance.Infra.Ergodic.BasicL1.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

noncomputable def AVenhance.Infra.Ergodic.BasicL1.pairingLinearMap {d : ℕ} (g : UnitTorus d → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : C(UnitTorus d, ℂ) →ₗ[ℂ] ℂ

Pair an integrable torus function with a continuous test function, linearly in the test.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Ergodic.BasicL1.pairingContinuousLinearMap {d : ℕ} (g : UnitTorus d → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : C(UnitTorus d, ℂ) →L[ℂ] ℂ

Continuous linear form obtained by pairing with an integrable torus function.

Equations

• AVenhance.Infra.Ergodic.BasicL1.pairingContinuousLinearMap g hg = (AVenhance.Infra.Ergodic.BasicL1.pairingLinearMap g hg).mkContinuous (∫ (x : AVenhance.Infra.Ergodic.UnitTorus d), ‖g x‖) ⋯

theorem AVenhance.Infra.Ergodic.BasicL1.pairing_apply_fourierTerm {d : ℕ} (g : UnitTorus d → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (a : ℂ) (k : Fin d → ℤ) : (pairingContinuousLinearMap g hg) (a • UnitAddTorus.mFourier k) = a * UnitAddTorus.mFourierCoeff g (-k)

theorem AVenhance.Infra.Ergodic.hasSum_integral_mul_fourierCoeff {d : ℕ} (f : C(UnitTorus d, ℂ)) (g : UnitTorus d → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hf : Summable (UnitAddTorus.mFourierCoeff ⇑f)) : HasSum (fun (k : Fin d → ℤ) => UnitAddTorus.mFourierCoeff (⇑f) k * UnitAddTorus.mFourierCoeff g (-k)) (∫ (x : UnitTorus d), f x * g x)

Integrating a Fourier series against an L¹ function gives the usual coefficient pairing.

theorem AVenhance.Infra.Ergodic.mFourierCoeff_norm_le_integral_norm {d : ℕ} (g : UnitTorus d → ℂ) (k : Fin d → ℤ) : ‖UnitAddTorus.mFourierCoeff g k‖ ≤ ∫ (x : UnitTorus d), ‖g x‖

A Fourier coefficient of an integrable function is bounded by its L¹ norm on the normalized torus.

theorem AVenhance.Infra.Ergodic.mFourierCoeff_eq_zero_of_translation_invariant {d : ℕ} (g : UnitTorus d → ℂ) (k : Fin d → ℤ) (a : UnitTorus d) (hga : ∀ (x : UnitTorus d), g (x + a) = g x) (hchar : (UnitAddTorus.mFourier (-k)) a ≠ 1) : UnitAddTorus.mFourierCoeff g k = 0

A translation-invariant function has zero Fourier coefficient whenever the character is nontrivial on the translation.

theorem AVenhance.Infra.Ergodic.mFourierCoeff_eq_zero_of_fastTorusShift {d N : ℕ} (g : UnitTorus d → ℂ) (k : Fin d → ℤ) (i : Fin d) (hg : ∀ (x : UnitTorus d), g (x + fastTorusShift N i) = g x) (hchar : (UnitAddTorus.mFourier (-k)) (fastTorusShift N i) ≠ 1) : UnitAddTorus.mFourierCoeff g k = 0

Fast-periodic torus functions have no coefficient at a character that is nontrivial on a coordinate fast-period shift.

theorem AVenhance.Infra.Ergodic.BasicL1.mFourier_fastTorusShift_formula {d N : ℕ} (hN : 0 < N) (k : Fin d → ℤ) (i : Fin d) : (UnitAddTorus.mFourier (-k)) (fastTorusShift N i) = Complex.exp (2 * ↑Real.pi * Complex.I * -↑(k i) / ↑N)

theorem AVenhance.Infra.Ergodic.BasicL1.exp_two_pi_I_mul_int_div_eq_one_iff {n : ℤ} {N : ℕ} (hN : N ≠ 0) : Complex.exp (2 * ↑Real.pi * Complex.I * ↑n / ↑N) = 1 ↔ ↑N ∣ n

def AVenhance.Infra.Ergodic.IsFastFrequency {d : ℕ} (N : ℕ) (k : Fin d → ℤ) : Prop

A frequency lies in the sublattice N ℤ^d.

Equations

• AVenhance.Infra.Ergodic.IsFastFrequency N k = ∀ (i : Fin d), ↑N ∣ k i

@[instance_reducible]

instance AVenhance.Infra.Ergodic.fastFrequencyDecidable {d N : ℕ} (k : Fin d → ℤ) : Decidable (IsFastFrequency N k)

Equations

• AVenhance.Infra.Ergodic.fastFrequencyDecidable k = id inferInstance

theorem AVenhance.Infra.Ergodic.BasicL1.hasSum_sub_single {ι : Type u_1} [DecidableEq ι] (i₀ : ι) {f : ι → ℂ} {s : ℂ} (hf : HasSum f s) : HasSum (fun (k : ι) => if k = i₀ then 0 else f k) (s - f i₀)

theorem AVenhance.Infra.Ergodic.mFourierCoeff_eq_zero_of_fastPeriod_not_dvd {d N : ℕ} {g : UnitTorus d → ℂ} (hN : 0 < N) (k : Fin d → ℤ) (i : Fin d) (hg : ∀ (x : UnitTorus d), g (x + fastTorusShift N i) = g x) (hnot : ¬↑N ∣ k i) : UnitAddTorus.mFourierCoeff g k = 0

A coefficient of an N⁻¹-periodic function vanishes at every frequency whose selected coordinate is not divisible by N.

theorem AVenhance.Infra.Ergodic.mFourierCoeff_eq_zero_of_not_fastFrequencyLattice {d N : ℕ} {g : UnitTorus d → ℂ} (hN : 0 < N) (k : Fin d → ℤ) (hg : ∀ (i : Fin d) (x : UnitTorus d), g (x + fastTorusShift N i) = g x) (hnot : ¬∀ (i : Fin d), ↑N ∣ k i) : UnitAddTorus.mFourierCoeff g k = 0

A function invariant under every coordinate fast-period shift has Fourier support contained in the sublattice N ℤ^d.

theorem AVenhance.Infra.Ergodic.BasicL1.mFourierCoeff_zero_eq_integral {d : ℕ} (f : UnitTorus d → ℂ) : UnitAddTorus.mFourierCoeff f 0 = ∫ (x : UnitTorus d), f x

theorem AVenhance.Infra.Ergodic.torusCovariance_le_fourier_envelope {d N : ℕ} (F : C(UnitTorus d, ℂ)) (G : UnitTorus d → ℂ) (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hF : Summable (UnitAddTorus.mFourierCoeff ⇑F)) (A rate : ℝ) (hA : 0 ≤ A) (hdecay : ∀ (k : Fin d → ℤ), k ≠ 0 → IsFastFrequency N k → ‖UnitAddTorus.mFourierCoeff (⇑F) k‖ ≤ A * Real.exp (-rate * ‖k‖)) (hzero : ∀ (k : Fin d → ℤ), k ≠ 0 → ¬IsFastFrequency N k → UnitAddTorus.mFourierCoeff G (-k) = 0) (htail : Summable fun (k : Fin d → ℤ) => if k = 0 then 0 else if IsFastFrequency N k then Real.exp (-rate * ‖k‖) else 0) : ‖(∫ (x : UnitTorus d), F x * G x) - (∫ (x : UnitTorus d), F x) * ∫ (x : UnitTorus d), G x‖ ≤ (A * ∫ (x : UnitTorus d), ‖G x‖) * ∑' (k : Fin d → ℤ), if k = 0 then 0 else if IsFastFrequency N k then Real.exp (-rate * ‖k‖) else 0

Fourier covariance bound from exponential coefficient decay and fast frequency support. The lattice exponential tail is left explicit so callers can use the sharp counting estimate appropriate to their dimension.