Iterates Mean Correction Regularity

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_mean_correction_word_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (κprev : ℝ) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (w : List (Fin 2)) : ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm z.1 y) w z.2) (Set.Ici 0 ×ˢ Set.univ)

Every jet of the actual mean-plus-spatial correction is continuous up to the initial time under the conditional flow carrier.