OAI/NumberTheory/DukePrimeDegree/Dynamics/ForwardOrbitSection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A complete orbit section is visited in the future almost everywhere

Finite measure turns the forward saturation of a set into an invariant set modulo null sets. No ergodicity assumption is needed.

  1. lemma OAI.DukePrimeDegree.ae_future_visits_of_orbit_section line 19