Joint regularity of the building blocks of the pointwise §5.1 terms

Each lemma is on the open half space tcU = (0,∞) × ℝ², componentwise. T is any field that is jointly C^∞ on [0,∞) × ℝ² (an actual iterate).

theorem AVenhance.Infra.Section5.Contracts.tc_G_contDiffOn {β : ℝ} (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.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => G I hΦ m T l p.1 p.2 i) tcU

The pulled gradient G_l is jointly C^∞ on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_gradG_contDiffOn {β : ℝ} (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.Ici 0 ×ˢ Set.univ)) (i j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => gradG I hΦ m T l p.1 p.2 i j) tcU

The spatial derivative matrix ∇G_l is jointly C^∞ on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_chiTilde_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (i : Fin 2) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => I.chiTilde hΦ m κm k p.1 p.2 i) tcU

The twisted corrector components are jointly C².

theorem AVenhance.Infra.Section5.Contracts.tc_flowGradK_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (i j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => flowGradK I hΦ m k p.1 p.2 i j) tcU

The flow gradient flowGradK is jointly C^∞.

theorem AVenhance.Infra.Section5.Contracts.tc_zetaMK_contDiff {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (I.zetaMK m k)

ζ_{m,k} is C^∞.

theorem AVenhance.Infra.Section5.Contracts.tc_psiCoeff_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => I.hatZetaML m (lIdx β I.Λ m k) p.1 * I.zetaMK m k p.1 * psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) p.1 p.2)) tcU

The scalar coefficient ζ̂_{m,l_k} ζ_{m,k} ψ_{m,k} ∘ X⁻¹ is jointly C^∞.

theorem AVenhance.Infra.Section5.Contracts.tc_gradChiMK_comp_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k l : ℤ) (i j : Fin 2) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k p.1 z) (I.xFlowInv hΦ m l p.1 p.2) i j) tcU

The matrix ∇Χ^κ_{m,k} evaluated at the inverse flow is jointly C¹.

theorem AVenhance.Infra.Section5.Contracts.tc_gradXInv_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (i a : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m l p.1 z) p.2 i a) tcU

The Jacobian of the inverse flow is jointly C^∞.