OAI/Geometry/WeakHessian/LocalBounds/DistDecayCover.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.exp_geometric_bound_eq line 47
2. def OAI.WeakHessian.distDecayCover line 57
3. lemma OAI.WeakHessian.measurable_distDecayCover line 60
4. lemma OAI.WeakHessian.exp_neg_dist_le_cover line 64
5. lemma OAI.WeakHessian.lintegral_distDecayCover_le line 76
6. lemma OAI.WeakHessian.integrable_exp_neg_dist_of_growth line 88
7. lemma OAI.WeakHessian.memLp_exp_neg_dist_of_growth line 106