OAI/InformationTheory/BooleanNoise/Attainment.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_dictator line 16
  2. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_dictator line 39
  3. theorem OAI.LeanBlast.CourtadeKumar.signEncoding_complementDictator line 43
  4. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_complementDictator line 48
  5. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_complementDictator line 54
  6. theorem OAI.LeanBlast.CourtadeKumar.isSignValued_signEncoding line 58
  7. theorem OAI.LeanBlast.CourtadeKumar.entropyAverage_const line 62
  8. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_const line 66
  9. theorem OAI.LeanBlast.CourtadeKumar.entropyAverage_neg line 70
  10. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_neg line 74
  11. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_const line 78
  12. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_zero line 85
  13. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_one_le line 92
  14. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_dictator line 106
  15. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_complementDictator line 121
  16. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_dictator line 130
  17. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_complementDictator line 135
  18. theorem OAI.LeanBlast.CourtadeKumar.dictatorAttainment line 141
  19. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_zero_le line 146
  20. theorem OAI.LeanBlast.CourtadeKumar.mutualInformation_half line 153
  21. theorem OAI.LeanBlast.CourtadeKumar.courtadeKumar_zero line 158
  22. theorem OAI.LeanBlast.CourtadeKumar.courtadeKumar_half line 162