Pointwise bound for ∇θTilde_m - F ∇T_{m-1} #
Combines the exact decomposition ansatz_spaceGrad_sub_leadingGrad with the pointwise bound on the
three remainder fields: the partition of unity ∑_{k odd} ξ_{m,k} = 1 with 0 ≤ ξ ≤ 1 turns the
k-uniform bound into a bound for the weighted sum.
theorem
AVenhance.Infra.Section5.RelativeError.xiMK_nonneg'
{β : ℝ}
(I : Ingredients β)
(m : ℕ)
(k : ℤ)
(t : ℝ)
:
theorem
AVenhance.Infra.Section5.RelativeError.ansatz_error_sub_Hm_component_le
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm : ℝ}
(hκ : 0 < κm)
{T : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hTt : ContDiff ℝ (↑⊤) (T t))
(x : Homogenization.Vec 2)
(hHt : DifferentiableAt ℝ (I.Hm hΦ m κm T t) x)
{gT : ℝ}
{h : Fin 2 → ℝ}
(hg : ∀ (p : Fin 2), |spaceGrad (T t) x p| ≤ gT)
(hh : ∀ (i p : Fin 2), |spaceHess (T t) x i p| ≤ h p)
(i : Fin 2)
:
|(spaceGrad (I.ansatz hΦ m κm T t) x - LeftToShow.leadingGrad I hΦ m κm T t x - spaceGrad (I.Hm hΦ m κm T t) x) i| ≤ 20 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * gT + epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * (4 * (h 0 + h 1) + 16 * (2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹) * gT)
The componentwise bound on the leading-gradient error with the ∇HTilde_m part removed, at
(t, x), t ≥ 0.
theorem
AVenhance.Infra.Section5.RelativeError.ansatz_error_component_le
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm : ℝ}
(hκ : 0 < κm)
{T : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hTt : ContDiff ℝ (↑⊤) (T t))
(x : Homogenization.Vec 2)
(hHt : DifferentiableAt ℝ (I.Hm hΦ m κm T t) x)
{gT : ℝ}
{h : Fin 2 → ℝ}
(hg : ∀ (p : Fin 2), |spaceGrad (T t) x p| ≤ gT)
(hh : ∀ (i p : Fin 2), |spaceHess (T t) x i p| ≤ h p)
(i : Fin 2)
:
|(spaceGrad (I.ansatz hΦ m κm T t) x - LeftToShow.leadingGrad I hΦ m κm T t x) i| ≤ 20 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * gT + epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * (4 * (h 0 + h 1) + 16 * (2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹) * gT) + |spaceGrad (I.Hm hΦ m κm T t) x i|
The componentwise bound on the leading-gradient error at (t, x), t ≥ 0.