Basic uniqueness for global integral curves of uniformly Lipschitz fields.

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

A uniform spatial Lipschitz bound, stated with a real constant, gives a nonnegative LipschitzWith constant for each time slice.

theorem AVenhance.Infra.Flow.integralCurve_unique (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {L : ℝ} (hL : ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {γ η : ℝ → Homogenization.Vec 2} (hγ : ∀ (t : ℝ), HasDerivAt γ (b t (γ t)) t) (hη : ∀ (t : ℝ), HasDerivAt η (b t (η t)) t) {s : ℝ} (h₀ : γ s = η s) : γ = η

Two global integral curves with the same value at one time coincide.