OAI/Geometry/WeakHessian/Entropy/IntegralDensityMeasureLp'.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.integral_densityMeasure_lp'line 50 - lemma
OAI.WeakHessian.CurvatureDimension.prox_weak_pairing_perturbedline 55 - lemma
OAI.WeakHessian.CurvatureDimension.prox_weak_pairing_centeredline 94