OAI/Probability/SKRatio/Matrices/PathEvaluations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.PathBridge.pathEvaluations line 13
2. lemma OAI.SKRatioGaussian.PathBridge.measurableEmbedding_pathEvaluations line 14
3. def OAI.SKRatioGaussian.PathBridge.continuousPathVersion line 26
4. lemma OAI.SKRatioGaussian.PathBridge.continuousPathVersion_eval line 30
5. lemma OAI.SKRatioGaussian.PathBridge.aemeasurable_continuousPathVersion line 36
6. lemma OAI.SKRatioGaussian.PathBridge.gaussian_continuousPathVersion line 45
7. lemma OAI.SKRatioGaussian.PathBridge.mean_continuousPathVersion line 63
8. theorem OAI.SKRatioGaussian.PathBridge.continuous_gaussian_process_fernique line 72
9. def OAI.SKRatioGaussian.PathBridge.unitBrownianProcess line 86
10. lemma OAI.SKRatioGaussian.PathBridge.brownian_unit_gaussian line 89
11. lemma OAI.SKRatioGaussian.PathBridge.brownian_unit_continuous line 93
12. theorem OAI.SKRatioGaussian.PathBridge.brownian_unit_fernique line 99