OAI/Probability/SKSupport/Diffusion/ProgressiveBrownian.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.leftMeshTime line 12
2. lemma OAI.ZeroTemperatureSK.leftMeshTime_le line 15
3. lemma OAI.ZeroTemperatureSK.leftMeshTime_gt line 22
4. lemma OAI.ZeroTemperatureSK.leftMeshTime_tendsto line 31
5. lemma OAI.ZeroTemperatureSK.leftMesh_progressive line 41
6. def OAI.ZeroTemperatureSK.BrownianSystem.progressiveVersion line 67
7. lemma OAI.ZeroTemperatureSK.BrownianSystem.progressiveVersion_progressive line 70
8. lemma OAI.ZeroTemperatureSK.BrownianSystem.progressiveVersion_eq line 84
9. lemma OAI.ZeroTemperatureSK.BrownianSystem.progressiveVersion_indistinguishable line 88
10. def OAI.ZeroTemperatureSK.BrownianSystem.driver line 93
11. lemma OAI.ZeroTemperatureSK.BrownianSystem.driver_progressive line 96
12. lemma OAI.ZeroTemperatureSK.BrownianSystem.driver_zero line 104
13. lemma OAI.ZeroTemperatureSK.BrownianSystem.driver_indistinguishable line 106
14. lemma OAI.ZeroTemperatureSK.BrownianSystem.driver_continuous line 111