OAI/Geometry/WeakHessian/Calculus/NoncompactCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.hopf_dual_le_planEnergy line 19
2. lemma OAI.WeakHessian.exists_coupling_of_energy_limit line 55
3. lemma OAI.WeakHessian.planEnergy_le_coupling_of_restricted_contact line 74