OAI/NumberTheory/DukePrimeDegree/Geometry/RegularLusinSets.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Regular Lusin sets and regular maximal-inequality base points

Removing the single regularity null set from the base-point good set does not change its measure bound. The compact Lusin set can avoid that null set and any additional prescribed null set at the same time.

  1. def OAI.DukePrimeDegree.RootLeafRegular line 21
  2. theorem OAI.DukePrimeDegree.exists_regular_lusin_rootLeaf_good_set line 33