OAI/NumberTheory/DukePrimeDegree/Dynamics/BoundedReturnCompactSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded section returns force compact support

This is the compact case in the return-partition construction: if a relatively compact section has essentially bounded positive return time, its finitely many translates support the whole ergodic measure.

  1. theorem OAI.DukePrimeDegree.ae_mem_bounded_return_translates line 17
  2. theorem OAI.DukePrimeDegree.exists_compact_support_of_bounded_returns line 52