OAI/Probability/PosteriorReplicas/Information/ParametricKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.parametricMapKernel line 13
2. instance OAI.PosteriorReplicas.parametricMapKernel_sfinite line 16
3. lemma OAI.PosteriorReplicas.parametricMapKernel_markov line 21
4. lemma OAI.PosteriorReplicas.parametricMapKernel_apply line 25
5. lemma OAI.PosteriorReplicas.compProd_parametricMapKernel line 33
6. def OAI.PosteriorReplicas.randomSideLaw line 51
7. instance OAI.PosteriorReplicas.randomSideLaw_finite line 55
8. lemma OAI.PosteriorReplicas.cmi_randomSideLaw line 59
9. lemma OAI.PosteriorReplicas.measurable_cmi_attachSide line 76