Fixed-point material form of the pulled-gradient transport identity.

theorem AVenhance.Infra.Section5.final_iterate_pulled_gradient_material_transport {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (l : ℤ) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) (j : Fin 2) {L : ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hG : HasFDerivAt (Function.uncurry fun (r : ℝ) (y : Homogenization.Vec 2) => G I hΦ m (T (Nstar β)) l r y) L (t, x)) : deriv (fun (r : ℝ) => G I hΦ m (T (Nstar β)) l r x j) t + (fderiv ℝ (G I hΦ m (T (Nstar β)) l t) x) (streamVel (Φ (m - 1)) t x) j = (I.flowGrad hΦ m l t x).mulVec (gradDiv (fun (r : ℝ) (y : Homogenization.Vec 2) => (I.Kmat κm m r + I.sMat hΦ m κm r y).mulVec (spaceGrad (T (Nstar β) r) y) + iterateError I hΦ m κm κprev T r y) t x) j

The transported gradient of the last iterate obeys the source's fixed-point material identity. This is e.tbm1.two after changing from a characteristic to its fixed spatial point.