OAI/Probability/PosteriorReplicas/Information/GraphKL.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.klDiv_map_leftInverse line 10
2. lemma OAI.PosteriorReplicas.compProd_prod_right line 19
3. def OAI.PosteriorReplicas.attachSide line 29
4. instance OAI.PosteriorReplicas.attachSide_finite line 33
5. lemma OAI.PosteriorReplicas.attachSide_probability line 39
6. lemma OAI.PosteriorReplicas.attachSide_first_pair line 44
7. lemma OAI.PosteriorReplicas.compProd_condKernel_fst line 51
8. lemma OAI.PosteriorReplicas.attachSide_conditional_reference line 59
9. lemma OAI.PosteriorReplicas.mutualInformation_attachSide_chain line 77