OAI/Analysis/BiholderTransport/LocalFlow/ImplicitODE.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.exists_smooth_rescaled_equation_on line 50
2. lemma OAI.WeakMTWTransport.exists_smooth_rescaled_ode_family_on line 81
3. def OAI.WeakMTWTransport.rescaledIntegralCurve line 96
4. lemma OAI.WeakMTWTransport.rescaledIntegralCurve_zero line 100
5. lemma OAI.WeakMTWTransport.rescaledIntegralCurve_eq line 104
6. lemma OAI.WeakMTWTransport.hasDerivAt_rescaledIntegralCurve line 110
7. lemma OAI.WeakMTWTransport.lipschitzOnWith_const_smul line 125
8. lemma OAI.WeakMTWTransport.rescaled_ode_path_time_scaling line 134