OAI/Probability/PosteriorReplicas/Gaussian/GaussianPolar.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.gaussianRadialDensity line 13
2. lemma OAI.PosteriorReplicas.continuous_gaussianRadialDensity line 16
3. lemma OAI.PosteriorReplicas.stdGaussian_density line 20
4. lemma OAI.PosteriorReplicas.stdGaussian_absolutelyContinuous_volume line 46
5. lemma OAI.PosteriorReplicas.stdGaussian_singleton_eq_zero line 50
6. def OAI.PosteriorReplicas.gaussianPolarRadius line 53
7. instance OAI.PosteriorReplicas.(instance at line 58) line 58
8. lemma OAI.PosteriorReplicas.gaussian_polar line 62
9. lemma OAI.PosteriorReplicas.gaussian_polar_reconstruction line 90
10. lemma OAI.PosteriorReplicas.gaussian_polar_mass line 104
11. lemma OAI.PosteriorReplicas.gaussianPolarRadius_mass line 110
12. instance OAI.PosteriorReplicas.(instance at line 118) line 118
13. def OAI.PosteriorReplicas.normalDirection line 124
14. lemma OAI.PosteriorReplicas.measurable_normalDirection line 126
15. def OAI.PosteriorReplicas.uniformDirection line 130
16. lemma OAI.PosteriorReplicas.normalDirection_smul_sphere line 136
17. lemma OAI.PosteriorReplicas.gaussian_normalDirection line 141
18. instance OAI.PosteriorReplicas.(instance at line 155) line 155