Material primitive identity for actual differentiated increments.

theorem AVenhance.Infra.Section4.iterate_increment_material_primitive_pairing {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hm : 1 ≤ m) (hκm : 0 < κm) (i : ℕ) (hi : i + 1 ≤ Nstar β) (w r : List (Fin 2)) (j k : Fin 2) {s : ℝ} (hs : 0 ≤ s) : have u := fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T (i + 1) t); have v := fun (t : ℝ) => iterateSpatialWord r (iterateIncrement T i t); have q := fun (t : ℝ) => iterateKmatPrimitive I κm m t j k; ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, (I.Kmat κm m t j k - timeAvgMat (I.Kmat κm m) j k) * u t x * v t x = ((∫ (x : Homogenization.Vec 2) in unitCube, u s x * (q s * v s x)) - ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, q t * u t x * amnrMaterial (streamVel (Φ (m - 1))) v t x) - ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, q t * v t x * amnrMaterial (streamVel (Φ (m - 1))) u t x

Apply material primitive integration by parts to the actual finite increment sequence. The terminal term is retained; all natural integrability and regularity premises are discharged.