OAI/Geometry/WeakMTW/Variations/CurveCalculus.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.WeakMTWGlobalSupport.VariationCalculus.directional_linearizationline 19 - theorem
OAI.WeakMTWGlobalSupport.VariationCalculus.hasDerivAt_time_sliceline 37 - theorem
OAI.WeakMTWGlobalSupport.VariationCalculus.variation_hasDerivAtline 44