OAI/Geometry/WeakHessian/Calculus/ScalarSecondDifference.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.secondDifference line 17
2. lemma OAI.WeakHessian.taylorPolynomial_two line 20
3. lemma OAI.WeakHessian.secondDifference_tendsto line 28
4. lemma OAI.WeakHessian.taylor_remainder_one line 55
5. lemma OAI.WeakHessian.norm_secondDifference_le line 68
6. lemma OAI.WeakHessian.integral_mul_translate line 87
7. lemma OAI.WeakHessian.integrable_mul_translate line 92
8. lemma OAI.WeakHessian.integrable_translate_mul line 98
9. lemma OAI.WeakHessian.integral_mul_secondDifference line 104
10. lemma OAI.WeakHessian.secondDifference_eq_zero_outside line 134
11. lemma OAI.WeakHessian.secondDifference_nonpos_of_concave line 157
12. lemma OAI.WeakHessian.integral_secondDifference_tendsto line 171