OAI/Analysis/BiholderTransport/CostGeometry/OuterCurvature.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.deriv_eq_of_eqOn_interval line 12
2. lemma OAI.WeakMTWTransport.outerJ_affine_integral line 18
3. lemma OAI.WeakMTWTransport.outerJ_barrier line 47
4. lemma OAI.WeakMTWTransport.outerProfile_forces_affine line 55
5. lemma OAI.WeakMTWTransport.outerProfile_derivatives_left line 64
6. lemma OAI.WeakMTWTransport.outerProfile_curvature line 82