A global-flow interface for normed state spaces beyond the case Vec 2.
def
AVenhance.Infra.Flow.IsFlowOn
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(F : ℝ → E → E)
(Y : ℝ → E → ℝ → E)
:
A characterized global ODE flow on an arbitrary normed state space.
Equations
- AVenhance.Infra.Flow.IsFlowOn F Y = ((∀ (y : E) (s : ℝ), Y s y s = y) ∧ ∀ (y : E) (s t : ℝ), HasDerivAt (fun (r : ℝ) => Y r y s) (F t (Y t y s)) t)