The selected diffusion divergence written in the named Section 5.1 terms.
theorem
AVenhance.Infra.Section5.frozen_ansatz_diffusion_named_expansion
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κ : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(x : Homogenization.Vec 2)
(hT : ∀ (y : Homogenization.Vec 2), HasFDerivAt (T t) (fderiv ℝ (T t) y) y)
(hH : ∀ (y : Homogenization.Vec 2), HasFDerivAt (I.Hm hΦ m κ T t) (fderiv ℝ (I.Hm hΦ m κ T t) y) y)
(hχ :
∀ k ∈ ⋯.toFinset,
∀ (y : Homogenization.Vec 2), HasFDerivAt (I.chiTilde hΦ m κ k t) (fderiv ℝ (I.chiTilde hΦ m κ k t) y) y)
(hGglobal :
∀ k ∈ ⋯.toFinset,
∀ (y : Homogenization.Vec 2),
HasFDerivAt (fun (z : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t z)
(fderiv ℝ (fun (z : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t z) y) y)
(hB :
∀ q ∈ ⋯.toFinset,
∀ (i j : Fin 2),
HasFDerivAt (fun (y : Homogenization.Vec 2) => correctorFlux I hΦ m κ (↑q) t y i j)
(fderiv ℝ (fun (y : Homogenization.Vec 2) => correctorFlux I hΦ m κ (↑q) t y i j) x) x)
(hG :
∀ q ∈ ⋯.toFinset,
HasFDerivAt (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m ↑q) t y)
(fderiv ℝ (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m ↑q) t y) x) x)
{LM LC LH : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2}
(hM :
HasFDerivAt
(fun (y : Homogenization.Vec 2) =>
(diffusionMatrix I hΦ m κ t y).mulVec
(spaceGrad (T t) y - ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t • G I hΦ m T (lIdx β I.Λ m ↑q) t y))
LM x)
(hC :
HasFDerivAt
(fun (y : Homogenization.Vec 2) =>
∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t • (diffusionMatrix I hΦ m κ t y).mulVec (chiGradG I hΦ m κ T (↑q) t y))
LC x)
(hHflux :
HasFDerivAt (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.Hm hΦ m κ T t) y))
LH x)
:
vecDiv (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.ansatz hΦ m κ T t) y)) x = ∑ q ∈ ⋯.toFinset,
I.xiMK m (↑q) t * (Homogenization.vecDot (matDiv (correctorDefectMatrix I hΦ m (↑q) t κ) x)
(G I hΦ m T (lIdx β I.Λ m ↑q) t x) + Homogenization.vecDot (matDiv (correctorPushforwardMatrix I hΦ m (↑q) t κ) x)
(G I hΦ m T (lIdx β I.Λ m ↑q) t x) + frob (correctorFlux I hΦ m κ (↑q) t x) (gradMatrix (G I hΦ m T (lIdx β I.Λ m ↑q) t) x) + Homogenization.vecDot
(fun (j : Fin 2) =>
deriv (fun (s : ℝ) => I.chiMK κ m (↑q) s (I.xFlowInv hΦ m (lIdx β I.Λ m ↑q) t x) j) t)
(G I hΦ m T (lIdx β I.Λ m ↑q) t x)) - twistie3 I hΦ m κ T t x - normie1 I hΦ m κ T t x - normie2 I hΦ m κ T t x
Expand the ansatz diffusion divergence into the selected
corrector contributions and the named mismatch, chi-gradient, and H_m
terms. The differentiability assumptions are local product-rule inputs.