Exists Unique Flow

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Proofs.existsUnique_flow (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb : Continuous fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) : ∃! X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow b X

Provider for the globally well-posed flow of a continuous uniformly globally Lipschitz vector field.