OAI/Geometry/WeakHessian/LocalBounds/PositiveProbes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.densityMeasure_ac_of_pos line 17
2. lemma OAI.WeakHessian.restrict_le_densityMeasure line 22
3. lemma OAI.WeakHessian.densityMeasure_locally_le line 38
4. def OAI.WeakHessian.positiveProbe line 53
5. lemma OAI.WeakHessian.positiveProbe_coe line 56
6. lemma OAI.WeakHessian.positiveProbe_pos line 61
7. lemma OAI.WeakHessian.positiveProbe_integrable line 67
8. lemma OAI.WeakHessian.positiveProbe_le line 74
9. lemma OAI.WeakHessian.positiveProbe_locally_dominates line 85