OAI/Geometry/WeakHessian/LocalBounds/CappedExcess.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.cappedExcess line 47
2. lemma OAI.WeakHessian.cappedExcess_lowerSemicontinuous line 51
3. lemma OAI.WeakHessian.cappedExcess_query_le line 62
4. lemma OAI.WeakHessian.cappedExcess_le_one line 67
5. lemma OAI.WeakHessian.cappedExcess_closed_query_le line 82
6. lemma OAI.WeakHessian.cappedExcess_eq_zero_iff line 99
7. lemma OAI.WeakHessian.exists_cappedExcess_minimizer line 126
8. lemma OAI.WeakHessian.measure_le_add_cappedExcess line 132
9. lemma OAI.WeakHessian.measure_le_sub_add line 147
10. lemma OAI.WeakHessian.positivePart_total_of_hahn line 163
11. lemma OAI.WeakHessian.cappedExcess_eq_positivePart line 177