Joint continuity of the six non-divergence §5.1 terms

For the actual iterates (I.IsTIterates), the terms cutoff1, twistie1, twistie4, twistie5, normie3 and tiny are jointly continuous on the open half space (0,∞) × ℝ². Open time only: HTilde_m and Amnr use the two-sided time derivative.

• TermContinuityPointwiseTools: locally finite sums, spatial gradients/divergences of jointly smooth fields, composition with the inverse flow;
• TermContinuityPointwiseFields: joint regularity of the building blocks;
• TermContinuityPointwiseTerms: cutoff1, twistie1, twistie4, twistie5, normie3 for a jointly smooth T;
• TermContinuityPointwiseTiny: tiny.

theorem AVenhance.Infra.Section5.Contracts.cutoff1_term_continuousOn {β : ℝ} (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) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => cutoff1 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

cutoff1 of the terminal iterate is jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.twistie1_term_continuousOn {β : ℝ} (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) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => twistie1 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

twistie1 of the terminal iterate is jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.twistie4_term_continuousOn {β : ℝ} (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) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => twistie4 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

twistie4 of the terminal iterate is jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.twistie5_term_continuousOn {β : ℝ} (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) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => twistie5 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

twistie5 of the terminal iterate is jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.normie3_term_continuousOn {β : ℝ} (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) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => normie3 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

normie3 of the terminal iterate is jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tiny_term_continuousOn {β : ℝ} (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) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => tiny I hΦ m κm (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

tiny (with the d_m and last-iterate error e_{m-1}) is jointly continuous on the open half space.