Pointwise bounds for the remainder fields of e.grad.tildetheta.again

Componentwise (entrywise) bounds, valid at every point (t, x) with ξ_{m,k}(t) ≠ 0, for the sum E¹ + E² + E³ of the three remainder fields in terms of gT ≥ |∂_p T| and h_p ≥ |∂_i∂_p T|:

|(E¹ + E² + E³)_i| ≤ 20 e c gT + ε_m c (4 (h₀ + h₁) + 16 D gT),

with e = ε_{m-1}^{2δ}, c = a_m ε_m²/κ_m and D = 2^16 ε_{m-1}⁻¹. Source: enhance.tex 8146–8200 (the second through fourth displays after e.grad.tildetheta.again).

Elementary entry calculus on 2 × 2 matrices

theorem AVenhance.Infra.Section5.RelativeError.abs_mul_le_of_le {a b A B : ℝ} (ha : |a| ≤ A) (hb : |b| ≤ B) : |a * b| ≤ A * B

theorem AVenhance.Infra.Section5.RelativeError.abs_add_le_of_le {a b A B : ℝ} (ha : |a| ≤ A) (hb : |b| ≤ B) : |a + b| ≤ A + B

theorem AVenhance.Infra.Section5.RelativeError.abs_mulVec_le {M : Matrix (Fin 2) (Fin 2) ℝ} {μ gT : ℝ} {g : Homogenization.Vec 2} (hM : ∀ (i j : Fin 2), |M i j| ≤ μ) (hg : ∀ (j : Fin 2), |g j| ≤ gT) (i : Fin 2) : |M.mulVec g i| ≤ 2 * μ * gT

theorem AVenhance.Infra.Section5.RelativeError.abs_matMul_le {M N : Matrix (Fin 2) (Fin 2) ℝ} {μ ν : ℝ} (hM : ∀ (i j : Fin 2), |M i j| ≤ μ) (hN : ∀ (i j : Fin 2), |N i j| ≤ ν) (i j : Fin 2) : |(M * N) i j| ≤ 2 * μ * ν

theorem AVenhance.Infra.Section5.RelativeError.abs_le_two_of_sub_one {A : Matrix (Fin 2) (Fin 2) ℝ} {e : ℝ} (he1 : e ≤ 1) (hA : ∀ (i j : Fin 2), |(A - 1) i j| ≤ e) (i j : Fin 2) : |A i j| ≤ 2

theorem AVenhance.Infra.Section5.RelativeError.flowInv_flowFwd_component_le {A C Fl : Matrix (Fin 2) (Fin 2) ℝ} {e c gT : ℝ} {g : Homogenization.Vec 2} (he1 : e ≤ 1) (hA : ∀ (i j : Fin 2), |(A - 1) i j| ≤ e) (hC : ∀ (i j : Fin 2), |C i j| ≤ c) (hFl : ∀ (i j : Fin 2), |(Fl - 1) i j| ≤ e) (hg : ∀ (j : Fin 2), |g j| ≤ gT) (i : Fin 2) : |((A - 1) * C).mulVec g i| ≤ 4 * e * c * gT ∧ |(A * C * (Fl - 1)).mulVec g i| ≤ 16 * e * c * gT

Componentwise bounds for the second and third remainder fields.

theorem AVenhance.Infra.Section5.RelativeError.hessian_component_le {χ g : Homogenization.Vec 2} {Fl : Matrix (Fin 2) (Fin 2) ℝ} {a : Fin 2 → ℝ} {Dd : Fin 2 → Fin 2 → Fin 2 → ℝ} {Hs h : Fin 2 → ℝ} {cχ D gT : ℝ} (hχ : ∀ (j : Fin 2), |χ j| ≤ cχ) (hFl : ∀ (j p : Fin 2), |Fl j p| ≤ 2) (ha : ∀ (q : Fin 2), |a q| ≤ 2) (hD : ∀ (p j q : Fin 2), |Dd p j q| ≤ D) (hH : ∀ (p : Fin 2), |Hs p| ≤ h p) (hg : ∀ (p : Fin 2), |g p| ≤ gT) : |∑ j : Fin 2, χ j * ∑ p : Fin 2, (Fl j p * Hs p + (∑ q : Fin 2, a q * Dd p j q) * g p)| ≤ cχ * (4 * (h 0 + h 1) + 16 * D * gT)

Componentwise bound for the Hessian remainder field.

The second derivative of the flow

theorem AVenhance.Infra.Section5.RelativeError.fderiv_apply_const_eq {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (z v w : Homogenization.Vec 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) w) z) v = (iteratedFDeriv ℝ 2 f z) ![v, w]

theorem AVenhance.Infra.Section5.RelativeError.xFlowHess_eq_iteratedFDeriv {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (z : Homogenization.Vec 2) (p j q : Fin 2) : xFlowHess I hΦ m l t z p j q = (iteratedFDeriv ℝ 2 (fun (y : Homogenization.Vec 2) => I.xFlow hΦ m l t y p) z) ![Homogenization.basisVec q, Homogenization.basisVec j]

The second derivative xFlowHess as an iterated Fréchet derivative.

theorem AVenhance.Infra.Section5.RelativeError.abs_xFlowHess_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (z : Homogenization.Vec 2) (p j q : Fin 2) : |xFlowHess I hΦ m (lIdx β I.Λ m k) t z p j q| ≤ 2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹

Entry bound |∂_q∂_j X^p| ≤ 2^16 ε_{m-1}⁻¹ on supp ξ_{m,k}.