OAI/Probability/PosteriorReplicas/Information/FiniteKL.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.finite_ac_of_singleton line 14
2. lemma OAI.PosteriorReplicas.finite_withDensity_ratio line 22
3. lemma OAI.PosteriorReplicas.finite_llr_ratio line 31
4. lemma OAI.PosteriorReplicas.finite_klDiv_formula line 39
5. lemma OAI.PosteriorReplicas.finite_klDiv_le_crossEntropy line 46
6. lemma OAI.PosteriorReplicas.finite_crossEntropy_nonneg line 64
7. lemma OAI.PosteriorReplicas.ae_kernel_ac_marginal line 79
8. lemma OAI.PosteriorReplicas.integrable_kernel_atom line 94
9. lemma OAI.PosteriorReplicas.integral_kernel_atom line 101
10. lemma OAI.PosteriorReplicas.klDiv_kernel_le_finiteEntropy line 113
11. lemma OAI.PosteriorReplicas.mutualInformation_le_finiteEntropy line 141