IsAEIntegralCurve γ v means γ : ℝ → E is a global integral curve of v almost everywhere.
That is, γ t is tangent to v t (γ t) for almost all t : ℝ.
1.4. Caratheodory existence
def
IsAEIntegralCurve.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (γ : ℝ → E) (v : ℝ → E → E) : PropIsAEIntegralCurve.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (γ : ℝ → E) (v : ℝ → E → E) : Prop