Pointwise bound for the actual remainder fields #
Instantiates flowInv_flowFwd_component_le and hessian_component_le with the flow estimates
e.Xm.bound.1, e.Xm.bound.2 (LeadingErrorFlow) and the corrector bounds e.corrm.
theorem
AVenhance.Infra.Section5.RelativeError.epsilon_le_one'
{β : ℝ}
(I : Ingredients β)
(n : ℕ)
:
theorem
AVenhance.Infra.Section5.RelativeError.leadingErr_sum_component_le
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm : ℝ}
(hκ : 0 < κm)
(T : ℝ → Homogenization.Vec 2 → ℝ)
{t : ℝ}
(k : ℤ)
(hξ : I.xiMK m k t ≠ 0)
(x : Homogenization.Vec 2)
{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)
:
|(leadingErrFlowInv I hΦ m κm T k t x + leadingErrFlowFwd I hΦ m κm T k t x + leadingErrHessian I hΦ m κm T k 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)
Pointwise bound on the sum of the three remainder fields at (t, x) with ξ_{m,k}(t) ≠ 0.