Statement file: flowInv (FlowDefs).
This file contains exactly one declaration of the formalization's public statement surface.
noncomputable def
AVenhance.flowInv
(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‖)
(t : ℝ)
(y : Homogenization.Vec 2)
(s : ℝ)
:
The inverse flow X⁻¹(t,·,s), the inverse function of X(t,·,s) (source 1410–1415,
e.flowabbrev), realized by the group law as X⁻¹(t,y,s) = X(s,y,t).
Equations
- AVenhance.flowInv b hb hL t y s = AVenhance.flow b hb hL s y t