Per-time centered bounds for twistie4, twistie5 #
In the corrected form, both slots are pure divergences of smooth periodic fluxes
(twistie4_eq_neg_div_flux),
so the centered HDot⁻¹ bound is flux-only. The bounds for the earlier bodies twistie4ND,
twistie5ND are kept as sd_tw4ND_time_bound, sd_tw5ND_time_bound.
theorem
AVenhance.Infra.Section5.Contracts.sd_assemble_time_bound
{Nd1 cf g₀ g₁ g₂ k₀ k₁ E2 Q : ℝ}
(hk₀ : 0 ≤ k₀)
(hk₁ : 0 ≤ k₁)
(h₀ : 0 ≤ g₀)
(h₁ : 0 ≤ g₁)
(h₂ : 0 ≤ g₂)
(hNd1 : 0 ≤ Nd1)
(hE2 : 0 ≤ E2)
(hQ : Q ≤ cf * √g₀)
(hQ0 : 0 ≤ Q)
:
Common real-variable assembly: nondivergence bound + flux bound, with the square root of the three slice energies split into a sum of square roots.
theorem
AVenhance.Infra.Section5.Contracts.sd_tw4_time_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
{t : ℝ}
(hTt : ContDiff ℝ (↑⊤) (T t))
(hTp : IsZ2Periodic (T t))
{cf : ℝ}
{V₀ : Homogenization.Vec 2 → Homogenization.Vec 2}
(h₀ : Continuous V₀)
(hflux :
∀ (x : Homogenization.Vec 2),
Homogenization.vecNormSq (twistie4Flux I hΦ m κm T t x) ≤ cf ^ 2 * Homogenization.vecNormSq (V₀ x))
:
hMinusOneNorm (Integration.centerCell (twistie4 I hΦ m κm T t)) ≤ ENNReal.ofReal (|cf| * √(gradNormSq V₀))
Per-time centered bound for twistie4 (corrected form): twistie4 = -div (flux) is a pure
divergence, so its centered HDot⁻¹ norm is at most the L² norm of the flux.
theorem
AVenhance.Infra.Section5.Contracts.sd_tw5_time_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
{t : ℝ}
(hTt : ContDiff ℝ (↑⊤) (T t))
(hTp : IsZ2Periodic (T t))
{cf : ℝ}
{V₀ : Homogenization.Vec 2 → Homogenization.Vec 2}
(h₀ : Continuous V₀)
(hflux :
∀ (x : Homogenization.Vec 2),
Homogenization.vecNormSq (twistie5Flux I hΦ m κm T t x) ≤ cf ^ 2 * Homogenization.vecNormSq (V₀ x))
:
hMinusOneNorm (Integration.centerCell (twistie5 I hΦ m κm T t)) ≤ ENNReal.ofReal (|cf| * √(gradNormSq V₀))
Per-time centered bound for twistie5 (corrected form): twistie5 = -div (flux).
theorem
AVenhance.Infra.Section5.Contracts.sd_tw4ND_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₁ cf : ℝ}
(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 : ℤ) (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)))
(hflux :
∀ (x : Homogenization.Vec 2),
Homogenization.vecNormSq (twistie4Flux I hΦ m κm T t x) ≤ cf ^ 2 * 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)) * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * k₀ + |cf|) * √(gradNormSq V₀) + 144 * (sdCd / ↑(ergodicFrequency β I.Λ m)) * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * k₁ * √(gradNormSq V₁) + 144 * (sdCd / ↑(ergodicFrequency β I.Λ m)) * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * k₁ * √(gradNormSq V₂) + 144 * sdCd * Cf * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * Real.exp (-r * ↑(ergodicFrequency β I.Λ m) / 4096))
Per-time centered bound for the earlier body twistie4ND (nondivergence part by the ergodic
lemma, divergence part by its flux). Kept for reference.
theorem
AVenhance.Infra.Section5.Contracts.sd_tw5ND_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₁ cf : ℝ}
(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 : ℤ) (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)))
(hflux :
∀ (x : Homogenization.Vec 2),
Homogenization.vecNormSq (twistie5Flux I hΦ m κm T t x) ≤ cf ^ 2 * 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)) * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2)) * k₀ + |cf|) * √(gradNormSq V₀) + 144 * (sdCd / ↑(ergodicFrequency β I.Λ m)) * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2)) * k₁ * √(gradNormSq V₁) + 144 * (sdCd / ↑(ergodicFrequency β I.Λ m)) * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2)) * k₁ * √(gradNormSq V₂) + 144 * sdCd * Cf * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2)) * Real.exp (-r * ↑(ergodicFrequency β I.Λ m) / 4096))
Per-time centered bound for the earlier body twistie5ND (choice 3). Kept for reference.