Component form of the nondivergence parts

Pure algebra: termwise identities ξ_k D_k : ∇G_k = Σ_{a,j} (fast factor) (slow factor) and the passage from the tsum over odd k to a finite sum over any S containing the support.

theorem AVenhance.Infra.Section5.Contracts.sd_term4_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xiMK m k t * frob (sdDefect4 I hΦ m κm k t x) (gradG I hΦ m T (lIdx β I.Λ m k) t x) = ∑ a : Fin 2, ∑ j : Fin 2, sdFast4 I κm m k t a j (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) * section5SlowChoice2 I hΦ m κm T k t a j x

Termwise component form for twistie4.

theorem AVenhance.Infra.Section5.Contracts.sd_term5_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xiMK m k t * frob (sdDefect5 I hΦ m κm k t x) (gradG I hΦ m T (lIdx β I.Λ m k) t x) = ∑ a : Fin 2, ∑ j : Fin 2, sdFast5 I κm m k t a j (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) * section5SlowChoice3 I hΦ m T k t a j x

Termwise component form for twistie5.

theorem AVenhance.Infra.Section5.Contracts.sd_tsum_eq_sum {f : { k : ℤ // Odd k } → ℝ} (S : Finset { k : ℤ // Odd k }) (hS : ∀ (k : { k : ℤ // Odd k }), f k ≠ 0 → k ∈ S) : ∑' (k : { k : ℤ // Odd k }), f k = ∑ k ∈ S, f k

A tsum over odd k of terms vanishing off S is the finite sum over S.