Joint continuity of the second variation in target time and initial point.

theorem AVenhance.Infra.Flow.flow_secondVariation_jointContinuous_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => flowSecondVariation hb hX p.2 s ⋯ h k p.1 0 s) (Set.Icc s t ×ˢ Set.univ)

On a forward compact target-time interval, a fixed second spatial variation is jointly continuous in target time and initial point.