OAI/NumberTheory/CubicMoment/Estimates/NarrowPrimeBinCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform bin counts when the geometric ratio is allowed to approach one. The width loss is explicit, as required for logarithmic stopping bins.

  1. lemma OAI.CubicFirstMoment.logarithm_one_add_lower line 10
  2. theorem OAI.CubicFirstMoment.geometricBinCount_width_bound line 16