OAI/Geometry/WeakHessian/LocalBounds/HopfEnergyLower.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessianTransport.continuousOn_integral_boundedHopfMapline 19 - lemma
OAI.WeakHessianTransport.integral_hopf_positive_slopeline 30 - lemma
OAI.WeakHessianTransport.integral_hopf_fallingline 51