OAI/NumberTheory/DukePrimeDegree/Geometry/LeafClosedRadius.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurable small-ball good sets

Nonatomic root leaves admit a common small closed-ball radius outside a measurable set of arbitrarily small measure. Pointwise agreement with the intrinsic leaves is obtained by removing one measurable null set.

  1. theorem OAI.DukePrimeDegree.exists_rootLeaf_closedBall_good_set line 20