Divergence expansion for the four selected pieces of the ansatz flux.
theorem
AVenhance.Infra.Section5.selected_ansatz_diffusion_divergence
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κ : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(x : Homogenization.Vec 2)
(S : Finset { k : ℤ // Odd k })
(hxi : ∀ q ∈ S, I.xiMK m (↑q) t ≠ 0)
(hB :
∀ q ∈ S,
∀ (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 ∈ S,
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 ∈ S, 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 ∈ S, I.xiMK m (↑q) t • (diffusionMatrix I hΦ m κ t y).mulVec (chiGradG I hΦ m κ T (↑q) t y))
LC x)
(hH :
HasFDerivAt (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.Hm hΦ m κ T t) y))
LH x)
(hflux :
∀ (y : Homogenization.Vec 2),
(diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.ansatz hΦ m κ T t) y) = ∑ q ∈ S, I.xiMK m (↑q) t • (correctorFlux I hΦ m κ (↑q) t y).mulVec (G I hΦ m T (lIdx β I.Λ m ↑q) t y) + (diffusionMatrix I hΦ m κ t y).mulVec
(spaceGrad (T t) y - ∑ q ∈ S, I.xiMK m (↑q) t • G I hΦ m T (lIdx β I.Λ m ↑q) t y) + ∑ q ∈ S, I.xiMK m (↑q) t • (diffusionMatrix I hΦ m κ t y).mulVec (chiGradG I hΦ m κ T (↑q) t y) + (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.Hm hΦ m κ T t) y))
:
vecDiv (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.ansatz hΦ m κ T t) y)) x = ∑ q ∈ S,
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)) + vecDiv
(fun (y : Homogenization.Vec 2) =>
(diffusionMatrix I hΦ m κ t y).mulVec
(spaceGrad (T t) y - ∑ q ∈ S, I.xiMK m (↑q) t • G I hΦ m T (lIdx β I.Λ m ↑q) t y))
x + vecDiv
(fun (y : Homogenization.Vec 2) =>
∑ q ∈ S, I.xiMK m (↑q) t • (diffusionMatrix I hΦ m κ t y).mulVec (chiGradG I hΦ m κ T (↑q) t y))
x + vecDiv (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.Hm hΦ m κ T t) y)) x
If the pointwise selected-gradient decomposition holds, its divergence is the sum of the selected corrector flux divergence and the three remaining flux divergences. Regularity is stated only at the evaluation point.