Iterates C1Spatial Continuity

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_spatial_partial_continuous_up_to_initial {f : AmnrSpace → ℝ} (hf : ContDiffOn ℝ 1 f (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContinuousOn (fun (z : AmnrSpace) => spaceGrad (fun (y : Homogenization.Vec 2) => f (z.1, y)) z.2 i) (Set.Ici 0 ×ˢ Set.univ)