OAI/NumberTheory/DukePrimeDegree/Geometry/RowLongBoxes.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Row-root boxes around arbitrary compact orbit pieces

Almost every lattice has a free row-group orbit. Every compact piece of such an orbit therefore lies in one row-root box, by the local covering map and the compact tube lemma. This allows conditional measures from bounded boxes to be compared on arbitrarily large leaf neighborhoods.

  1. lemma OAI.DukePrimeDegree.rowRoot_injective line 22
  2. theorem OAI.DukePrimeDegree.ae_rowRoot_stabilizer_trivial line 30
  3. lemma OAI.DukePrimeDegree.rowQuotientParametrization_injective_of_free line 43
  4. theorem OAI.DukePrimeDegree.rowRootBox_contains_compact_time line 57
  5. theorem OAI.DukePrimeDegree.rowRootBox_arbitrary_compact_of_free line 78