OAI/Geometry/WeakHessian/LocalBounds/CoreAlgebra.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsLaplacian.unique line 20
2. lemma OAI.WeakHessian.laplacian_isLaplacian line 42
3. lemma OAI.WeakHessian.IsLaplacian.ae_laplacian line 48
4. lemma OAI.WeakHessian.laplacian_congr_ae line 52
5. def OAI.WeakHessian.integratedBochner line 66
6. def OAI.WeakHessian.driftBochner line 70
7. lemma OAI.WeakHessian.driftBochner_eq_sub_hessian line 77
8. lemma OAI.WeakHessian.weakHessian_const_mul line 171
9. lemma OAI.WeakHessian.WeakHessianUpperBound.core_dual line 204
10. lemma OAI.WeakHessian.WeakHessianUpperBound.core_integrated line 235