OAI/Geometry/WeakHessian/Entropy/ReducedEntropyDual.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.integral_renormalizedEntropy_eq line 21
2. lemma OAI.WeakHessian.tendsto_regularizedEntropy_difference line 30
3. lemma OAI.WeakHessian.entropy_dual_of_regularized line 47
4. lemma OAI.WeakHessian.cheegerHeat_entropy_dual_reduced line 66