OAI/Geometry/WeakHessian/LocalBounds/QuadraticContact.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.planEnergy_le_of_restricted_contact line 20
2. lemma OAI.WeakHessian.entropy_pairing_congr_squareDensity line 52
3. lemma OAI.WeakHessian.RCD.compact_quadratic_entropy_subgradient line 70