OAI/NumberTheory/CubicMoment/Estimates/SmallBPoissonTotal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete nonzero Poisson series for arbitrary dyadic squarefree coefficients in the small-B range, including its actual infinite tail.

  1. theorem OAI.CubicFirstMoment.smallB_poisson_total_height_power line 13