OAI/Geometry/WeakHessian/Entropy/CenteredMulLogDeriv.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.centered_mul_log_hasDeriv line 48
2. lemma OAI.WeakHessian.centered_mul_log_antitone line 53
3. lemma OAI.WeakHessian.centered_mul_log_monotone line 65
4. lemma OAI.WeakHessian.centered_mul_log_le_of_between line 77
5. lemma OAI.WeakHessian.ae_le_of_withDensity_le line 91
6. lemma OAI.WeakHessian.rnDeriv_le_of_domination line 98
7. lemma OAI.WeakHessian.finiteEntropy_of_bounded_density line 104
8. lemma OAI.WeakHessian.entropyReal_le_of_density_capping line 116