OAI/Geometry/WeakHessian/Entropy/RenormalizedEntropy.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.WeakHessian.renormalizedEntropyline 46 - lemma
OAI.WeakHessian.renormalizedEntropy_eqline 49 - lemma
OAI.WeakHessian.renormalizedEntropy_lowerline 54 - lemma
OAI.WeakHessian.renormalizedEntropy_hasDerivline 70 - lemma
OAI.WeakHessian.renormalizedEntropy_upperline 75