OAI/NumberTheory/DukePrimeDegree/Geometry/LeafMeasurableBad.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measurable bad sets for intrinsic leaf averages

Strict bad inequalities at rational radii define a measurable set. Its complement controls every real radius, by continuity from above. The diagonal scaling estimate bounds this set uniformly over all radii.

  1. def OAI.DukePrimeDegree.rootHitTimes line 20
  2. lemma OAI.DukePrimeDegree.measurableSet_rootHitTimes line 24
  3. lemma OAI.DukePrimeDegree.measurable_rootHitMass line 29
  4. def OAI.DukePrimeDegree.rootRationalBad line 40
  5. lemma OAI.DukePrimeDegree.measurableSet_rootRationalBad line 45
  6. theorem OAI.DukePrimeDegree.all_radii_rootRationalBad_bound line 61
  7. theorem OAI.DukePrimeDegree.rootRationalBad_compl_all_radii line 91