OAI/NumberTheory/DukePrimeDegree/Geometry/LeafCompactMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform short-interval maximal estimates on compact sets

The root-box estimate and a finite cover of a compact set give one positive radius and one finite constant, uniformly over all finite ambient measures with essentially free root action.

  1. theorem OAI.DukePrimeDegree.compact_intrinsic_maximal_bound line 20