Per-time centered bound for normie3 #
normie3 = Σ_k Σ_{p,j} n3Fast_{kpj}(Y_k x) · n3Slow_{kpj}(x) is a locally finite sum of fast-slow
products with mean-zero fast factors, so the generic centered ergodic bound
sd_nd_centered_bound applies directly (there is no divergence part). The fast factors are
bounded by G = 4ψ(1 + ψ/κ), ψ = a_m ε_m².
theorem
AVenhance.Infra.Section5.Contracts.n3_time_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm : ℝ}
(hκm : 0 < κm)
(T : ℝ → Homogenization.Vec 2 → ℝ)
{t : ℝ}
(hTt : ContDiff ℝ (↑⊤) (T t))
(hTp : IsZ2Periodic (T t))
{Cf r k₀ k₁ : ℝ}
(hk₀ : 0 ≤ k₀)
(hk₁ : 0 ≤ k₁)
{V₀ V₁ V₂ : Homogenization.Vec 2 → Homogenization.Vec 2}
(h₀ : Continuous V₀)
(h₁ : Continuous V₁)
(h₂ : Continuous V₂)
(hpt :
∀ (k : ℤ) (p j : Fin 2) (x : Homogenization.Vec 2),
n3Slow I hΦ m T k t p j x ^ 2 ≤ k₀ ^ 2 * Homogenization.vecNormSq (V₀ x) + k₁ ^ 2 * (Homogenization.vecNormSq (V₁ x) + Homogenization.vecNormSq (V₂ x)))
(hCf : 0 ≤ Cf)
(hr : 0 < r)
(hder :
∀ (k : { k : ℤ // Odd k }),
I.xiMK m (↑k) t ≠ 0 →
∀ (p j : Fin 2),
Ergodic.HasCoordinateAnalyticL2Bounds
(fun (x : Homogenization.Vec 2) => ↑(n3Slow I hΦ m T (↑k) t p 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))
(hNr : 2 ≤ r * ↑(ergodicFrequency β I.Λ m))
:
hMinusOneNorm (Integration.centerCell (normie3 I hΦ m κm T t)) ≤ ENNReal.ofReal
(144 * (sdCd / ↑(ergodicFrequency β I.Λ m)) * (4 * (a β I.Λ m * epsilon β I.Λ m ^ 2) * (1 + a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * k₀ * √(gradNormSq V₀) + 144 * (sdCd / ↑(ergodicFrequency β I.Λ m)) * (4 * (a β I.Λ m * epsilon β I.Λ m ^ 2) * (1 + a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * k₁ * √(gradNormSq V₁) + 144 * (sdCd / ↑(ergodicFrequency β I.Λ m)) * (4 * (a β I.Λ m * epsilon β I.Λ m ^ 2) * (1 + a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * k₁ * √(gradNormSq V₂) + 144 * sdCd * Cf * (4 * (a β I.Λ m * epsilon β I.Λ m ^ 2) * (1 + a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * Real.exp (-r * ↑(ergodicFrequency β I.Λ m) / 4096))
Per-time centered bound of normie3.