OAI/NumberTheory/DukePrimeDegree/Dynamics/CompactFlowReturns.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact simultaneous returns outside a prescribed null set

A summable sequence of maximal-inequality exceptional sets gives one conull set on which any two points return to a common compact set with uniformly positive overlap. No ergodicity of the individual flow is used.

  1. theorem OAI.DukePrimeDegree.exists_eventual_flow_good_sets line 22
  2. theorem OAI.DukePrimeDegree.exists_compact_flow_return_family line 61
  3. theorem OAI.DukePrimeDegree.exists_late_simultaneous_compact_return line 87
  4. theorem OAI.DukePrimeDegree.exists_conull_simultaneous_compact_returns line 121