OAI/Geometry/WeakHessian/Entropy/EntropySlope.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.squareDensity_zero_outside line 18
2. lemma OAI.WeakHessian.integral_mul_le_sqrt_integral_sq line 28
3. lemma OAI.WeakHessian.IsTestPlan.contact_gamma_fisher_bound line 42
4. lemma OAI.WeakHessian.squareDensity_sobolev_of_supported line 104
5. theorem OAI.WeakHessian.RCD.bounded_entropy_fisher line 111