OAI/Geometry/WeakHessian/LocalBounds/ExpMulLp.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.sq_exp_eq line 54
2. lemma OAI.WeakHessian.IsLaplacian.davies_form line 57
3. def OAI.WeakHessian.expMulLp line 117
4. lemma OAI.WeakHessian.expMulLp_ae line 122
5. lemma OAI.WeakHessian.expMulLp_inner line 126
6. lemma OAI.WeakHessian.expMulLp_norm_sq line 135
7. lemma OAI.WeakHessian.CurvatureDimension.cheegerHeat_davies_generator line 143