OAI/NumberTheory/DukePrimeDegree/Geometry/LeafGoodSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Large good sets for all leafwise radii

For a sufficiently small exceptional ambient set, almost every base point sees only a prescribed small fraction of that set in every centered root interval. This is the maximal-inequality good set used in EKL (2006), Section 4.3.

  1. theorem OAI.DukePrimeDegree.exists_large_rootLeaf_good_set line 21