OAI/Geometry/WeakHessian/Calculus/DerivSinSubMul.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.hasDerivAt_sin_sub_mul_cos line 45
2. lemma OAI.WeakHessian.hasDerivAt_sin_cubic line 49
3. lemma OAI.WeakHessian.hasDerivAt_mul_cosh_sub_sinh line 56
4. lemma OAI.WeakHessian.hasDerivAt_sinh_cubic line 60
5. lemma OAI.WeakHessian.hasDerivAt_log_sin_correction line 67
6. lemma OAI.WeakHessian.hasDerivAt_log_sinh_correction line 74
7. lemma OAI.WeakHessian.sin_sub_mul_cos_nonneg line 81
8. lemma OAI.WeakHessian.sin_cubic_cot_bound line 94
9. lemma OAI.WeakHessian.mul_cosh_sub_sinh_nonneg line 110
10. lemma OAI.WeakHessian.sinh_cubic_coth_bound line 122
11. lemma OAI.WeakHessian.antitone_log_sin_correction line 137
12. lemma OAI.WeakHessian.antitone_log_sinh_correction line 158
13. lemma OAI.WeakHessian.sin_ratio_exp_lower line 176
14. lemma OAI.WeakHessian.sinh_ratio_exp_lower line 192