Spatial regularity of the averaged coefficient sMat.
theorem
AVenhance.Infra.Section5.sMat_spatial_contDiff
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κm t : ℝ)
{n : WithTop ℕ∞}
(hflow : ∀ (l : ℤ), ContDiff ℝ n fun (x : Homogenization.Vec 2) => I.flowGrad hΦ m l t x)
:
ContDiff ℝ n fun (x : Homogenization.Vec 2) => I.sMat hΦ m κm t x
Finite support of hatXiML transfers spatial regularity of the pulled
flow Jacobians to their averaged matrix field.
theorem
AVenhance.Infra.Section5.sMat_spatial_contDiff_one
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κm t : ℝ)
:
ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => I.sMat hΦ m κm t x
theorem
AVenhance.Infra.Section5.sMat_spatial_contDiff_two
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κm t : ℝ)
:
ContDiff ℝ 2 fun (x : Homogenization.Vec 2) => I.sMat hΦ m κm t x