OAI/Geometry/WeakHessian/LocalBounds/RelaxedProx.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.slopeGraph_hom line 31
2. lemma OAI.WeakHessian.relaxedGraph_hom line 47
3. lemma OAI.WeakHessian.relaxedGraph_add line 60
4. lemma OAI.WeakHessian.relaxedGraph_zero line 73
5. structure OAI.WeakHessian.RelaxedProx line 90
6. lemma OAI.WeakHessian.exists_relaxedProx line 95
7. lemma OAI.WeakHessian.RelaxedProx.euler line 130
8. lemma OAI.WeakHessian.RelaxedProx.dual line 140
9. lemma OAI.WeakHessian.RelaxedProx.displacement line 153
10. lemma OAI.WeakHessian.RelaxedProx.comparison line 157