OAI/Probability/PosteriorReplicas/Kernels/PosteriorKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.measurable_tiltedFiber line 11
2. def OAI.PosteriorReplicas.posteriorKernel line 30
3. lemma OAI.PosteriorReplicas.posteriorKernel_markov line 35
4. def OAI.PosteriorReplicas.dataLaw line 40
5. instance OAI.PosteriorReplicas.(instance at line 43) line 43
6. lemma OAI.PosteriorReplicas.posterior_disintegration_lintegral line 48
7. lemma OAI.PosteriorReplicas.dataLaw_density line 74