OAI/Geometry/WeakHessian/Transport/CcConst.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessianTransport.ccConst line 32
  2. lemma OAI.WeakHessianTransport.ccConst_apply line 35
  3. def OAI.WeakHessianTransport.marginalSum line 37
  4. lemma OAI.WeakHessianTransport.marginalSum_apply line 49
  5. lemma OAI.WeakHessianTransport.exists_marginal_majorant line 52
  6. def OAI.WeakHessianTransport.marginalIntegral line 61
  7. lemma OAI.WeakHessianTransport.marginalIntegral_apply line 67
  8. lemma OAI.WeakHessianTransport.integral_marginalSum line 71
  9. lemma OAI.WeakHessianTransport.exists_measure_of_positive_functional line 83
  10. lemma OAI.WeakHessianTransport.probability_of_first_marginal line 91
  11. lemma OAI.WeakHessianTransport.integral_marginalSum_of_marginals line 98
  12. lemma OAI.WeakHessianTransport.marginals_of_integral_identity line 117