Extend actual short-time spatial smoothness by the proved flow group law.

theorem AVenhance.Infra.Section4.amnr_flow_spatial_contDiff_infty_global {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) (s t : ℝ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => X t x s

Every fixed-time map of the actual flow is spatially smooth. A finite subdivision and the actual group law extend the proved short-time result.

theorem AVenhance.Infra.Section4.amnr_flow_joint_contDiff_infty_global {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) (s : ℝ) : ContDiff ℝ ↑⊤ fun (z : ℝ × Homogenization.Vec 2) => X z.1 z.2 s

The actual flow is jointly smooth in target time and initial point at all times, using a fixed intermediate time for the local joint argument.