OAI/NumberTheory/DukePrimeDegree/Geometry/DiagonalTwoTargets.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Diagonal orbit control for both shearing target sets

The same large measurable set controls visits to the compact-return good set and the small-leaf-ball good set. Together with the common-time lemma this supplies the two-target recurrence step of EKL Lemmas 4.5 and 4.6.

  1. theorem OAI.DukePrimeDegree.exists_diagonal_two_target_control line 20
  2. theorem OAI.DukePrimeDegree.common_diagonal_two_scale_time line 43