OAI/Geometry/WeakHessian/Entropy/SmoothDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.timeAverageLaw_integral line 19
2. def OAI.WeakHessian.kernelMeasure line 41
3. lemma OAI.WeakHessian.kernelMeasure_probability line 43
4. lemma OAI.WeakHessian.integral_kernelMeasure line 50
5. def OAI.WeakHessian.smoothDensity line 57
6. lemma OAI.WeakHessian.smoothDensity_eq_average line 61
7. lemma OAI.WeakHessian.locallyIntegrable_clampedDensity line 68
8. lemma OAI.WeakHessian.smoothDensity_hasDerivAt line 84
9. lemma OAI.WeakHessian.IsTestPlan.smoothDensity_properties line 91
10. lemma OAI.WeakHessian.IsTestPlan.smoothDensity_energy line 109