OAI/NumberTheory/DukePrimeDegree/Geometry/SublinearHeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Sublinear growth of a height with bounded upward increments

A high endpoint forces a long preceding interval in a high-level set. The maximal occupation bound therefore makes every positive linear slope an eventual upper bound. The height itself need not be integrable.

  1. lemma OAI.DukePrimeDegree.height_iterate_le line 19
  2. lemma OAI.DukePrimeDegree.height_endpoint_visit_bound line 28
  3. theorem OAI.DukePrimeDegree.ae_height_affine_bound line 57