OAI/NumberTheory/DukePrimeDegree/Dynamics/DiagonalFlowMaximal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform long-time returns for the diagonal flow

This specializes the proved maximal occupation bound to the actual canonical diagonal flow on the arithmetic quotient.

  1. lemma OAI.DukePrimeDegree.continuous_diagonalOneParameter line 19
  2. theorem OAI.DukePrimeDegree.exists_diagonal_return_good_set line 34