OAI/Probability/SKSupport/Diffusion/StepDrift.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.WeakIto.stepDrift line 16
2. def OAI.ZeroTemperatureSK.WeakIto.stepCost line 19
3. lemma OAI.ZeroTemperatureSK.WeakIto.bounded_control_intervalIntegrable line 22
4. lemma OAI.ZeroTemperatureSK.WeakIto.stepDrift_measurable line 38
5. lemma OAI.ZeroTemperatureSK.WeakIto.stepCost_measurable line 45
6. lemma OAI.ZeroTemperatureSK.WeakIto.stepDrift_bound line 53
7. lemma OAI.ZeroTemperatureSK.WeakIto.stepCost_bound line 67
8. lemma OAI.ZeroTemperatureSK.WeakIto.stepDrift_integrable line 79
9. lemma OAI.ZeroTemperatureSK.WeakIto.stepCost_integrable line 87
10. lemma OAI.ZeroTemperatureSK.WeakIto.step_completion_square line 95