Iterates Flux Pairing Continuity

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_word_flux_pairing_continuousOn {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (hA : ∀ p ∈ iterateSpatialSplits w, ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) p.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (z : AmnrSpace) => Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateWordFlux (A z.1) (v z.1) w z.2)) (Set.Ici 0 ×ˢ Set.univ)

The actual word flux pairing is continuous up to zero when its scalar carriers and literal coefficient jets are continuous up to zero.