Joint continuity of tiny for the actual iterates

tiny = ∇·(d + e) + ∑_k ξ_{m,k} ΧTilde_{m,k} · (∇X ∘ X⁻¹) ∇(∇·e), with d = sourceErrorD and e = iterateError. In the corrected form, d = Σ_l ξ̂_l F_lᵀ (JHat - 𝒥) F_l ∇T + tail. The coefficient JHat_m - 𝒥_m of d is only continuous in time, so the divergence of d + e is computed by differentiating under the (spatially constant) matrix: the first summand is Σ_{a,b} (JHat - 𝒥)_{ab} w_{abi} with the jointly smooth w_{abi} = Σ_l ξ̂_l (F_l)_{ai} (F_l ∇T)_b (tcPulled).

theorem AVenhance.Infra.Section5.Contracts.tc_slice_differentiableAt {F : ℝ → Homogenization.Vec 2 → ℝ} {n : WithTop ℕ∞} (hn : n ≠ 0) (hF : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) tcU) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (F t) x

Slices of a jointly differentiable field on the open half space are differentiable.

noncomputable def AVenhance.Infra.Section5.Contracts.tcPulled {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (a b i : Fin 2) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The scalar field w_{abi} = ∑_l ξ̂_{m,l} (F_l)_{ai} (F_l ∇T)_b (with F_l = ∇X_l ∘ X_l⁻¹), the part of the first summand of d_m that does not involve the time-only matrix JHat - 𝒥.

Equations

• AVenhance.Infra.Section5.Contracts.tcPulled I hΦ m T a b i t x = ∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t x a i * (I.flowGrad hΦ m l t x).mulVec (AVenhance.spaceGrad (T t) x) b)

noncomputable def AVenhance.Infra.Section5.Contracts.tcAmnrTail {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The terminal A_{m,n,Jcut} q_{m,n,Jcut} tail of d_m.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Contracts.tc_sourceErrorD_apply {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : sourceErrorD I hΦ m κm T t x i = ∑ a : Fin 2, ∑ b : Fin 2, (I.Jhat κm m t - I.flux κm m t) a b * tcPulled I hΦ m T a b i t x + tcAmnrTail I hΦ m κm T t x i

Coordinates of d_m: ∑_{a,b} (JHat - 𝒥)_{ab} w_{abi} + tail_i.

theorem AVenhance.Infra.Section5.Contracts.tc_pulled_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (a b i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => tcPulled I hΦ m T a b i p.1 p.2) tcU

The w_{abi} field is jointly C^∞ on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_amnrTail_contDiffOn {β : ℝ} (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) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => tcAmnrTail I hΦ m κm (T (Nstar β)) p.1 p.2 i) tcU

The terminal tail of d_m is jointly C^∞ on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_iterateError_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (κprev : ℝ) {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT0 : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T (Nstar β - 1) p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hT1 : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T (Nstar β) p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => iterateError I hΦ m κm κprev T p.1 p.2 i) tcU

The last-iterate error is jointly C^∞ on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_vecDiv_pulled_add (M : Matrix (Fin 2) (Fin 2) ℝ) {w : Fin 2 → Fin 2 → Fin 2 → Homogenization.Vec 2 → ℝ} {a e : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hw : ∀ (p q i : Fin 2), DifferentiableAt ℝ (w p q i) x) (ha : ∀ (i : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => a y i) x) (he : ∀ (i : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => e y i) x) : vecDiv (fun (y : Homogenization.Vec 2) (i : Fin 2) => ∑ p : Fin 2, ∑ q : Fin 2, M p q * w p q i y + a y i + e y i) x = ∑ i : Fin 2, (∑ p : Fin 2, ∑ q : Fin 2, M p q * spaceGrad (w p q i) x i + spaceGrad (fun (y : Homogenization.Vec 2) => a y i) x i + spaceGrad (fun (y : Homogenization.Vec 2) => e y i) x i)

Divergence of ∑_{p,q} M_{pq} w_{pqi} + a_i + e_i with M constant in space (product rule in coordinates).

theorem AVenhance.Infra.Section5.Contracts.tc_vecDiv_sourceErrorD_add_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) {e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (he : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => e p.1 p.2 i) tcU) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => vecDiv (fun (y : Homogenization.Vec 2) => sourceErrorD I hΦ m κm (T (Nstar β)) p.1 y + e p.1 y) p.2) tcU

The divergence of d_m + e for a jointly smooth e is jointly continuous on the open half space: d_m has the time-only (merely continuous) coefficient JHat - 𝒥, so the divergence is computed by differentiating under it.

theorem AVenhance.Infra.Section5.Contracts.tc_vecDiv_sourceErrorD_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) => vecDiv (sourceErrorD I hΦ m κm (T (Nstar β)) p.1) p.2) tcU

The divergence of d_m is jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_sourceErrorD_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) (i : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => sourceErrorD I hΦ m κm (T (Nstar β)) p.1 p.2 i) tcU

d_m is jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_tiny_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) tcU

tiny for the actual iterates is jointly continuous on the open half space.