Spatial C² regularity of a smooth periodic flow.

theorem AVenhance.Infra.Flow.flow_spatial_contDiff_two_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) (hst : s ≤ t) : ContDiff ℝ 2 fun (x : Homogenization.Vec 2) => X t x s

On a forward interval, a smooth flow map is twice continuously differentiable in its initial point.

theorem AVenhance.Infra.Flow.flow_spatial_contDiff_two {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) : ContDiff ℝ 2 fun (x : Homogenization.Vec 2) => X t x s

Every fixed-time map of a smooth flow is twice continuously differentiable in its initial point.