Continuity #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.CoarseCoeffForm.word_joint_continuousOn
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hΦ : IsStreamSeq I Φ}
{m : ℕ}
{κ : ℝ}
{s : ℝ → Homogenization.Vec 2 → CoarseMatrix}
(hs : CoarseCoeffForm I hΦ m κ s)
(hm : 1 ≤ m)
(hκ : 0 < κ)
(hflow : ∀ (l : ℤ), ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
(i j : Fin 2)
:
ContinuousOn (fun (z : AmnrSpace) => iterateSpatialWord w (fun (y : Homogenization.Vec 2) => s z.1 y i j) z.2)
(Set.Ici 0 ×ˢ Set.univ)
All ordered coefficient jets are jointly continuous up to the initial time. The only conditional regularity inputs concern the flow; the polynomial and locally finite cutoff calculus apply to both structural instances.