OAI/Geometry/WeakHessian/Entropy/TauDensityLinearLower.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.tau_density_linear_lower line 49
2. lemma OAI.WeakHessian.integral_le_of_lintegral_ofReal_le line 64
3. lemma OAI.WeakHessian.renyiIntegral_ofReal line 85
4. lemma OAI.WeakHessian.integrable_density_neg_rpow_comp line 99
5. lemma OAI.WeakHessian.integral_density_neg_rpow_comp line 107
6. lemma OAI.WeakHessian.cd_renyi_gap_bound line 117