OAI/Analysis/BiholderTransport/CostGeometry/StrictDividedAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.shifted_injectivityDomain_of_injectivityDomain line 183
2. lemma OAI.WeakMTWTransport.splitTrialValue_source line 210
3. lemma OAI.WeakMTWTransport.hessianValue_strict_radial_decrease line 217
4. lemma OAI.WeakMTWTransport.divided_hessian_strict_decrease line 228
5. lemma OAI.WeakMTWTransport.WeakMTW.contracted_transverse_concaveOn_set line 251
6. lemma OAI.WeakMTWTransport.WeakMTW.finite_transverse_slack_strict line 274