OAI/Geometry/WeakHessian/LocalBounds/GammaRepresentativePairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.BoundedLipschitzRepresentative line 19
2. lemma OAI.WeakHessian.IsLaplacian.mixed_pairing_ae line 23
3. lemma OAI.WeakHessian.IsLaplacian.square_gamma_pairing_ae line 45
4. lemma OAI.WeakHessian.RCD.weighted_heat_boundedLipschitzRepresentative line 58