: spatial smoothness of the objects regrouped in Regroup.
At a fixed time every selected-mode object (selCoeff, flowGradK, B_k, D_k, E_k, G_k,
∇T) is C^∞ in space, given T t ∈ C^∞. These are consequences of the smoothness
lemmas of RelativeError.LeadingErrorAlgebraDefs; only ContDiff ℝ ∞ (T t) is assumed.
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_gradMatrix_entry
{f : Homogenization.Vec 2 → Homogenization.Vec 2}
(hf : ContDiff ℝ (↑⊤) f)
(i j : Fin 2)
:
ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => gradMatrix f x i j
Entries of the row-Jacobian of a smooth field are smooth.
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_selCoeff
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
:
ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => selCoeff I hΦ m k t y
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_flowGradK_entry
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(i j : Fin 2)
:
ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => flowGradK I hΦ m k t y i j
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_gradYEntry
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(i j : Fin 2)
:
ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => gradMatrix (I.xFlowInv hΦ m (lIdx β I.Λ m k) t) y i j
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_cellGradEntry
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(k : ℤ)
(t : ℝ)
(i j : Fin 2)
:
ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) =>
gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k t z) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t y) i j
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_defect_entry
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(k : ℤ)
(t : ℝ)
(i j : Fin 2)
:
ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => correctorDefectMatrix I hΦ m k t κm y i j
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_pushforward_entry
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(k : ℤ)
(t : ℝ)
(i j : Fin 2)
:
ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => correctorPushforwardMatrix I hΦ m k t κm y i j
theorem
AVenhance.Infra.Section5.LeftJacobian.contDiff_spaceGrad_T
{T : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hT : ContDiff ℝ (↑⊤) (T t))
:
ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => spaceGrad (T t) y