OAI/Probability/PosteriorReplicas/Measures/BaseDisintegration.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PosteriorReplicas.baseLaw_probability line 11
2. lemma OAI.PosteriorReplicas.measurable_baseDensity line 19
3. lemma OAI.PosteriorReplicas.measurable_projectedDensity line 33
4. lemma OAI.PosteriorReplicas.baseDensity_lt_top line 38
5. lemma OAI.PosteriorReplicas.baseDensity_spherical line 42
6. lemma OAI.PosteriorReplicas.base_lintegral line 48
7. lemma OAI.PosteriorReplicas.weighted_base_lintegral line 78
8. lemma OAI.PosteriorReplicas.tiltMass_le line 86
9. lemma OAI.PosteriorReplicas.tiltMass_ne_top line 93
10. lemma OAI.PosteriorReplicas.projectedDensity_ne_top line 97
11. lemma OAI.PosteriorReplicas.weighted_fiber_labels line 102
12. lemma OAI.PosteriorReplicas.projected_measure line 114