OAI/Geometry/WeakHessian/Measure/TimeMeasure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakHessian.timeMeasure line 35
2. abbrev OAI.WeakHessian.ControlSpace line 36
3. def OAI.WeakHessian.intervalVector line 38
4. def OAI.WeakHessian.intervalFunctional line 42
5. lemma OAI.WeakHessian.intervalFunctional_apply line 45
6. lemma OAI.WeakHessian.norm_intervalVector_sq line 53
7. def OAI.WeakHessian.HasControlBound line 62
8. lemma OAI.WeakHessian.HasControlBound.nonneg line 68
9. lemma OAI.WeakHessian.HasControlBound.dist_sq_le line 72
10. lemma OAI.WeakHessian.HasControlBound.squareControl line 87
11. lemma OAI.WeakHessian.isClosed_hasControlBound line 114