OAI/Probability/SKSupport/Diffusion/BoundedDiffusionProperties.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.progressive_measurable_at line 16
2. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_adapted line 23
3. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_measurable line 28
4. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_integrable line 32
5. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_continuous_ae line 44
6. def OAI.ZeroTemperatureSK.BoundedLipschitzDrift.pathDrift line 48
7. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.pathDrift_measurable line 51
8. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.pathDrift_bound line 57
9. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.pathDrift_integrable line 59
10. def OAI.ZeroTemperatureSK.BoundedLipschitzDrift.displacement line 66
11. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.displacement_measurable line 68
12. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.displacement_bound line 71
13. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_increment line 77