OAI/Geometry/WeakHessian/HeatFlow/CheegerHeatAbs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.cheegerHeat_abs_le line 51
2. lemma OAI.WeakHessian.cheegerHeat_integrable line 65
3. lemma OAI.WeakHessian.integrable_posPartLp line 78
4. lemma OAI.WeakHessian.integrable_negPartLp line 83
5. lemma OAI.WeakHessian.posPart_sub_negPartLp line 88
6. lemma OAI.WeakHessian.cheegerHeat_pairing_bound line 96
7. lemma OAI.WeakHessian.CurvatureDimension.cheegerHeat_L1_tendsto_nonneg line 125
8. lemma OAI.WeakHessian.CurvatureDimension.cheegerHeat_L1_tendsto line 143
9. lemma OAI.WeakHessian.CurvatureDimension.cheegerHeat_bounded_pairing_continuousOn line 182