OAI/Geometry/WeakHessian/Sobolev/GlobalCheegerEnergyReal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.CurvatureDimension.global_cheegerEnergy_toReal line 49
2. lemma OAI.WeakHessian.CurvatureDimension.global_integral_gamma_eq line 61
3. lemma OAI.WeakHessian.CurvatureDimension.global_integral_gamma_form line 74
4. lemma OAI.WeakHessian.CurvatureDimension.global_formGenerator_of_isLaplacian line 93
5. lemma OAI.WeakHessian.CurvatureDimension.global_isLaplacian_of_formGenerator line 107
6. lemma OAI.WeakHessian.CurvatureDimension.global_isLaplacian_iff_formGenerator line 134