OAI/Analysis/BiholderTransport/Geodesics/SprayMinimizerUnique.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.sprayFlow_minimizer_terminal_eq line 82
2. lemma OAI.WeakMTWTransport.sprayFlow_minimizer_unique_of_gradient line 96
3. lemma OAI.WeakMTWTransport.exists_local_spray_minimizer_unique line 112
4. lemma OAI.WeakMTWTransport.tangentScale_injective line 131
5. lemma OAI.WeakMTWTransport.sprayFlow_unit_minimizer_unique line 151