OAI/NumberTheory/DukePrimeDegree/Dynamics/ErgodicReturnLevels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Visiting arbitrarily high positive return levels

This is the ergodic case of the recurrent-section construction. The ergodicity premise is explicit here and is not added to the packet theorem.

  1. lemma OAI.DukePrimeDegree.ae_future_visit_of_positive line 15
  2. theorem OAI.DukePrimeDegree.ae_visits_unbounded_return_levels line 37