OAI/NumberTheory/DukePrimeDegree/Geometry/LeafLusinGoodSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Lusin sets with uniform leafwise return control

The compact Lusin set and the maximal-inequality good set can be chosen together. This supplies the two large sets used to select shearing returns in EKL (2006), Section 4.3.

  1. theorem OAI.DukePrimeDegree.exists_compact_lusin_and_rootLeaf_good_set line 20