OAI/NumberTheory/CubicMoment/Estimates/GeometricPrimeBins.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A concrete descending geometric binning of the actual prime norms. The number of bins is logarithmic and all lower endpoints exceed one, so the exact first-crossing construction applies without empty-bin cases.

  1. def OAI.CubicFirstMoment.geometricBinCount line 12
  2. def OAI.CubicFirstMoment.geometricPrimeBin line 14
  3. def OAI.CubicFirstMoment.geometricBinLower line 17
  4. lemma OAI.CubicFirstMoment.geometricPrimeBin_index line 20
  5. lemma OAI.CubicFirstMoment.geometricBinLower_gt_one line 39
  6. lemma OAI.CubicFirstMoment.geometricPrimeBin_cell line 43
  7. theorem OAI.CubicFirstMoment.geometricBinCount_log_bound line 68