Joint continuity follows from curve continuity, the flow law, and the spatial Grönwall estimate.

theorem AVenhance.Infra.Flow.flow_continuous_fixed_start (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {L : ℝ} (hL : ∀ (u : ℝ) (x y : Homogenization.Vec 2), ‖b u x - b u y‖ ≤ L * ‖x - y‖) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) : Continuous fun (p : ℝ × Homogenization.Vec 2) => X p.1 p.2 s

For a fixed initial time, the flow is jointly continuous in target time and initial position.

theorem AVenhance.Infra.Flow.flow_continuous_joint (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {L : ℝ} (hL : ∀ (u : ℝ) (x y : Homogenization.Vec 2), ‖b u x - b u y‖ ≤ L * ‖x - y‖) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous fun (p : ℝ × Homogenization.Vec 2 × ℝ) => X p.1 p.2.1 p.2.2

A globally characterized flow is jointly continuous in target time, initial position, and initial time.