L²_{t,x} bound for the leading-gradient error in terms of the temperature norms #
Given the pointwise bound ansatz_error_component_le, the continuity of the gradient norms of
T, ∂_p T and HTilde_m on [0,∞) × ℝ² and the scalar L² triangle inequality, this module
proves
‖∇θTilde_m - F∇T‖_{L²} ≤ 2 (P ‖∇T‖ + Q (‖∇∂₀T‖ + ‖∇∂₁T‖) + ‖∇HTilde_m‖)
with P = 20 e c + ε_m c · 16 (2^16 ε_{m-1}⁻¹), Q = 4 ε_m c, e = ε_{m-1}^{2δ},
c = a_m ε_m²/κ_m.
theorem
AVenhance.Infra.Section5.RelativeError.continuousOn_spaceGrad_of_contDiffOn_two
{F : ℝ → Homogenization.Vec 2 → ℝ}
(hF : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ))
(i : Fin 2)
:
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (F p.1) p.2 i) (Set.Ioi 0 ×ˢ Set.univ)
Joint continuity of ∇_x F on (0,∞) × ℝ² for F of class C² there.
theorem
AVenhance.Infra.Section5.RelativeError.sqrt_leadingErr_le
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm : ℝ}
(hκ : 0 < κm)
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hTs : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (T t))
(hH2 : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κm T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ))
(hHs : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (I.Hm hΦ m κm T t))
:
√(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad (I.ansatz hΦ m κm T s) x - LeftToShow.leadingGrad I hΦ m κm T s x) ≤ 2 * ((20 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) + epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * (16 * (2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹))) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T s) x) + 4 * epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * √(spaceTimeGradNormSq fun (s : ℝ) => spaceGrad (Section4.iterateSpatialWord [0] (T s))) + 4 * epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * √(spaceTimeGradNormSq fun (s : ℝ) => spaceGrad (Section4.iterateSpatialWord [1] (T s))) + √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (I.Hm hΦ m κm T s) x))
The L²_{t,x} bound for the leading-gradient error in terms of the temperature norms.