OAI/NumberTheory/DukePrimeDegree/Entropy/RareLabelEntropy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The entropy cost of rare observation errors

This finite-label estimate converts small boundary-visit frequencies into a small entropy cost for the neutral orbit covers.

  1. def OAI.DukePrimeDegree.rareLabelCost line 19
  2. theorem OAI.DukePrimeDegree.rareLabelCost_small line 22
  3. theorem OAI.DukePrimeDegree.finiteShannon_option_le line 50
  4. theorem OAI.DukePrimeDegree.observationEntropy_option_le line 94
  5. def OAI.DukePrimeDegree.observationError line 105
  6. theorem OAI.DukePrimeDegree.conditionalObservationEntropy_le_error line 108