the open-time HTilde_m gradient from the AMNR tensor bound (actual iterates)

relative_Hm_gradient_actual is relative_Hm_gradient for the actual last iterate T N* of an IsTIterates family. The only analytic input is the AMNR tensor bound; all differentiability and measurability facts are proved from the joint C^∞ regularity of Amnr and HTilde_{m,r} on the open half space (0,∞) × ℝ², so nothing is assumed at t ≤ 0.

theorem AVenhance.Infra.Section5.RelativeError.differentiableAt_slice_of_contDiffOn_Ioi {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (F t) x

A function jointly C^∞ on the open half space is differentiable in space at each positive time.

theorem AVenhance.Infra.Section5.RelativeError.aestronglyMeasurable_timeCube_of_contDiffOn_Ioi {G : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hG : ContinuousOn G (Set.Ioi 0 ×ˢ Set.univ)) : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict timeCube)

A function jointly C^∞ on the open half space is a.e.-strongly measurable on the time cube.

theorem AVenhance.Infra.Section5.RelativeError.relative_Hm_gradient_actual (β 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 → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → ∀ (S : ℝ), 0 ≤ S → (∀ r₀ ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (Section4.amnrSpatialDivergenceGradientTensor I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) 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 (Nstar β)) s) x) ≤ CH * epsilon β I.Λ (m - 1) ^ (4 * delta β) * S

Open-time HTilde_m gradient bound for the actual iterates (16)-(18). The AMNR tensor bound is the only analytic input; all regularity and measurability premises of relative_Hm_gradient are discharged on the open half space.