OAI/Geometry/WeakHessian/LocalBounds/Smul.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.FiniteOnBoundedSets.of_le_smul line 53
2. lemma OAI.WeakHessian.LocalGradientParallelogram.change_measure line 60
3. lemma OAI.WeakHessian.exponentialMeasure_neg line 74
4. lemma OAI.WeakHessian.IsLaplacian.congr_ae line 90
5. lemma OAI.WeakHessian.IsLaplacian.of_exponentialMeasure line 101
6. lemma OAI.WeakHessian.inLaplacianDomain_exponentialMeasure_iff line 120