OAI/Geometry/WeakHessian/Entropy/RadialEntropy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.mul_log_product line 16
2. lemma OAI.WeakHessian.entropy_integral_multipliers_tendsto line 27
3. lemma OAI.WeakHessian.squareDensity_entropy_eq line 55
4. lemma OAI.WeakHessian.squareDensity_finiteEntropy_iff line 64
5. lemma OAI.WeakHessian.normalized_radial_entropy_tendsto line 75