OAI/InformationTheory/BooleanNoise/Model.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LeanBlast.CourtadeKumar.Cube line 12

    Also declared: ComparatorChallenges/CourtadeKumar.lean:19 (same declaration text).

  2. def OAI.LeanBlast.CourtadeKumar.cubeAverage line 14

    Also declared: ComparatorChallenges/CourtadeKumar.lean:21 (same declaration text).

  3. def OAI.LeanBlast.CourtadeKumar.ell line 17

    Also declared: ComparatorChallenges/CourtadeKumar.lean:24 (same declaration text).

  4. def OAI.LeanBlast.CourtadeKumar.bitFlipKernel line 19

    Also declared: ComparatorChallenges/CourtadeKumar.lean:26 (same declaration text).

  5. def OAI.LeanBlast.CourtadeKumar.jointProbability line 22

    Also declared: ComparatorChallenges/CourtadeKumar.lean:29 (same declaration text).

  6. def OAI.LeanBlast.CourtadeKumar.functionMarginal line 25

    Also declared: ComparatorChallenges/CourtadeKumar.lean:32 (same declaration text).

  7. def OAI.LeanBlast.CourtadeKumar.observationMarginal line 28

    Also declared: ComparatorChallenges/CourtadeKumar.lean:35 (same declaration text).

  8. def OAI.LeanBlast.CourtadeKumar.xlogx line 31

    Also declared: ComparatorChallenges/CourtadeKumar.lean:38 (same declaration text).

  9. def OAI.LeanBlast.CourtadeKumar.binaryEntropy line 33

    Also declared: ComparatorChallenges/CourtadeKumar.lean:40 (same declaration text).

  10. def OAI.LeanBlast.CourtadeKumar.mutualInformation line 36

    Also declared: ComparatorChallenges/CourtadeKumar.lean:43 (same declaration text).

  11. def OAI.LeanBlast.CourtadeKumar.dictator line 44

    Also declared: ComparatorChallenges/CourtadeKumar.lean:51 (same declaration text).

  12. def OAI.LeanBlast.CourtadeKumar.complementDictator line 46

    Also declared: ComparatorChallenges/CourtadeKumar.lean:53 (same declaration text).

  13. def OAI.LeanBlast.CourtadeKumar.CourtadeKumarStatement line 48

    Also declared: ComparatorChallenges/CourtadeKumar.lean:55 (same declaration text).

  14. def OAI.LeanBlast.CourtadeKumar.DictatorAttainmentStatement line 53

    Also declared: ComparatorChallenges/CourtadeKumar.lean:60 (same declaration text).

  15. def OAI.LeanBlast.CourtadeKumar.FullStatement line 60

    Also declared: ComparatorChallenges/CourtadeKumar.lean:67 (same declaration text).