The finite-sum product rule for the material derivative of an ansatz.

def AVenhance.Infra.Section5.finiteAnsatzField {ι : Type u_1} (S : Finset ι) (T H : ℝ → Homogenization.Vec 2 → ℝ) (ξ : ι → ℝ → ℝ) (χ G : ι → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

A finite model for the corrector ansatz at a space-time point.

Equations

• AVenhance.Infra.Section5.finiteAnsatzField S T H ξ χ G t x = T t x + ∑ k ∈ S, ξ k t * Homogenization.vecDot (χ k t x) (G k t x) + H t x

theorem AVenhance.Infra.Section5.finiteAnsatz_material_expansion {ι : Type u_1} (S : Finset ι) (T H : ℝ → Homogenization.Vec 2 → ℝ) (ξ : ι → ℝ → ℝ) (χ G : ι → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x v : Homogenization.Vec 2) (Tt Ht : ℝ) (ξt : ι → ℝ) (χt Gt : ι → Homogenization.Vec 2) (LT LH : Homogenization.Vec 2 →L[ℝ] ℝ) (Lχ LG : ι → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (hTt : HasDerivAt (fun (s : ℝ) => T s x) Tt t) (hHt : HasDerivAt (fun (s : ℝ) => H s x) Ht t) (hξt : ∀ k ∈ S, HasDerivAt (ξ k) (ξt k) t) (hχt : ∀ k ∈ S, HasDerivAt (fun (s : ℝ) => χ k s x) (χt k) t) (hGt : ∀ k ∈ S, HasDerivAt (fun (s : ℝ) => G k s x) (Gt k) t) (hTx : HasFDerivAt (T t) LT x) (hHx : HasFDerivAt (H t) LH x) (hχx : ∀ k ∈ S, HasFDerivAt (χ k t) (Lχ k) x) (hGx : ∀ k ∈ S, HasFDerivAt (G k t) (LG k) x) : deriv (fun (s : ℝ) => finiteAnsatzField S T H ξ χ G s x) t + (fderiv ℝ (finiteAnsatzField S T H ξ χ G t) x) v = Tt + Ht + ∑ k ∈ S, (ξt k * Homogenization.vecDot (χ k t x) (G k t x) + ξ k t * (Homogenization.vecDot (χt k) (G k t x) + Homogenization.vecDot (χ k t x) (Gt k))) + (LT v + ∑ k ∈ S, ξ k t * (Homogenization.vecDot ((Lχ k) v) (G k t x) + Homogenization.vecDot (χ k t x) ((LG k) v)) + LH v)

Differentiate the finite corrector ansatz in time and along a spatial direction. This is the product-rule bridge used in e.timecomp.0; local finiteness of the cutoff sum is handled separately by ansatz_hasDerivAt.