Centered Appendix C estimates in the smooth-test norm. Only the fast factor is required to have zero mean; the actual product is centered explicitly.

theorem AVenhance.Infra.Section5.SlowFactorBoundsCentered.centered_avg_cube (f : Homogenization.Vec 2 → ℝ) : Ergodic.cellAverage f = ∫ (x : Homogenization.Vec 2) in unitCube, f x

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

theorem AVenhance.Infra.Section5.SlowFactorBoundsCentered.centered_product_L2 {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec 2) => |g x| ^ 2) MeasureTheory.volume) : Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => f x * g x

def AVenhance.Infra.Section5.SlowFactorBoundsCentered.centeredFlowHomeomorph (X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2) : Homogenization.Vec 2 ≃ₜ Homogenization.Vec 2

Homeomorphism underlying a periodic volume-preserving flow in the centered estimates.

Equations

• AVenhance.Infra.Section5.SlowFactorBoundsCentered.centeredFlowHomeomorph X = { toFun := X.toFun, invFun := X.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem AVenhance.Infra.Section5.SlowFactorBoundsCentered.centered_flow_local_integrable (X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2) {g : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec 2) => g (X.invFun x)) MeasureTheory.volume

theorem AVenhance.Infra.Section5.centered_hMinusOneNorm_eq_ergodic {h : Homogenization.Vec 2 → ℝ} (hL2 : Homogenization.MemL2On unitCube h) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) : hMinusOneNorm (Ergodic.centerCell h) = Ergodic.homogeneousHMinusOneNorm h

theorem AVenhance.Infra.Section5.centered_frozen_hMinusOneNorm_le_of_fastPeriodicProduct_flow {N : ℕ} (hN : 0 < N) (X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : Ergodic.IsZPeriodic f) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hderivComp : Ergodic.HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec 2) => ↑(f (X.toFun x))) Cf r) {g : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec 2) => |g x| ^ 2) MeasureTheory.volume) (hfast : Ergodic.IsFastPeriodic N g) (hNr : 2 ≤ r * ↑N) (hnear : Ergodic.FlowDerivativeNearIdentity X) (hgMean : Ergodic.cellAverage g = 0) : hMinusOneNorm (Ergodic.centerCell fun (x : Homogenization.Vec 2) => f x * g (X.invFun x)) ≤ ENNReal.ofReal (3 * 2 ^ 2 * ((1 + 64 * Ergodic.ergodicFourierWeight 2 ^ (1 / 2) + 1024 * (2 + 1)) / ↑N * (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |f x| ^ 2) ^ (1 / 2) * (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |g x| ^ 2) ^ (1 / 2) + (1 + 64 * Ergodic.ergodicFourierWeight 2 ^ (1 / 2) + 1024 * (2 + 1)) * Cf * (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |g x| ^ 2) ^ (1 / 2) * Real.exp (-r * ↑N / 4096)))

theorem AVenhance.Infra.Section5.frozen_hMinusOneNorm_sum_le_of_centered_bounds {ι : Type u_1} (s : Finset ι) (h : ι → Homogenization.Vec 2 → ℝ) (B : ι → ENNReal) (hL2 : ∀ i ∈ s, Homogenization.MemL2On unitCube (h i)) (hh : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (h i) MeasureTheory.volume) (hm : (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => ∑ i ∈ s, h i x) = 0) (hb : ∀ i ∈ s, hMinusOneNorm (Ergodic.centerCell (h i)) ≤ B i) : (hMinusOneNorm fun (x : Homogenization.Vec 2) => ∑ i ∈ s, h i x) ≤ ∑ i ∈ s, B i

Consumer repair: retain a separate proof of the actual total's zero mean. Component estimates are made on centered data, with no component-mean premise.