Fixed-time spatial differentiation of the cutoff ansatz.
theorem
AVenhance.Infra.Section5.ansatz_spaceGrad
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(x : Homogenization.Vec 2)
{LT LH : Homogenization.Vec 2 →L[ℝ] ℝ}
(LP : ℤ → Homogenization.Vec 2 →L[ℝ] ℝ)
(hT : HasFDerivAt (T t) LT x)
(hH : HasFDerivAt (I.Hm hΦ m κm T t) LH x)
(hP :
∀ k ∈ ⋯.toFinset,
HasFDerivAt
(fun (y : Homogenization.Vec 2) =>
Homogenization.vecDot (I.chiTilde hΦ m κm k t y) (G I hΦ m T (lIdx β I.Λ m k) t y))
(LP k) x)
(i : Fin 2)
:
At a fixed time the ansatz series is exactly a finite sum over the
support of xiMK; the spatial gradient therefore follows from the ordinary
finite-sum product rule.
theorem
AVenhance.Infra.Section5.ansatz_spaceGrad_expanded
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(x : Homogenization.Vec 2)
{LT LH : Homogenization.Vec 2 →L[ℝ] ℝ}
(Lχ LG : ℤ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2)
(hT : HasFDerivAt (T t) LT x)
(hH : HasFDerivAt (I.Hm hΦ m κm T t) LH x)
(hχ : ∀ k ∈ ⋯.toFinset, HasFDerivAt (I.chiTilde hΦ m κm k t) (Lχ k) x)
(hG : ∀ k ∈ ⋯.toFinset, HasFDerivAt (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t y) (LG k) x)
(i : Fin 2)
:
spaceGrad (I.ansatz hΦ m κm T t) x i = spaceGrad (T t) x i + ∑ k ∈ ⋯.toFinset,
I.xiMK m k t * ((gradMatrix (I.chiTilde hΦ m κm k t) x).mulVec (G I hΦ m T (lIdx β I.Λ m k) t x) i + ∑ j : Fin 2,
I.chiTilde hΦ m κm k t x j * spaceGrad (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t y j) x i) + spaceGrad (I.Hm hΦ m κm T t) x i
Corrected line-2 spatial expansion of the ansatz. The finite sum
uses the selected flow l_k in both the corrector and the pulled gradient.