The S-normalised HTilde_m gradient bound from the AMNR tensor estimate

Equations (16)-(18). The tensor hypothesis is the scale form of equation (5), stated for each r₀ < Jcut β separately: CA · S · (ε_m²/κ_m)/√ν · L² · (τ'_m)^{-r₀} with L = ε_{m-1}^{-1-γ/2} and ν = κ_{m-1}, and is the literal hAmnrHess premise of hmr_spaceGrad_eLpNorm_le_of_pAmnr_qMNR. The conclusion is the hHgrad input shape of the leading-error assembly: √κ_m √(spaceTimeGradNormSq ∇HTilde_m) ≤ CH ε_{m-1}^{4δ} S.

theorem AVenhance.Infra.Section5.RelativeError.leh_epsilon_rpow_delta_le {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 1 ≤ m) (hbig : 4 ^ (1 / delta β) ≤ ↑Λ) : epsilon β Λ m ^ delta β ≤ 1 / 4

ε_{m-1}^δ ≤ 1/4 once Λ ≥ 4^{1/δ}.

theorem AVenhance.Infra.Section5.RelativeError.relative_Hm_gradient (β C₀ CA : ℝ) (hCA : 0 ≤ CA) : ∃ (CH : ℝ), 0 ≤ CH ∧ ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (T : ℝ → Homogenization.Vec 2 → ℝ) (S : ℝ), 0 ≤ S → (∀ r ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), ∀ (i j k p : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => Section4.amnrSpatialDivergenceGradientTensor I hΦ m (I.kappaSeq κ M m) T n r z i j k p) (MeasureTheory.volume.restrict timeCube)) → (∀ r ∈ Finset.range (Jcut β), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m (I.kappaSeq κ M m) T r z.1 x) z.2) (MeasureTheory.volume.restrict timeCube)) → (∀ r ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m (I.kappaSeq κ M m) n T r t y i j k) x) → (∀ r ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m (I.kappaSeq κ M m) n T r t x i j k) y i) x) → (∀ r ∈ Finset.range (Jcut β), ∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m (I.kappaSeq κ M m) T r t y) x) → (∀ r₀ ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (Section4.amnrSpatialDivergenceGradientTensor I hΦ m (I.kappaSeq κ M m) T n r₀) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (CA * S * (epsilon β I.Λ m ^ 2 / I.kappaSeq κ M m) / √(I.kappaSeq κ M (m - 1)) * (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ 2 * (tauP β I.Λ m)⁻¹ ^ r₀)) → √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (I.Hm hΦ m (I.kappaSeq κ M m) T s) x) ≤ CH * epsilon β I.Λ (m - 1) ^ (4 * delta β) * S

Gradient bound (16)-(18).