OAI/Geometry/WeakHessian/Sobolev/CheegerEnergyMinimal.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.CurvatureDimension.cheegerEnergy_eq_minimalline 55 - lemma
OAI.WeakHessian.CurvatureDimension.sobolev_iff_cheeger_lt_topline 67 - lemma
OAI.WeakHessian.CurvatureDimension.cheegerEnergy_eq_weakGradientline 84