OAI/NumberTheory/DukePrimeDegree/Entropy/PredecessorSymbols.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite symbol recovers a countable label from its successor

A uniform finite predecessor bound replaces an unbounded observation by a finite symbol once its next countable label is known.

  1. theorem OAI.DukePrimeDegree.exists_finite_predecessor_observation line 15
  2. lemma OAI.DukePrimeDegree.predecessor_word_recovers line 51