OAI/Geometry/WeakHessian/Transport/QuadraticCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.compact_kantorovich_duality line 40
2. def OAI.WeakHessianTransport.quadraticCost line 98
3. lemma OAI.WeakHessianTransport.quadraticCost_apply line 103
4. lemma OAI.WeakHessianTransport.lipschitz_dual_improvement line 108
5. lemma OAI.WeakHessianTransport.compact_hopf_duality line 147