OAI/Probability/PosteriorReplicas/Geometry/LabelEllipsoids.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.liftLabel_norm_coordinates line 11
2. lemma OAI.PosteriorReplicas.label_closedBall_volume line 21
3. lemma OAI.PosteriorReplicas.label_closedBall_scale line 29
4. lemma OAI.PosteriorReplicas.label_ellipsoid_volume line 35
5. lemma OAI.PosteriorReplicas.label_ellipsoid_translate_volume line 52
6. lemma OAI.PosteriorReplicas.projectedDensity_support_ellipsoid line 61
7. lemma OAI.PosteriorReplicas.projectedDensity_support_volume line 67
8. lemma OAI.PosteriorReplicas.gaussian_integrable_gramVolume line 74
9. lemma OAI.PosteriorReplicas.gaussian_label_support_volume_finite line 84