OAI/Geometry/WeakHessian/Transport/CompactBounded.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessianTransport.compactToBounded line 34
2. lemma OAI.WeakHessianTransport.compactToBounded_apply line 39
3. lemma OAI.WeakHessianTransport.compact_thickenedIndicator line 43
4. def OAI.WeakHessianTransport.ballCutoff line 53
5. lemma OAI.WeakHessianTransport.ballCutoff_nonneg line 58
6. lemma OAI.WeakHessianTransport.ballCutoff_le_one line 59
7. lemma OAI.WeakHessianTransport.ballCutoff_eq_one line 61
8. lemma OAI.WeakHessianTransport.tendsto_ballCutoff line 67
9. def OAI.WeakHessianTransport.boundedMulCompact line 73
10. lemma OAI.WeakHessianTransport.exists_finite_measure_le_positive_functional line 79