OAI/Geometry/WeakHessian/LocalBounds/WeightedEnergyClosure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.exists_boundedContinuous_of_compact line 21
2. lemma OAI.WeakHessian.integrable_bounded_Lp_sq line 33
3. lemma OAI.WeakHessian.integral_bounded_Lp_sq line 41
4. lemma OAI.WeakHessian.tendsto_integral_bounded_Lp_sq line 52
5. lemma OAI.WeakHessian.RCD.cheegerHeat_weightedEnergy line 59