Joint continuity of the divergence-form terms on the open half space #
twistie3, normie1, normie2 and R46 are divergences of fluxes that are jointly C² on
(0,∞) × ℝ² (resp. a time-continuous matrix times a jointly smooth vector for R46), hence jointly
continuous there. Nothing is claimed at t ≤ 0: HTilde_m and Amnr use the two-sided time
derivative.
theorem
AVenhance.Infra.Section5.Contracts.twistie3_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) => twistie3 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section5.Contracts.normie1_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) => normie1 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section5.Contracts.normie2_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) => normie2 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section5.Contracts.R46_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) => R46 I hΦ m κm (T (Nstar β)) p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)