OAI/InformationTheory/BooleanNoise/InformationIdentity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.sum_xlogx_signProbability line 15
  2. theorem OAI.LeanBlast.CourtadeKumar.binaryEntropy_eq_binEntropy line 24
  3. theorem OAI.LeanBlast.CourtadeKumar.one_sub_binaryEntropy_eq_psi line 30
  4. theorem OAI.LeanBlast.CourtadeKumar.joint_xlogx_sum_bool line 40
  5. theorem OAI.LeanBlast.CourtadeKumar.joint_xlogx_sum line 49
  6. theorem OAI.LeanBlast.CourtadeKumar.functionMarginal_xlogx_sum line 57
  7. theorem OAI.LeanBlast.CourtadeKumar.observationMarginal_xlogx_sum line 63
  8. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_eq_informationDeficit line 68
  9. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_nats line 83
  10. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_nats_eq_entropy line 90
  11. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_nats_eq_psi line 98