OAI/Geometry/WeakHessian/Measure/RadialCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.exists_probability_reference line 42
2. def OAI.WeakHessian.radialCutoff line 125
3. lemma OAI.WeakHessian.radialCutoff_nonneg line 126
4. lemma OAI.WeakHessian.radialCutoff_le_one line 127
5. lemma OAI.WeakHessian.radialCutoff_lipschitz line 131
6. lemma OAI.WeakHessian.radialCutoff_compact line 141
7. lemma OAI.WeakHessian.radialCutoff_tendsto line 149