OAI/Geometry/WeakHessian/LocalBounds/ChangeLpLp.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.changeLp_toLpline 50 - lemma
OAI.WeakHessian.tendsto_toLp_changeMeasureline 60 - lemma
OAI.WeakHessian.FiniteOnBoundedSets.of_measure_le_smulline 69 - lemma
OAI.WeakHessian.changeLp_inverseline 86 - lemma
OAI.WeakHessian.relaxedGraph_changeMeasureline 95 - lemma
OAI.WeakHessian.relaxedGradient_minimal_comparableline 120 - lemma
OAI.WeakHessian.cheegerEnergy_relaxed_comparableline 149