OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingSelectionData.lean

The actual sets used for the low-entropy shearing argument

The constants are fixed for this application. The two maximal estimates, Lusin continuity, small central leaf mass, arithmetic freeness and leaf regularity are all supplied by proved results. In particular the source set has positive measure, so the neutral return theorem applies to it.