OAI/Geometry/WeakHessian/Sobolev/L2GradientGraph.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.eLpNorm_sub_tendsto_of_tendsto_Lp line 23
2. def OAI.WeakHessian.l2GradientGraph line 34
3. lemma OAI.WeakHessian.isClosed_l2GradientGraph line 37
4. lemma OAI.WeakHessian.convex_l2GradientGraph line 47
5. lemma OAI.WeakHessian.exists_upperGradient_of_bounded_l2 line 63
6. lemma OAI.WeakHessian.isClosed_upperGradient_sublevel line 71
7. lemma OAI.WeakHessian.exists_norm_minimal_upperGradient line 79