OAI/Probability/PosteriorReplicas/Information/ReplicaInformation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PosteriorReplicas.mutualInformation line 12
  2. def OAI.PosteriorReplicas.totalCorrelation line 15
  3. lemma OAI.PosteriorReplicas.snd_compProd_map line 18
  4. lemma OAI.PosteriorReplicas.mutualInformation_swap line 26
  5. def OAI.PosteriorReplicas.coordinateJoint line 37
  6. instance OAI.PosteriorReplicas.coordinateJoint_probability line 40
  7. lemma OAI.PosteriorReplicas.coordinateJoint_fst line 45
  8. lemma OAI.PosteriorReplicas.coordinateJoint_snd line 51
  9. lemma OAI.PosteriorReplicas.coordinateJoint_information line 55
  10. lemma OAI.PosteriorReplicas.tuple_information_decomposition line 62
  11. lemma OAI.PosteriorReplicas.coordinateJoint_projection line 81
  12. lemma OAI.PosteriorReplicas.coordinate_information_chain line 92
  13. lemma OAI.PosteriorReplicas.replica_information_inequality line 111
  14. lemma OAI.PosteriorReplicas.replica_information_le_entropy line 141