OAI/Geometry/WeakHessian/LocalBounds/RadialCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.squareDensity_const_mul line 20
2. lemma OAI.WeakHessian.squareDensity_radial_le line 29
3. lemma OAI.WeakHessian.squareDensity_normalized_radial_support line 41
4. lemma OAI.WeakHessian.squareDensity_normalized_radial_le line 57
5. lemma OAI.WeakHessian.radial_secondMoment_tendsto line 68
6. lemma OAI.WeakHessian.normalized_radial_cost_tendsto line 93