Statement file: flow (FlowDefs).
This file contains exactly one declaration of the formalization's public statement surface.
noncomputable def
AVenhance.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‖)
:
ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2
The flow X(t,x,s) of e.flow.m.def (source 1397–1410): the unique X with
IsFlow b X, chosen from the proved existsUnique_flow.
Equations
- AVenhance.flow b hb hL = Classical.choose ⋯