OAI/InformationTheory/BooleanNoise/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_le_psi_of_increasing_case line 11
2. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_le_psi line 39
3. theorem OAI.LeanBlast.CourtadeKumar.courtadeKumar_bound line 47
4. theorem OAI.LeanBlast.CourtadeKumar.courtadeKumar line 56
5. theorem OAI.LeanBlast.CourtadeKumar.courtadeKumarAndAttainment line 60

   Distinct definitions of this name: ComparatorChallenges/CourtadeKumar.lean:69 (same statement text; different proof or body). Qualify references as OAI.LeanBlast.CourtadeKumar.courtadeKumarAndAttainment@path.