OAI/Analysis/BiholderTransport/Geodesics/SprayDistanceBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.sprayFlow_pathELength line 84
2. lemma OAI.WeakMTWTransport.dist_sprayFlow_le line 100
3. lemma OAI.WeakMTWTransport.continuous_riemannianExp line 126
4. lemma OAI.WeakMTWTransport.dist_riemannianExp_smul_le line 129
5. lemma OAI.WeakMTWTransport.dist_riemannianExp_le line 134
6. lemma OAI.WeakMTWTransport.minimizingVectors_smul line 139
7. lemma OAI.WeakMTWTransport.injectivityDomain_subset_minimizingVectors line 152
8. lemma OAI.WeakMTWTransport.contracted_minimizer_mem_injectivityDomain line 167
9. lemma OAI.WeakMTWTransport.isClosed_minimizingVectors line 174
10. lemma OAI.WeakMTWTransport.isCompact_minimizingVectors line 177
11. lemma OAI.WeakMTWTransport.closure_injectivityDomain line 186
12. lemma OAI.WeakMTWTransport.isCompact_total_minimizingVectors line 196