RelativeError: short-time derivative bounds for the transport flow

theorem AVenhance.Infra.Section5.RelativeError.flow_fderiv_norm_le_exp {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {B : ℝ} (hB : 0 ≤ B) (hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B) (s t : ℝ) (x : Homogenization.Vec 2) : ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x‖ ≤ Real.exp (B * |t - s|)

Grönwall's deviation estimate gives the exponential bound on the full operator norm of a spatial flow derivative.

theorem AVenhance.Infra.Section5.RelativeError.flow_transport_derivatives_le_exp_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {B T : ℝ} (hB : 0 ≤ B) (hBT : B * T ≤ 1) (hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B) {t : ℝ} (ht : t ∈ Set.Icc 0 T) (x : Homogenization.Vec 2) : ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y 0) x‖ ≤ Real.exp 1 ∧ ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X 0 y t) x‖ ≤ Real.exp 1

On a window with B T ≤ 1, both the forward and inverse spatial flow derivatives are bounded by e.