OAI/Probability/PosteriorReplicas/Information/KLTools.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.klDiv_map_equiv line 10
2. lemma OAI.PosteriorReplicas.klDiv_swap line 18
3. lemma OAI.PosteriorReplicas.klDiv_prod_left line 23
4. lemma OAI.PosteriorReplicas.klDiv_prod_right line 29
5. lemma OAI.PosteriorReplicas.klDiv_prod_first_chain line 35
6. lemma OAI.PosteriorReplicas.klDiv_prod_decomposition line 43
7. lemma OAI.PosteriorReplicas.withDensity_kernel_rnDeriv line 64
8. lemma OAI.PosteriorReplicas.rnDeriv_compProd_kernel line 72
9. lemma OAI.PosteriorReplicas.klDiv_compProd_kernel_integral line 77
10. lemma OAI.PosteriorReplicas.measurable_kernel_klDiv line 95
11. lemma OAI.PosteriorReplicas.klDiv_compProd_kernel line 113