Grönwall and displacement estimates for characterized global flows.

theorem AVenhance.Infra.Flow.lipschitz_constant_nonneg (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {L : ℝ} (hL : ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) : 0 ≤ L

The real constant in a global Lipschitz estimate is nonnegative when the estimate holds on the nontrivial space Vec 2.

theorem AVenhance.Infra.Flow.flow_spatial_gronwall_of_le (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {L : ℝ} (hL : ∀ (u : ℝ) (x y : Homogenization.Vec 2), ‖b u x - b u y‖ ≤ L * ‖x - y‖) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x y : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : ‖X t x s - X t y s‖ ≤ Real.exp (L * (t - s)) * ‖x - y‖

Grönwall's spatial stability estimate when the target time is not before the initial time.

theorem AVenhance.Infra.Flow.flow_spatial_gronwall (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {L : ℝ} (hL : ∀ (u : ℝ) (x y : Homogenization.Vec 2), ‖b u x - b u y‖ ≤ L * ‖x - y‖) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x y : Homogenization.Vec 2) (s t : ℝ) : ‖X t x s - X t y s‖ ≤ Real.exp (L * |t - s|) * ‖x - y‖

Grönwall's spatial stability estimate at arbitrary times.