OAI/Geometry/WeakHessian/Transport/BoundedMarginalSum.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessianTransport.boundedMarginalSum line 36
2. lemma OAI.WeakHessianTransport.boundedMarginalSum_apply line 42
3. lemma OAI.WeakHessianTransport.exists_boundedMarginal_majorant line 45
4. def OAI.WeakHessianTransport.compactTensor line 51
5. def OAI.WeakHessianTransport.boundedIntegral line 60
6. lemma OAI.WeakHessianTransport.boundedIntegral_mono line 65
7. def OAI.WeakHessianTransport.boundedMarginalIntegral line 68
8. lemma OAI.WeakHessianTransport.boundedMarginalIntegral_apply line 72
9. lemma OAI.WeakHessianTransport.integral_boundedMarginalSum line 78
10. lemma OAI.WeakHessianTransport.exists_probability_of_positive_marginal_functional line 92