OAI/NumberTheory/DukePrimeDegree/Entropy/PredecessorEntropyLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The entropy upper bound from finite predecessor symbols

The countable terminal label has sublinear information cost. A finite conditional chain rule and Cesaro convergence control every clipped rate.

  1. theorem OAI.DukePrimeDegree.predecessor_word_conditional_rate line 17
  2. theorem OAI.DukePrimeDegree.predecessor_clipped_entropyRate_le line 43
  3. theorem OAI.DukePrimeDegree.finite_predecessors_entropy_upper line 65