Part I: continuous extension of the actual HTilde_m and of ∇(ansatz) to t ≥ 0

The actual HTilde_m (built from the two-sided Amnr recursion) is jointly C^∞ on the open half space. Its one-sided version Hhat, built from amnrWithin, is jointly C^∞ on the closed half space and equals HTilde_m at every positive time. Consequently ∇ θTilde_m has a continuous extension to [0,∞) × ℝ². Nothing is assumed about Amnr, Hm or the ansatz at t ≤ 0.

theorem AVenhance.Infra.Section5.Integration.Hm_extends_Ici {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) : ∃ (Hhat : ℝ × Homogenization.Vec 2 → ℝ), ContDiffOn ℝ (↑⊤) Hhat (Set.Ici 0 ×ˢ Set.univ) ∧ ∀ p ∈ Set.Ioi 0 ×ˢ Set.univ, I.Hm hΦ m κm (T (Nstar β)) p.1 p.2 = Hhat p

HTilde_m extends to a jointly C^∞ function on [0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.ansatz_spaceGrad_extends_Ici {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) : ∃ (G : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2), ContinuousOn G (Set.Ici 0 ×ˢ Set.univ) ∧ ∀ p ∈ Set.Ioi 0 ×ˢ Set.univ, spaceGrad (I.ansatz hΦ m κm (T (Nstar β)) p.1) p.2 = G p

∇(θTilde_m) extends continuously to [0,∞) × ℝ².