OAI/Geometry/WeakHessian/Sobolev/UpperGradientTendstoNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.upperGradient_tendsto_of_norm_tendsto line 49
2. lemma OAI.WeakHessian.IsMinimalLocalWeakUpperGradient.norm_le line 104
3. lemma OAI.WeakHessian.IsMinimalLocalWeakUpperGradient.tendsto_of_norm_tendsto line 111
4. lemma OAI.WeakHessian.CurvatureDimension.reference_relaxedGradient_isMinimal line 127
5. lemma OAI.WeakHessian.CurvatureDimension.reference_exists_relaxedGradient_le line 141