OAI/Probability/PosteriorReplicas/Information/RandomProjectionInformation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.measurable_projected_totalCorrelation line 16
2. lemma OAI.PosteriorReplicas.random_replica_information_le_entropy line 40
3. lemma OAI.PosteriorReplicas.random_replica_information_identical line 53
4. lemma OAI.PosteriorReplicas.conditionalInformation_eq_cmi line 72
5. lemma OAI.PosteriorReplicas.sideLaw_eq_randomSideLaw line 76
6. lemma OAI.PosteriorReplicas.messageEntropy_eq_finiteEntropy line 79