OAI/NumberTheory/DukePrimeDegree/Entropy/UpperRootCutItineraries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual diagonal cut itineraries contain root neighborhoods

For each logarithmic distance observable one can choose a cut with summable boundary returns. The proved matrix contraction then places a whole upper-root neighborhood in almost every infinite itinerary atom.

  1. lemma OAI.DukePrimeDegree.upperRoot_orbit_iterate_diagonal line 21
  2. theorem OAI.DukePrimeDegree.quotientLogDistance_upperRoot_iterate_bound line 34
  3. theorem OAI.DukePrimeDegree.exists_cut_with_upperRoot_itinerary_neighborhoods line 50