OAI/Geometry/WeakHessian/Entropy/AveragedDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.timeAverageLaw line 19
2. lemma OAI.WeakHessian.continuous_timeAverageEval line 23
3. lemma OAI.WeakHessian.IsTestPlan.timeAverageLaw_le line 28
4. lemma OAI.WeakHessian.isProbabilityMeasure_timeAverageLaw line 45
5. lemma OAI.WeakHessian.integrable_shiftedDensity line 52
6. lemma OAI.WeakHessian.timeAverageLaw_density_pairing line 67
7. lemma OAI.WeakHessian.IsTestPlan.exists_timeAverageDensity line 89