Actual joint smoothness of a flow from its parameterized integral equation.

theorem AVenhance.Infra.Section4.amnr_flow_contDiffAt_joint_of_short {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 : ℝ) (x : Homogenization.Vec 2) (hshort : |t - s| * M ≤ 1 / 4) : ContDiffAt ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => X z.1 z.2 s) (t, x)

The actual target-time and initial-position flow map is smooth locally on a short interval. A parameter scaling makes its augmented Volterra operator invertible; no mixed flow derivative is assumed.