OAI/Probability/SKValue/Processes/DiffusionExistence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.terminalEulerProcess line 10
2. def OAI.SKValue.diffusionProcess line 12
3. lemma OAI.SKValue.terminalEulerProcess_measurable line 14
4. lemma OAI.SKValue.diffusionProcess_measurable line 22
5. lemma OAI.SKValue.diffusionProcess_adapted line 31
6. lemma OAI.SKValue.diffusionProcess_path line 37
7. theorem OAI.SKValue.diffusionProcess_isDiffusion line 74
8. lemma OAI.SKValue.exists_diffusion line 78