OAI/NumberTheory/DukePrimeDegree/Entropy/CompactFutureLifts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Consistent small lifts of compact future itineraries

On an orbit staying in a compact set, sufficiently fine finite observations force the small relative lifts to evolve by diagonal conjugation. Boundedness then excludes every expanding matrix entry.

  1. lemma OAI.DukePrimeDegree.small_future_lifts_conjugate line 20
  2. theorem OAI.DukePrimeDegree.exists_observation_with_bounded_future_lift line 44
  3. theorem OAI.DukePrimeDegree.exists_observation_with_upper_triangular_future_lift line 106