The corrector divergence expansion paired with a selected pulled gradient.

theorem AVenhance.Infra.Section5.correctorFlux_mulVec_G_divergence_expansion {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hk : Odd k) (hxi : I.xiMK m k t ≠ 0) {LB : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} {LG : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hB : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => correctorFlux I hΦ m κ k t y i j) (LB i j) x) (hG : HasFDerivAt (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t y) LG x) : vecDiv (fun (y : Homogenization.Vec 2) => (correctorFlux I hΦ m κ k t y).mulVec (G I hΦ m T (lIdx β I.Λ m k) t y)) x = Homogenization.vecDot (fun (j : Fin 2) => deriv (fun (s : ℝ) => I.chiMK κ m k s (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) j) t) (G I hΦ m T (lIdx β I.Λ m k) t x) + Homogenization.vecDot (matDiv (correctorDefectMatrix I hΦ m k t κ) x) (G I hΦ m T (lIdx β I.Λ m k) t x) + Homogenization.vecDot (matDiv (correctorPushforwardMatrix I hΦ m k t κ) x) (G I hΦ m T (lIdx β I.Λ m k) t x) + frob (correctorFlux I hΦ m κ k t x) (gradMatrix (G I hΦ m T (lIdx β I.Λ m k) t) x)

Pairing the selected corrector flux divergence with its pulled gradient gives the corrector time term, the two flow errors, and the Frobenius contraction with gradG.