OAI/Geometry/WeakHessian/LocalBounds/CostMetric.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.cost_ne_top_iff_integrable_sq line 20
  2. lemma OAI.WeakHessian.product_coupling_finite_cost line 27
  3. lemma OAI.WeakHessian.exists_optimal_coupling_of_moments line 42
  4. lemma OAI.WeakHessian.IsCoupling.swap line 51
  5. lemma OAI.WeakHessian.quadraticTransportCost_swap line 58
  6. lemma OAI.WeakHessian.quadraticWassersteinSq_comm line 64
  7. lemma OAI.WeakHessian.quadraticWassersteinSq_le_cost line 74
  8. lemma OAI.WeakHessian.sqrt_integral_sq_eq_norm_toLp line 79
  9. lemma OAI.WeakHessian.integral_sq_triangle line 83
  10. lemma OAI.WeakHessian.exists_coupling_triangle line 96
  11. lemma OAI.WeakHessian.quadraticWassersteinSq_triangle line 143