OAI/Probability/SKRatio/Matrices/UnitInterval.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SKRatioGaussian.PathBridge.UnitInterval line 11
2. abbrev OAI.SKRatioGaussian.PathBridge.UnitPath line 12
3. instance OAI.SKRatioGaussian.PathBridge.pathMeasurable line 13
4. instance OAI.SKRatioGaussian.PathBridge.pathBorel line 14
5. def OAI.SKRatioGaussian.PathBridge.pathPairEvaluations line 16
6. lemma OAI.SKRatioGaussian.PathBridge.continuous_pathPairEvaluations line 19
7. lemma OAI.SKRatioGaussian.PathBridge.injective_pathPairEvaluations line 25
8. lemma OAI.SKRatioGaussian.PathBridge.measurableEmbedding_pathPairEvaluations line 37
9. lemma OAI.SKRatioGaussian.PathBridge.centered_gaussian_path_rotation line 40
10. theorem OAI.SKRatioGaussian.PathBridge.centered_gaussian_path_fernique line 75