Differentiability of a flow with respect to its initial-time parameter.

theorem AVenhance.Infra.Flow.StartTimeDerivative.hasDerivAt_diagonalIntervalIntegral {g : ℝ × ℝ → Homogenization.Vec 2} (hg : Continuous g) (a : ℝ) : HasDerivAt (fun (r : ℝ) => ∫ (u : ℝ) in r..a, g (u, r)) (-g (a, a)) a

theorem AVenhance.Infra.Flow.StartTimeDerivative.hasDerivAt_flow_from_fixed_target {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (a : ℝ) : HasDerivAt (fun (r : ℝ) => X a x r) (-b a x) a

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

The derivative with respect to the initial time is the negative spatial Jacobian applied to the vector field at the initial point.