Start-time continuity of the second spatial derivative via inverse flow.

theorem AVenhance.Infra.Flow.HessianJointAll.flowSecondSpatialDerivative_comp {F G : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ 2 F) (hG : ContDiff ℝ 2 G) (x h k : Homogenization.Vec 2) : ((fderiv ℝ (fun (y : Homogenization.Vec 2) => fderiv ℝ (fun (z : Homogenization.Vec 2) => F (G z)) y) x) h) k = ((fderiv ℝ (fun (y : Homogenization.Vec 2) => fderiv ℝ F y) (G x)) ((fderiv ℝ G x) h)) ((fderiv ℝ G x) k) + (fderiv ℝ F (G x)) (((fderiv ℝ (fun (y : Homogenization.Vec 2) => fderiv ℝ G y) x) h) k)

The second derivative of a composition, represented as a nested continuous linear map.

theorem AVenhance.Infra.Flow.flowSecondSpatialDerivative_inverse_formula {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (r s : ℝ) (x h k : Homogenization.Vec 2) : ((flowSecondSpatialDerivative X r x s) h) k = -(fderiv ℝ (fun (y : Homogenization.Vec 2) => X r y s) x) (((flowSecondSpatialDerivative X s (X r x s) r) ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X r y s) x) h)) ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X r y s) x) k))

The Hessian of the inverse fixed-time flow is determined by the Hessian of the forward map and the inverse first derivative.

theorem AVenhance.Infra.Flow.flowSecondSpatialDerivative_jointContinuous_all {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 × ℝ) => flowSecondSpatialDerivative X p.1 p.2.1 p.2.2

The Hessian of the flow is jointly continuous in target time, initial point, and start time. The proof factors through one reference time and uses the inverse Hessian identity for the backward leg.