The spectral homogeneous H⁻¹ ergodic estimate

@[irreducible]

noncomputable def AVenhance.Infra.Ergodic.ergodicFourierWeight (d : ℕ) : ℝ

The dimension-dependent Fourier weight appearing in the source estimate.

Equations

• AVenhance.Infra.Ergodic.ergodicFourierWeight d = ∑' (k : Fin d → ℤ), Real.exp (-(1 / 1024) * ‖k‖)

theorem AVenhance.Infra.Ergodic.ergodicFourierWeight_eq_tsum (d : ℕ) : ergodicFourierWeight d = ∑' (k : Fin d → ℤ), Real.exp (-(1 / 1024) * ‖k‖)

@[instance_reducible]

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

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

Equations

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

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

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

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.torusRepresentative_eq_cellRepresentative {d : ℕ} (x : UnitAddTorus (Fin d)) : Torus.unitTorusRepresentative d x = unitCellRepresentative x

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.integral_torusFunction_eq_unitCell {d : ℕ} {v : Homogenization.Vec d → ℂ} : ∫ (x : UnitAddTorus (Fin d)), torusFunction v x = ∫ (x : Homogenization.Vec d) in Torus.unitCell d, v x

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.cellAverage_absSq_eq_sq {d : ℕ} {u : Homogenization.Vec d → ℝ} : (cellAverage fun (x : Homogenization.Vec d) => |u x| ^ 2) = cellAverage fun (x : Homogenization.Vec d) => u x ^ 2

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.l2norm_cell_eq_average_absSq {d : ℕ} {u : Homogenization.Vec d → ℝ} : (∫ (x : Homogenization.Vec d) in Torus.unitCell d, u x ^ 2) ^ (1 / 2) = (cellAverage fun (x : Homogenization.Vec d) => |u x| ^ 2) ^ (1 / 2)

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.cellAverage_mul_split {d : ℕ} {f p q g : Homogenization.Vec d → ℝ} (hpg : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => p x * g x) MeasureTheory.volume) (hqg : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => q x * g x) MeasureTheory.volume) (hpoint : ∀ (x : Homogenization.Vec d), f x * g x = p x * g x + q x * g x) : (cellAverage fun (x : Homogenization.Vec d) => f x * g x) = (cellAverage fun (x : Homogenization.Vec d) => p x * g x) + cellAverage fun (x : Homogenization.Vec d) => q x * g x

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.complex_norm_ofReal_square {x : ℝ} : ‖↑x‖ ^ 2 = x ^ 2

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.mFourierCoeff_zero_eq_integral_local {d : ℕ} (H : UnitAddTorus (Fin d) → ℂ) : UnitAddTorus.mFourierCoeff H 0 = ∫ (x : UnitAddTorus (Fin d)), H x

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.lowProjection_fastProduct_mean_gap {d N M : ℕ} (hN : 0 < N) (hgapPos : 0 < ↑N - ↑M) {f g : Homogenization.Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => |g x| ^ 2) MeasureTheory.volume) (hfast : IsFastPeriodic N g) (hgMean : cellAverage g = 0) : (cellAverage fun (x : Homogenization.Vec d) => lowProjection f M x * g x) = 0 ∧ ∀ (q : Fin d → ℤ), ‖q‖ < ↑N - ↑M → UnitAddTorus.mFourierCoeff (torusFunction fun (x : Homogenization.Vec d) => ↑(lowProjection f M x) * ↑(g x)) q = 0

theorem AVenhance.Infra.Ergodic.HMinusOneErgodic.fastProduct_split_l2_bound {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 : HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(f x)) Cf r) {g : Homogenization.Vec d → ℝ} (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => |g x| ^ 2) MeasureTheory.volume) (hfast : IsFastPeriodic N g) (hNr : 2 ≤ r * ↑N) : (∫ (x : Homogenization.Vec d) in Torus.unitCell d, (lowProjection f (N / 2) x * g x) ^ 2) ^ (1 / 2) ≤ ((cellAverage fun (x : Homogenization.Vec d) => |f x| ^ 2) ^ (1 / 2) + 32 * ergodicFourierWeight d ^ (1 / 2) * Cf * Real.exp (-r * ↑N / 4096)) * (cellAverage fun (x : Homogenization.Vec d) => |g x| ^ 2) ^ (1 / 2) ∧ (∫ (x : Homogenization.Vec d) in Torus.unitCell d, (highRemainder f (N / 2) x * g x) ^ 2) ^ (1 / 2) ≤ (1024 * (↑d + 1) * Cf + 32 * ergodicFourierWeight d ^ (1 / 2) * Cf) * Real.exp (-r * ↑N / 4096) * (cellAverage fun (x : Homogenization.Vec d) => |g x| ^ 2) ^ (1 / 2)