OAI/Geometry/WeakHessian/LocalBounds/GammaNatMulLeft.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.gamma_nat_mul_left line 50
2. lemma OAI.WeakHessian.gamma_int_mul_left line 63
3. lemma OAI.WeakHessian.gamma_rat_mul_left line 72
4. lemma OAI.WeakHessian.gamma_const_mul_left line 86
5. lemma OAI.WeakHessian.gamma_const_mul_right line 95
6. lemma OAI.WeakHessian.weakGradient_linear_combination_sq line 102
7. lemma OAI.WeakHessian.gamma_sq_le line 123
8. lemma OAI.WeakHessian.abs_gamma_le line 145
9. lemma OAI.WeakHessian.gamma_aestronglyMeasurable line 155
10. lemma OAI.WeakHessian.integrable_gamma line 161