OAI/Probability/SKGap/Brownian/BrownianPathFernique.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SKGap.PathBridge.UnitInterval line 12
2. abbrev OAI.SKGap.PathBridge.UnitPath line 13
3. instance OAI.SKGap.PathBridge.pathMeasurable line 14
4. instance OAI.SKGap.PathBridge.pathBorel line 15
5. def OAI.SKGap.PathBridge.pathPairEvaluations line 17
6. lemma OAI.SKGap.PathBridge.continuous_pathPairEvaluations line 20
7. lemma OAI.SKGap.PathBridge.injective_pathPairEvaluations line 26
8. lemma OAI.SKGap.PathBridge.measurableEmbedding_pathPairEvaluations line 38
9. lemma OAI.SKGap.PathBridge.centered_gaussian_path_rotation line 41
10. theorem OAI.SKGap.PathBridge.centered_gaussian_path_fernique line 76
11. def OAI.SKGap.PathBridge.pathEvaluations line 94
12. lemma OAI.SKGap.PathBridge.measurableEmbedding_pathEvaluations line 95
13. def OAI.SKGap.PathBridge.continuousPathVersion line 107
14. lemma OAI.SKGap.PathBridge.continuousPathVersion_eval line 111
15. lemma OAI.SKGap.PathBridge.aemeasurable_continuousPathVersion line 117
16. lemma OAI.SKGap.PathBridge.gaussian_continuousPathVersion line 126
17. lemma OAI.SKGap.PathBridge.mean_continuousPathVersion line 144
18. theorem OAI.SKGap.PathBridge.continuous_gaussian_process_fernique line 153
19. def OAI.SKGap.PathBridge.unitBrownianProcess line 165
20. lemma OAI.SKGap.PathBridge.brownian_unit_gaussian line 168
21. lemma OAI.SKGap.PathBridge.brownian_unit_continuous line 172
22. theorem OAI.SKGap.PathBridge.brownian_unit_fernique line 178