OAI/NumberTheory/DukePrimeDegree/Entropy/RareTernaryEntropy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Entropy of a rare three-valued increment

When a three-valued increment is usually the middle value, its entropy is bounded by binary entropy plus the exceptional mass times log 2. The bound tends to zero with the exceptional mass.

  1. lemma OAI.DukePrimeDegree.negMulLog_pair_le line 18
  2. def OAI.DukePrimeDegree.rareTernaryCost line 36
  3. lemma OAI.DukePrimeDegree.continuous_rareTernaryCost line 39
  4. lemma OAI.DukePrimeDegree.rareTernaryCost_zero line 43
  5. lemma OAI.DukePrimeDegree.finiteShannon_ternary_le line 46
  6. lemma OAI.DukePrimeDegree.observationEntropy_ternary_le line 57
  7. lemma OAI.DukePrimeDegree.rareTernaryCost_small line 77