One centered ergodic component

The centered Appendix C estimate (centered_frozen_hMinusOneNorm_le_of_fastPeriodicProduct_flow, §8 (27)) specialised to a continuous fast factor with a uniform sup bound Gm.

noncomputable def AVenhance.Infra.Section5.Contracts.sdCd : ℝ

The absolute constant of the centered App C estimate (dimension two).

Equations

• AVenhance.Infra.Section5.Contracts.sdCd = 1 + 64 * AVenhance.Infra.Ergodic.ergodicFourierWeight 2 ^ (1 / 2) + 1024 * (2 + 1)

theorem AVenhance.Infra.Section5.Contracts.sdCd_pos : 0 < sdCd

theorem AVenhance.Infra.Section5.Contracts.sd_cellAverage_sq_sqrt_le {g : Homogenization.Vec 2 → ℝ} (hg : Continuous g) {Gm : ℝ} (hGm : ∀ (y : Homogenization.Vec 2), |g y| ≤ Gm) : (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |g x| ^ 2) ^ (1 / 2) ≤ Gm

theorem AVenhance.Infra.Section5.Contracts.sd_centerCell_eq (h : Homogenization.Vec 2 → ℝ) : Integration.centerCell h = Ergodic.centerCell h

The two centering operators (unit-cube integral versus torus average) agree.

theorem AVenhance.Infra.Section5.Contracts.sd_component_bound {N : ℕ} (hN : 0 < N) (X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2) {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : Ergodic.IsZPeriodic f) {Cf r Gm : ℝ} (hCf : 0 ≤ Cf) (hr : 0 < r) (hder : Ergodic.HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec 2) => ↑(f (X.toFun x))) Cf r) (hg : Continuous g) (hfast : Ergodic.IsFastPeriodic N g) (hNr : 2 ≤ r * ↑N) (hnear : Ergodic.FlowDerivativeNearIdentity X) (hgmean : Ergodic.cellAverage g = 0) (hGm : ∀ (y : Homogenization.Vec 2), |g y| ≤ Gm) : hMinusOneNorm (Integration.centerCell fun (x : Homogenization.Vec 2) => f x * g (X.invFun x)) ≤ ENNReal.ofReal (3 * 2 ^ 2 * (sdCd / ↑N * (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |f x| ^ 2) ^ (1 / 2) * Gm + sdCd * Cf * Gm * Real.exp (-r * ↑N / 4096)))

One component of the centered ergodic estimate, with the fast factor bounded by Gm.

theorem AVenhance.Infra.Section5.Contracts.sd_memL2On_of_continuous {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : Homogenization.MemL2On unitCube f

theorem AVenhance.Infra.Section5.Contracts.sd_centered_finset_sum_bound {ι : Type u_1} (s : Finset ι) (h : ι → Homogenization.Vec 2 → ℝ) (B : ι → ENNReal) (hc : ∀ i ∈ s, Continuous (h i)) (hb : ∀ i ∈ s, hMinusOneNorm (Integration.centerCell (h i)) ≤ B i) : hMinusOneNorm (Integration.centerCell fun (x : Homogenization.Vec 2) => ∑ i ∈ s, h i x) ≤ ∑ i ∈ s, B i

The centered HDot⁻¹ norm of a finite sum of continuous functions is at most the sum of the centered norms (centering and the sum commute; the homogeneous seminorm is subadditive).