Part I: HTilde_m is jointly C^∞ on the open half space

HTilde_{m,r} = ∇ · ∑ 𝐀_{m,n,r} 𝐪_{m,n,r+1} and HTilde_m = ∑_{r < Jcut} HTilde_{m,r}. On the open set (0,∞) × ℝ² the spatial gradient of a jointly C^∞ function is jointly C^∞, so HTilde_m is jointly C^∞ there and every positive-time slice is C^∞.

theorem AVenhance.Infra.Section5.Integration.contDiffOn_spaceGrad_slice_Ioi {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (F p.1) p.2 j) (Set.Ioi 0 ×ˢ Set.univ)

On the open half space the spatial gradient components of a jointly C^∞ function are jointly C^∞.

theorem AVenhance.Infra.Section5.Integration.Hmr_contDiffOn_Ioi_top {β : ℝ} (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) (r : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => I.Hmr hΦ m κm (T (Nstar β)) r z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)

Each HTilde_{m,r} is jointly C^∞ on the open half space.

theorem AVenhance.Infra.Section5.Integration.Hm_contDiffOn_Ioi_top {β : ℝ} (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) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κm (T (Nstar β)) z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)

HTilde_m is jointly C^∞ on the open half space (0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.Hm_slice_contDiff_pos {β : ℝ} (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) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (I.Hm hΦ m κm (T (Nstar β)) t)

Every positive-time slice of HTilde_m is C^∞ in space.