Finite-support assembly of the selected per-corrector flux divergences.

theorem AVenhance.Infra.Section5.selected_corrector_flux_sum_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) {LB : { k : ℤ // Odd k } → Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} {LG : { k : ℤ // Odd k } → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hB : ∀ q ∈ S, ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => correctorFlux I hΦ m κ (↑q) t y i j) (LB q i j) x) (hG : ∀ q ∈ S, HasFDerivAt (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m ↑q) t y) (LG q) x) : vecDiv (fun (y : Homogenization.Vec 2) => ∑ 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)) 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))

Pass a finite selected sum of corrector fluxes through divergence and apply the per-index expansion.