The low-frequency gap and L2 splitting used in the centered extension. These finite spectral estimates do not require the product's mean to vanish.

@[instance_reducible]

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

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

Equations

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

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

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

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

theorem AVenhance.Infra.Ergodic.CenteredSpectralCore.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.CenteredSpectralCore.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.CenteredSpectralCore.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.CenteredSpectralCore.mFourierCoeff_zero_eq_integral_local {d : ℕ} (H : UnitAddTorus (Fin d) → ℂ) : UnitAddTorus.mFourierCoeff H 0 = ∫ (x : UnitAddTorus (Fin d)), H x

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