OAI/Geometry/WeakHessian/LocalBounds/L2SlopeGraph.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.localSlope_ne_top line 32
  2. lemma OAI.WeakHessian.localSlope_toReal_add_le line 37
  3. lemma OAI.WeakHessian.localSlope_toReal_const_mul line 46
  4. def OAI.WeakHessian.l2SlopeGraph line 50
  5. def OAI.WeakHessian.l2RelaxedGraph line 54
  6. lemma OAI.WeakHessian.convex_l2SlopeGraph line 58
  7. lemma OAI.WeakHessian.isClosed_l2RelaxedGraph line 89
  8. lemma OAI.WeakHessian.convex_l2RelaxedGraph line 91
  9. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.mono line 94
  10. lemma OAI.WeakHessian.slopeGraph_isUpperGradient line 108
  11. lemma OAI.WeakHessian.relaxedGraph_isUpperGradient line 116
  12. lemma OAI.WeakHessian.isClosed_relaxedGradient_sublevel line 123
  13. lemma OAI.WeakHessian.exists_norm_minimal_relaxedGradient line 134