OAI/Probability/PosteriorReplicas/Measures/ConstrainedDensityExpectation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.volume_labels_smul line 12
2. lemma OAI.PosteriorReplicas.gaussian_rows_inner_le_volume line 21
3. lemma OAI.PosteriorReplicas.projected_rows_ball_bound line 30
4. lemma OAI.PosteriorReplicas.label_ball_pos line 48
5. lemma OAI.PosteriorReplicas.label_ball_ne_top line 53
6. lemma OAI.PosteriorReplicas.expected_ballDensityVersion_le line 59