OAI/Geometry/WeakHessian/Sobolev/SobolevCheegerEnergyTop.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.sobolev_of_cheegerEnergy_lt_topline 51 - lemma
OAI.WeakHessian.integral_parallelogram_of_cheegerline 60 - lemma
OAI.WeakHessian.cheegerEnergy_integral_of_comparableline 83 - lemma
OAI.WeakHessian.quadraticCheegerEnergy_of_comparableline 106