The basic L¹ ergodic estimate

@[instance_reducible]

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

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

Equations

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

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

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

theorem AVenhance.Infra.Ergodic.AveragesL1.toUnitTorus_isOpenQuotientMap (d : ℕ) : IsOpenQuotientMap (Torus.toUnitTorus d)

theorem AVenhance.Infra.Ergodic.periodicToTorus_continuous_of_periodic {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) (hper : Torus.IsZdPeriodic f) : Continuous (Torus.periodicToTorus f)

theorem AVenhance.Infra.Ergodic.AveragesL1.unitCell_subset_closedCube (d : ℕ) : Torus.unitCell d ⊆ Set.univ.pi fun (x : Fin d) => Set.Icc 0 1

theorem AVenhance.Infra.Ergodic.integrable_periodicToTorus_of_locallyIntegrable {d : ℕ} {g : Homogenization.Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) : MeasureTheory.Integrable (Torus.periodicToTorus g) MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.AveragesL1.smoothFourierCoeff_eq_mFourierCoeff_periodicToTorus {d : ℕ} {f : Homogenization.Vec d → ℂ} (hper : Torus.IsZdPeriodic f) (hf : Continuous f) (k : Fin d → ℤ) : UnitAddTorus.mFourierCoeff (⇑{ toFun := Torus.periodicToTorus f, continuous_toFun := ⋯ }) k = Torus.smoothFourierCoeff f k

theorem AVenhance.Infra.Ergodic.fastFrequency_norm_ge_nat {d N : ℕ} (hN : 0 < N) {k : Fin d → ℤ} (hk0 : k ≠ 0) (hk : IsFastFrequency N k) : ↑N ≤ ‖k‖

theorem AVenhance.Infra.Ergodic.AveragesL1.periodicToTorus_eq_torusFunction {d : ℕ} {α : Type u_1} (f : Homogenization.Vec d → α) : Torus.periodicToTorus f = torusFunction f

theorem AVenhance.Infra.Ergodic.cellAverage_mul_sub_le_of_coordinateAnalyticL1Bounds {d N : ℕ} (hd : 0 < d) (hN : 0 < N) {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZPeriodic f) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hderiv : HasCoordinateAnalyticL1Bounds (fun (x : Homogenization.Vec d) => ↑(f x)) Cf r) {g : Homogenization.Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (hfast : IsFastPeriodic N g) (hNr : 1 ≤ r * ↑N) : |(cellAverage fun (x : Homogenization.Vec d) => f x * g x) - cellAverage f * cellAverage g| ≤ ((512 * Cf * cellAverage fun (x : Homogenization.Vec d) => |g x|) * ∑' (k : Fin d → ℤ), Real.exp (-(1 / 1024) * ‖k‖)) * Real.exp (-(r * ↑N) / 1024)

The basic ergodic covariance estimate. Its analytic premise is given in coordinate form, since only repeated coordinate derivatives enter the Fourier multiplier proof. The proof needs r > 0, Cf ≥ 0, and Nr ≥ 1; it does not use the paper's extra upper bound r ≤ 1.