Joint continuity of the spatial derivative in all flow parameters.

theorem AVenhance.Infra.Flow.flow_reference_derivative_inverse {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (r : ℝ) (x : Homogenization.Vec 2) (s : ℝ) (z : Homogenization.Vec 2) (hz : z = X r x s) : have A := fderiv ℝ (fun (y : Homogenization.Vec 2) => X s y r) z; have B := fderiv ℝ (fun (y : Homogenization.Vec 2) => X r y s) x; A.IsInvertible ∧ A.inverse = B

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_reference_factor {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (r : ℝ) (x : Homogenization.Vec 2) (s t : ℝ) : fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x = fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y r) (X r x s) ∘SL (fderiv ℝ (fun (y : Homogenization.Vec 2) => X s y r) (X r x s)).inverse

theorem AVenhance.Infra.Flow.JointSpatialDerivativeAll.flow_fixedStart_spatialFDeriv_continuousAt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (r T u : ℝ) (z : Homogenization.Vec 2) (hru : r < u) (huT : u < T) : ContinuousAt (fun (q : ℝ × Homogenization.Vec 2) => fderiv ℝ (fun (y : Homogenization.Vec 2) => X q.1 y r) q.2) (u, z)

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_jointContinuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous fun (p : ℝ × Homogenization.Vec 2 × ℝ) => fderiv ℝ (fun (y : Homogenization.Vec 2) => X p.1 y p.2.2) p.2.1

The spatial Fréchet derivative of a smooth flow is jointly continuous in target time, initial point, and initial time.