OAI/Geometry/WeakHessian/LocalBounds/EulerStep.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessianFunctional.eulerStep line 42
2. def OAI.WeakHessianFunctional.eulerApproximation line 44
3. lemma OAI.WeakHessianFunctional.eulerStep_denom_pos line 47
4. lemma OAI.WeakHessianFunctional.eulerStep_nonneg line 53
5. lemma OAI.WeakHessianFunctional.eulerStep_le_one line 56
6. lemma OAI.WeakHessianFunctional.eulerStep_continuousOn line 61
7. lemma OAI.WeakHessianFunctional.eulerStep_of_pos line 68
8. lemma OAI.WeakHessianFunctional.eulerStep_half_sq line 73
9. lemma OAI.WeakHessianFunctional.eulerApproximation_antitone line 86
10. lemma OAI.WeakHessianFunctional.eulerApproximation_tendsto line 97
11. lemma OAI.WeakHessianFunctional.eulerApproximation_uniform line 122