OAI/NumberTheory/CubicMoment/Decomposition/StoppedPoissonTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Absolute control after the stopped-row frequency cutoff b^(3/5). At A≥b^(3/2) this is a positive power beyond the natural Poisson scale; the inverse powers of A make the bound valid without an upper A limit.

  1. lemma OAI.CubicFirstMoment.stopped_poisson_cutoff line 13
  2. lemma OAI.CubicFirstMoment.stopped_poisson_cutoff_scale line 28
  3. lemma OAI.CubicFirstMoment.stopped_poisson_tail_scale line 53
  4. theorem OAI.CubicFirstMoment.stopped_poisson_tail_power line 106