OAI/InformationTheory/SoftChannel/Model.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SoftChannel204.Cube line 10

    Also declared: ComparatorChallenges/SoftChannel204.lean:11 (same declaration text).

  2. def OAI.SoftChannel204.sign line 12

    Also declared: ComparatorChallenges/SoftChannel204.lean:13 (same declaration text).

  3. def OAI.SoftChannel204.avg line 14

    Also declared: ComparatorChallenges/SoftChannel204.lean:15 (same declaration text).

  4. def OAI.SoftChannel204.L line 16

    Also declared: ComparatorChallenges/SoftChannel204.lean:17 (same declaration text).

  5. def OAI.SoftChannel204.psi line 18

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

  6. def OAI.SoftChannel204.H line 21

    Also declared: ComparatorChallenges/SoftChannel204.lean:22 (same declaration text).

  7. def OAI.SoftChannel204.info line 23

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

  8. def OAI.SoftChannel204.psiInv line 25

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

  9. def OAI.SoftChannel204.kernel line 27

    Also declared: ComparatorChallenges/SoftChannel204.lean:28 (same declaration text).

  10. def OAI.SoftChannel204.noise line 30

    Also declared: ComparatorChallenges/SoftChannel204.lean:31 (same declaration text).

  11. def OAI.SoftChannel204.Closed line 33

    Also declared: ComparatorChallenges/SoftChannel204.lean:34 (same declaration text).

  12. def OAI.SoftChannel204.Interior line 35

    Also declared: ComparatorChallenges/SoftChannel204.lean:36 (same declaration text).

  13. def OAI.SoftChannel204.softCoordinate line 37

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

  14. def OAI.SoftChannel204.flip line 39

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

  15. def OAI.SoftChannel204.numberOperator line 41

    Also declared: ComparatorChallenges/SoftChannel204.lean:42 (same declaration text).

  16. def OAI.SoftChannel204.production line 44

    Also declared: ComparatorChallenges/SoftChannel204.lean:45 (same declaration text).

  17. def OAI.SoftChannel204.F line 48

    Source documentation

    Defined by this formula on [0, L); no finite endpoint value at L is asserted.

    Also declared: ComparatorChallenges/SoftChannel204.lean:49 (same declaration text).

    def F (s : ℝ) : ℝ := psiInv s * Real.artanh (psiInv s)

    Mentions: OAI.SoftChannel204.psiInv

  18. def OAI.SoftChannel204.S line 51

    Source documentation

    The excess F s - 2 * s, used for s < L, is extended by zero to negative arguments.

    Also declared: ComparatorChallenges/SoftChannel204.lean:52 (same declaration text).

    def S (s : ℝ) : ℝ := if s < 0 then 0 else F s - 2 * s

    Mentions: OAI.SoftChannel204.F

  19. def OAI.SoftChannel204.reserve line 54

    Source documentation

    The reserve is used for |m| < 1 and 0 ≤ I < H m.

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

    def reserve (m I : ℝ) : ℝ :=
…
  20. def OAI.SoftChannel204.hybrid line 57

    Also declared: ComparatorChallenges/SoftChannel204.lean:58 (same declaration text).

  21. def OAI.SoftChannel204.softJoint line 59

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

  22. def OAI.SoftChannel204.boolJoint line 62

    Also declared: ComparatorChallenges/SoftChannel204.lean:63 (same declaration text).

  23. def OAI.SoftChannel204.leftMarginal line 65

    Also declared: ComparatorChallenges/SoftChannel204.lean:66 (same declaration text).

  24. def OAI.SoftChannel204.rightMarginal line 67

    Also declared: ComparatorChallenges/SoftChannel204.lean:68 (same declaration text).

  25. def OAI.SoftChannel204.mutualInformation line 69

    Also declared: ComparatorChallenges/SoftChannel204.lean:70 (same declaration text).

  26. def OAI.SoftChannel204.binaryEntropyBits line 73

    Also declared: ComparatorChallenges/SoftChannel204.lean:74 (same declaration text).

  27. def OAI.SoftChannel204.SoftContraction line 76

    Also declared: ComparatorChallenges/SoftChannel204.lean:77 (same declaration text).

  28. def OAI.SoftChannel204.SoftAttainment line 80

    Also declared: ComparatorChallenges/SoftChannel204.lean:81 (same declaration text).

  29. def OAI.SoftChannel204.SoftInformationIdentity line 85

    Also declared: ComparatorChallenges/SoftChannel204.lean:86 (same declaration text).

  30. def OAI.SoftChannel204.RefinedBoolean line 89

    Also declared: ComparatorChallenges/SoftChannel204.lean:90 (same declaration text).

  31. def OAI.SoftChannel204.BooleanAttainment line 97

    Also declared: ComparatorChallenges/SoftChannel204.lean:98 (same declaration text).

  32. def OAI.SoftChannel204.BitsConversion line 102

    Also declared: ComparatorChallenges/SoftChannel204.lean:103 (same declaration text).

  33. def OAI.SoftChannel204.SharpProduction line 107

    Also declared: ComparatorChallenges/SoftChannel204.lean:108 (same declaration text).

  34. def OAI.SoftChannel204.FullMain line 110

    Also declared: ComparatorChallenges/SoftChannel204.lean:111 (same declaration text).