OAI/NumberTheory/DukePrimeDegree/Geometry/LeafBoxMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic leaf maximal inequality inside root boxes

A measurable set of points witnessing a bad intrinsic leaf interval has small ambient measure, provided the witnessing interval stays in the root box. The constant is independent of the box and ambient measure.

  1. theorem OAI.DukePrimeDegree.exists_intrinsic_rootBox_maximal_constant line 20