Discharge the pointwise spatial differentiability inputs to the last-iterate transport equation.

theorem AVenhance.Infra.Section5.TEquationRegularity.sMat_spatial_contDiff_one {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm t : ℝ) : ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => I.sMat hΦ m κm t x

theorem AVenhance.Infra.Section5.final_iterate_transport_eq_of_classical {β : ℝ} (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) {t : ℝ} {x : Homogenization.Vec 2} (ht : 0 < t) : deriv (fun (s : ℝ) => T (Nstar β) s x) t + Homogenization.vecDot (streamVel (Φ (m - 1)) t x) (spaceGrad (T (Nstar β) t) x) = vecDiv (fun (y : Homogenization.Vec 2) => (I.Kmat κm m t + I.sMat hΦ m κm t y).mulVec (spaceGrad (T (Nstar β) t) y) + iterateError I hΦ m κm κprev T t y) x

The final iterate equation with its spatial differentiability inputs derived from the classical iterate hypotheses and cutoff support.