OAI/Geometry/WeakHessian/Entropy/LogAddTwoSqrt.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.log_one_add_le_two_sqrt line 46
2. lemma OAI.WeakHessian.renormalizedEntropy_error line 56
3. lemma OAI.WeakHessian.integrable_reducedEntropy_of_sqrt line 92
4. lemma OAI.WeakHessian.integral_renormalizedEntropy_error line 107
5. lemma OAI.WeakHessian.tendsto_integral_renormalizedEntropy_Lp line 122
6. lemma OAI.WeakHessian.tendsto_integral_reducedEntropy_of_sqrt_bound line 137