OAI/Geometry/WeakHessian/Calculus/ELpNormSq.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.eLpNorm_sq_eq_lintegral line 22
2. lemma OAI.WeakHessian.eLpNorm_localSlope_sq line 28
3. lemma OAI.WeakHessian.memLp_localSlope_of_lintegral_lt_top line 38
4. lemma OAI.WeakHessian.norm_localSlope_toLp_sq line 45
5. lemma OAI.WeakHessian.half_lintegral_localSlope_eq line 59
6. lemma OAI.WeakHessian.lipschitz_mem_upperGradient_sublevel line 69
7. lemma OAI.WeakHessian.exists_upperGradient_of_cheeger_lt line 88
8. lemma OAI.WeakHessian.exists_upperGradient_energy_le_cheeger line 108