OAI/Geometry/WeakHessian/Entropy/ReducedEntropy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.reducedEntropy line 46
2. lemma OAI.WeakHessian.renormalizedEntropy_tendsto line 48
3. lemma OAI.WeakHessian.reducedEntropy_lower line 58
4. lemma OAI.WeakHessian.reducedEntropy_upper line 63
5. lemma OAI.WeakHessian.renormalizedEntropy_abs_bound line 67
6. lemma OAI.WeakHessian.reducedEntropy_abs_bound line 75
7. lemma OAI.WeakHessian.integrable_reducedEntropy line 82
8. lemma OAI.WeakHessian.tendsto_integral_renormalizedEntropy line 91