OAI/Probability/SKSupport/Regularity/IntegralTimeStep.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.WeakIto.BoundedSmoothFamily_lipschitz line 15
2. lemma OAI.ZeroTemperatureSK.WeakIto.time_integral_spatial_bound line 22
3. lemma OAI.ZeroTemperatureSK.WeakIto.integrable_family_comp line 35
4. lemma OAI.ZeroTemperatureSK.WeakIto.measurable_family_integral line 42
5. lemma OAI.ZeroTemperatureSK.WeakIto.integrable_family_integral_comp line 47
6. lemma OAI.ZeroTemperatureSK.WeakIto.expected_integral_time_step line 56
7. lemma OAI.ZeroTemperatureSK.WeakIto.time_average_bound line 141
8. lemma OAI.ZeroTemperatureSK.WeakIto.time_average_tendsto_right line 149
9. lemma OAI.ZeroTemperatureSK.WeakIto.measurable_time_integral line 163
10. lemma OAI.ZeroTemperatureSK.WeakIto.expected_time_average_tendsto_right line 171