OAI/Analysis/BiholderTransport/Coordinates/ActiveDifferentiability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.activeLog_derivative_eq line 19
2. lemma OAI.WeakMTWTransport.activeLogs_subsingleton_of_mdifferentiable line 45
3. lemma OAI.WeakMTWTransport.contact_singleton_of_mdifferentiable line 60
4. lemma OAI.WeakMTWTransport.lipschitz_ae_mdifferentiable_metricVolume line 73
5. lemma OAI.WeakMTWTransport.cTransform_ae_singleton_contacts line 84