OAI/NumberTheory/DukePrimeDegree/Geometry/LeafBoundedMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A maximal bound uniform in the time window

Diagonal invariance rescales any bounded family of witnessing intervals into the short-time estimate. Its constant is independent of the bound on those intervals.

  1. theorem OAI.DukePrimeDegree.bounded_interval_intrinsic_maximal_bound line 20