OAI/Probability/PosteriorReplicas/Information/ConditionalPiKL.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.coordKernel line 17
2. instance OAI.PosteriorReplicas.coordKernel_markov line 18
3. lemma OAI.PosteriorReplicas.coordKernel_apply line 22
4. def OAI.PosteriorReplicas.conditionalTotalCorrelation line 25
5. lemma OAI.PosteriorReplicas.conditionalTotalCorrelation_integral line 29
6. lemma OAI.PosteriorReplicas.klDiv_conditional_pi_decomposition line 37
7. lemma OAI.PosteriorReplicas.conditionalTotalCorrelation_identity line 58
8. lemma OAI.PosteriorReplicas.marginalProduct_map line 79
9. lemma OAI.PosteriorReplicas.conditionalTotalCorrelation_map_le line 93