Generic centered ergodic bound for a locally finite sum of fast-slow products #
At a fixed time t, a nondivergence part Nd = Σ_{k,a,j} (fast_{kaj} ∘ X_k⁻¹) · slow_{kaj} with
at most three active odd k and four components (a,j) has centered HDot⁻¹ norm at most
144 · Cd · (Gm/N · ‖slow‖ + Cf Gm e^{-rN/4096}): Minkowski over the at most twelve components and
the centered App C flow estimate (sd_component_bound) for each.
theorem
AVenhance.Infra.Section5.Contracts.sd_nd_centered_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(t : ℝ)
(fast slow : { k : ℤ // Odd k } → Fin 2 → Fin 2 → Homogenization.Vec 2 → ℝ)
(Nd : Homogenization.Vec 2 → ℝ)
(hNd :
∀ (S : Finset { k : ℤ // Odd k }),
(∀ (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ≠ 0 → k ∈ S) →
∀ (x : Homogenization.Vec 2),
Nd x = ∑ k ∈ S, ∑ a : Fin 2, ∑ j : Fin 2, fast k a j (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x) * slow k a j x)
(hzero :
∀ (k : { k : ℤ // Odd k }) (a j : Fin 2), I.xiMK m (↑k) t = 0 → slow k a j = fun (x : Homogenization.Vec 2) => 0)
(hslow : ∀ (k : { k : ℤ // Odd k }) (a j : Fin 2), ContDiff ℝ (↑⊤) (slow k a j) ∧ Ergodic.IsZPeriodic (slow k a j))
(hfast_c : ∀ (k : { k : ℤ // Odd k }) (a j : Fin 2), Continuous (fast k a j))
(hfast_p : ∀ (k : { k : ℤ // Odd k }) (a j : Fin 2), Ergodic.IsFastPeriodic (ergodicFrequency β I.Λ m) (fast k a j))
(hfast_m : ∀ (k : { k : ℤ // Odd k }) (a j : Fin 2), Ergodic.cellAverage (fast k a j) = 0)
{Gm Cf r F2sq : ℝ}
(hGm : ∀ (k : { k : ℤ // Odd k }) (a j : Fin 2) (y : Homogenization.Vec 2), |fast k a j y| ≤ Gm)
(hder :
∀ (k : { k : ℤ // Odd k }) (a j : Fin 2),
I.xiMK m (↑k) t ≠ 0 →
Ergodic.HasCoordinateAnalyticL2Bounds
(fun (x : Homogenization.Vec 2) => ↑(slow k a j (I.xFlow hΦ m (lIdx β I.Λ m ↑k) t x))) Cf r)
(hnear :
∀ (k : { k : ℤ // Odd k }),
I.xiMK m (↑k) t ≠ 0 → Ergodic.FlowDerivativeNearIdentity (LeftToShow.xFlowDiffeo I hΦ m (lIdx β I.Λ m ↑k) t))
(hCf : 0 ≤ Cf)
(hr : 0 < r)
(hNpos : 0 < ergodicFrequency β I.Λ m)
(hNr : 2 ≤ r * ↑(ergodicFrequency β I.Λ m))
(hF2 :
∀ (k : { k : ℤ // Odd k }) (a j : Fin 2),
I.xiMK m (↑k) t ≠ 0 → (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |slow k a j x| ^ 2) ≤ F2sq)
:
hMinusOneNorm (Integration.centerCell Nd) ≤ ENNReal.ofReal
(144 * (sdCd / ↑(ergodicFrequency β I.Λ m) * √F2sq * Gm + sdCd * Cf * Gm * Real.exp (-r * ↑(ergodicFrequency β I.Λ m) / 4096)))
Generic nondivergence bound.