OAI/Analysis/MassAction/ODEUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.hasDerivWithinAt_initial_of_ode line 17

   Source documentation

   The ODE and continuity extend the derivative to the initial endpoint.

   theorem hasDerivWithinAt_initial_of_ode
       (hv : Continuous v) (hab : a < b)
       (hf : ContinuousOn f (Icc a b))
       (hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v (f t)) t) :
       HasDerivWithinAt f (v (f a)) (Ici a) a := by
   …

2. theorem OAI.Problem326.eqOn_Icc_of_locallyLipschitz_ode line 35

   Source documentation

   Uniqueness on a closed interval only requires the ODE on its interior.

   theorem eqOn_Icc_of_locallyLipschitz_ode
       (hv : LocallyLipschitz v) (hab : a ≤ b)
       (hf : ContinuousOn f (Icc a b))
       (hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v (f t)) t)
       (hg : ContinuousOn g (Icc a b))
       (hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v (g t)) t)
       (ha : f a = g a) : EqOn f g (Icc a b) := by
   …