OAI/Geometry/WeakHessian/HeatFlow/HeatProbability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.densityMeasure_probability_integral line 18
2. def OAI.WeakHessian.integrableDensityProbability line 24
3. lemma OAI.WeakHessian.integral_densityMeasure_L2 line 29
4. lemma OAI.WeakHessian.cheegerHeat_density_duality line 36
5. def OAI.WeakHessian.CurvatureDimension.heatProbability line 44
6. lemma OAI.WeakHessian.CurvatureDimension.heatProbability_coe line 53