OAI/Analysis/BiholderTransport/Coordinates/UniformShort.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.contMDiff_tangentScale line 87
2. lemma OAI.WeakMTWTransport.sprayFlow_zero_velocity_base line 104
3. lemma OAI.WeakMTWTransport.sprayFlow_minimizing_near_zero_section line 110
4. lemma OAI.WeakMTWTransport.sprayFlow_uniformly_short_minimizing line 160