OAI/Geometry/WeakHessian/Entropy/AcBoundedRenyiGaps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.ac_of_bounded_renyi_gaps line 49
2. lemma OAI.WeakHessian.finiteEntropy_of_renyi_gaps line 72
3. lemma OAI.WeakHessian.density_mul_neg_rpow line 101
4. lemma OAI.WeakHessian.integral_density_neg_rpow line 105
5. lemma OAI.WeakHessian.integrable_density_neg_rpow line 113
6. lemma OAI.WeakHessian.integrable_inverse_density line 121
7. lemma OAI.WeakHessian.density_pos_ae line 132
8. lemma OAI.WeakHessian.tendsto_integral_weighted_density_neg_rpow line 137