OAI/Geometry/WeakHessian/HeatFlow/HeatCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.quadraticWassersteinSq line 20
2. lemma OAI.WeakHessian.IsOptimalCoupling.quadraticWassersteinSq_eq line 24
3. lemma OAI.WeakHessian.densityMeasure_sqrt_memLp line 33
4. lemma OAI.WeakHessian.densityMeasure_sqrt_weighted line 40
5. lemma OAI.WeakHessian.densityMeasure_finiteEntropy line 50
6. lemma OAI.WeakHessian.CurvatureDimension.density_cost_support line 66
7. lemma OAI.WeakHessian.densityMeasure_quadratic_integrable line 85