OAI/NumberTheory/DukePrimeDegree/Geometry/LeafPairSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous compact returns on equal root leaves

The all-radius good-set estimate controls both exceptional time sets with the same leaf measure. A third small forbidden set can be removed while retaining a common return time.

  1. lemma OAI.DukePrimeDegree.exists_common_point_outside_forbidden line 20
  2. theorem OAI.DukePrimeDegree.exists_simultaneous_root_return line 37