Part I: regularity of the ansatz θTilde_m on the open half space

The open-time analogue of Energy/AnsatzRegularity: with T = T_{m-1} jointly C^∞ and HTilde_m jointly C² only on (0,∞) × ℝ², the ansatz θTilde_m = T + ∑_k ξ_{m,k} ΧTilde_{m,k}·(…) + HTilde_m is jointly C² on (0,∞) × ℝ². (The fixed-time statements ansatz_slice_contDiff and ansatz_periodic of Energy/AnsatzRegularity are pointwise in the time and are used as they stand for t > 0.)

theorem AVenhance.Infra.Section5.Integration.slice_contDiff_of_contDiffOn_Ioi {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (T t)

A function that is C^∞ on Ioi 0 ×ˢ univ is C^∞ on each slice at a positive time.

theorem AVenhance.Infra.Section5.Integration.transportedGrad_contDiffOn_Ioi {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => T p.1 (I.xFlow hΦ m l p.1 y)) (I.xFlowInv hΦ m l p.1 p.2) i) (Set.Ioi 0 ×ˢ Set.univ)

The transported gradient is jointly C^∞ on Ioi 0 ×ˢ univ whenever T is.

theorem AVenhance.Infra.Section5.Integration.ansatzSummand_contDiffOn_two_Ioi {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => ansatzSummand I hΦ m κm T k p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

Each summand is jointly C² on (0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.ansatz_series_contDiffOn_two_Ioi {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => ∑' (k : ℤ), ansatzSummand I hΦ m κm T k p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

Joint C² regularity of the ansatz series on (0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.ansatz_contDiffOn_two_Ioi {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hH : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κm T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => I.ansatz hΦ m κm T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

Joint C² regularity of the ansatz θTilde_m on (0,∞) × ℝ², given C^∞ regularity of the iterate T_{m-1} and C² regularity of HTilde_m on the open half space.