OAI/Geometry/WeakHessian/Transport/DensityMeasure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessianTransport.densityMeasure line 36
2. lemma OAI.WeakHessianTransport.integral_densityMeasure line 38
3. lemma OAI.WeakHessianTransport.densityMeasure_le line 47
4. lemma OAI.WeakHessianTransport.densityMeasure_ac line 54
5. lemma OAI.WeakHessianTransport.densityMeasure_probability line 58
6. def OAI.WeakHessianTransport.densityProbability line 65
7. lemma OAI.WeakHessianTransport.integral_densityMeasure_continuousMap line 70
8. lemma OAI.WeakHessianTransport.continuous_densityProbability line 77
9. lemma OAI.WeakHessianTransport.integral_densityMeasure_boundedContinuous line 97
10. lemma OAI.WeakHessianTransport.continuous_boundedDensityProbability line 105
11. lemma OAI.WeakHessianTransport.proper_density_coupling_bound line 126