OAI/Geometry/WeakHessian/Transport/QuadraticCostIncrement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.quadratic_cost_increment line 50
2. lemma OAI.WeakHessianTransport.hopfLax_lipschitz_diameter line 64
3. lemma OAI.WeakHessianTransport.isCompact_lipschitz_norm_ball line 79
4. lemma OAI.WeakHessianTransport.potential_integral_lipschitz line 103
5. lemma OAI.WeakHessianTransport.bounded_dual_improvement line 116
6. lemma OAI.WeakHessianTransport.compact_kantorovich_potentials line 192