Per-time centered bounds for the nondivergence parts #
theorem
AVenhance.Infra.Section5.Contracts.sd_cellAverage_sq_le
{f : Homogenization.Vec 2 → ℝ}
(hf : Continuous f)
{V₀ V₁ V₂ : Homogenization.Vec 2 → Homogenization.Vec 2}
(h₀ : Continuous V₀)
(h₁ : Continuous V₁)
(h₂ : Continuous V₂)
{k₀ k₁ : ℝ}
(hpt :
∀ (x : Homogenization.Vec 2),
f x ^ 2 ≤ k₀ ^ 2 * Homogenization.vecNormSq (V₀ x) + k₁ ^ 2 * (Homogenization.vecNormSq (V₁ x) + Homogenization.vecNormSq (V₂ x)))
:
(Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |f x| ^ 2) ≤ k₀ ^ 2 * gradNormSq V₀ + k₁ ^ 2 * (gradNormSq V₁ + gradNormSq V₂)
theorem
AVenhance.Infra.Section5.Contracts.section5SlowChoice2_zero
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κ : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(k : ℤ)
(t : ℝ)
(a j : Fin 2)
(h : I.xiMK m k t = 0)
:
theorem
AVenhance.Infra.Section5.Contracts.section5SlowChoice3_zero
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(k : ℤ)
(t : ℝ)
(a j : Fin 2)
(h : I.xiMK m k t = 0)
:
theorem
AVenhance.Infra.Section5.Contracts.sd_nd4_centered_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₁ : ℝ}
{V₀ V₁ V₂ : Homogenization.Vec 2 → Homogenization.Vec 2}
(h₀ : Continuous V₀)
(h₁ : Continuous V₁)
(h₂ : Continuous V₂)
(hpt :
∀ (k : ℤ) (a j : Fin 2) (x : Homogenization.Vec 2),
section5SlowChoice2 I hΦ m κm T k t a 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 →
∀ (a j : Fin 2),
Ergodic.HasCoordinateAnalyticL2Bounds
(fun (x : Homogenization.Vec 2) =>
↑(section5SlowChoice2 I hΦ m κm T (↑k) t 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))
(hNr : 2 ≤ r * ↑(ergodicFrequency β I.Λ m))
:
hMinusOneNorm (Integration.centerCell (twistie4Nd I hΦ m κm T t)) ≤ ENNReal.ofReal
(144 * (sdCd / ↑(ergodicFrequency β I.Λ m) * √(k₀ ^ 2 * gradNormSq V₀ + k₁ ^ 2 * (gradNormSq V₁ + gradNormSq V₂)) * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) + sdCd * Cf * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * Real.exp (-r * ↑(ergodicFrequency β I.Λ m) / 4096)))
Centered bound of the nondivergence part of twistie4 at a fixed time
(e.monster.est.8b).
theorem
AVenhance.Infra.Section5.Contracts.sd_nd5_centered_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₁ : ℝ}
{V₀ V₁ V₂ : Homogenization.Vec 2 → Homogenization.Vec 2}
(h₀ : Continuous V₀)
(h₁ : Continuous V₁)
(h₂ : Continuous V₂)
(hpt :
∀ (k : ℤ) (a j : Fin 2) (x : Homogenization.Vec 2),
section5SlowChoice3 I hΦ m T k t a 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 →
∀ (a j : Fin 2),
Ergodic.HasCoordinateAnalyticL2Bounds
(fun (x : Homogenization.Vec 2) =>
↑(section5SlowChoice3 I hΦ m T (↑k) t 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))
(hNr : 2 ≤ r * ↑(ergodicFrequency β I.Λ m))
:
hMinusOneNorm (Integration.centerCell (twistie5Nd I hΦ m κm T t)) ≤ ENNReal.ofReal
(144 * (sdCd / ↑(ergodicFrequency β I.Λ m) * √(k₀ ^ 2 * gradNormSq V₀ + k₁ ^ 2 * (gradNormSq V₁ + gradNormSq V₂)) * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2)) + sdCd * Cf * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2)) * Real.exp (-r * ↑(ergodicFrequency β I.Λ m) / 4096)))
Centered bound of the nondivergence part of twistie5 at a fixed time (choice 3).