OAI/Probability/PosteriorReplicas/Measures/EuclideanLabels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.euclideanLabelLaw line 10
2. instance OAI.PosteriorReplicas.(instance at line 13) line 13
3. lemma OAI.PosteriorReplicas.euclidean_map_density line 16
4. lemma OAI.PosteriorReplicas.euclideanLabelLaw_density line 30
5. lemma OAI.PosteriorReplicas.euclideanLabelLaw_ball line 44
6. lemma OAI.PosteriorReplicas.euclidean_label_ball_volume line 51
7. lemma OAI.PosteriorReplicas.projectedDensity_uniform_bound line 61
8. lemma OAI.PosteriorReplicas.ae_ballDensityVersion line 67