The exact transport equation for the final T-iterate.

noncomputable def AVenhance.Infra.Section5.iterateError {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The source error e_{m-1} from the difference between the last two T-iterates.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.final_iterate_transport_eq {β : ℝ} (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) {t : ℝ} {x : Homogenization.Vec 2} (hA : ∀ (i : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => (I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y).mulVec (spaceGrad (T (Nstar β - 1) t) y) i) x) (hgrad : ∀ (i : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (T (Nstar β) t) y i) x) (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 last iterate satisfies the source's exact T_{m-1} equation, with the finite-iteration error retained as e_{m-1}.