OAI/NumberTheory/DukePrimeDegree/Geometry/LeafShortMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Short-interval maximal control with a small exceptional set

Inner regularity and the compact-set estimate give uniform relative maximal control at sufficiently short times. The error is the measure of the complement of a large compact set.

  1. theorem OAI.DukePrimeDegree.short_interval_intrinsic_maximal_bound line 20