OAI/Probability/PosteriorReplicas/Kernels/ReplicaMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.equalReference line 10
2. instance OAI.PosteriorReplicas.(instance at line 13) line 13
3. instance OAI.PosteriorReplicas.(instance at line 18) line 18
4. def OAI.PosteriorReplicas.replicaDensity line 23
5. lemma OAI.PosteriorReplicas.measurable_replicaDensity line 28
6. def OAI.PosteriorReplicas.replicaLaw line 33
7. lemma OAI.PosteriorReplicas.equalReference_lintegral line 36
8. lemma OAI.PosteriorReplicas.density_power_cancel line 46
9. lemma OAI.PosteriorReplicas.replicaLaw_lintegral line 53
10. lemma OAI.PosteriorReplicas.lintegral_projectedDensity line 100
11. lemma OAI.PosteriorReplicas.replicaLaw_mass line 108
12. lemma OAI.PosteriorReplicas.replicaLaw_probability line 122