Selected diffusion flux decomposition on the odd-subtype support.

theorem AVenhance.Infra.Section5.frozen_ansatz_diffusion_flux_decomposition_odd_support {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (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) (hG : ∀ 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) (y : Homogenization.Vec 2) : (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.ansatz hΦ m κ T t) y) = ∑ q ∈ ⋯.toFinset, 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 ∈ ⋯.toFinset, I.xiMK m (↑q) t • G I hΦ m T (lIdx β I.Λ m ↑q) t y) + ∑ q ∈ ⋯.toFinset, 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)

Reindex the selected spatial-gradient decomposition from integer cutoff support to the finite odd-subtype support used by the named terms.