OAI/Geometry/WeakHessian/Calculus/RnDerivRestrictReference.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.rnDeriv_restrict_reference line 50
2. lemma OAI.WeakHessian.rnDeriv_restrict_reference_ae line 58
3. lemma OAI.WeakHessian.renyiIntegral_restrict_reference line 63
4. lemma OAI.WeakHessian.finiteEntropy_restrict_reference_iff line 79
5. lemma OAI.WeakHessian.entropyReal_restrict_reference line 90