OAI/Geometry/WeakHessian/LocalBounds/RootApproximation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.rootClip line 18
2. lemma OAI.WeakHessian.rootClip_lipschitz line 19
3. lemma OAI.WeakHessian.rootClip_zero line 21
4. lemma OAI.WeakHessian.rootClip_nonneg line 22
5. lemma OAI.WeakHessian.rootClip_le line 23
6. lemma OAI.WeakHessian.rootClip_eq line 25
7. lemma OAI.WeakHessian.exists_clipped_cutoff_approx line 31
8. def OAI.WeakHessian.rootCutoff line 158
9. lemma OAI.WeakHessian.rootCutoff_lipschitz line 159
10. lemma OAI.WeakHessian.rootCutoff_nonneg line 170
11. lemma OAI.WeakHessian.rootCutoff_le_one line 171
12. lemma OAI.WeakHessian.rootCutoff_one line 172
13. lemma OAI.WeakHessian.rootCutoff_support line 176
14. lemma OAI.WeakHessian.cutoff_gradient_identities line 188
15. theorem OAI.WeakHessian.CurvatureDimension.compact_root_approximation line 217