OAI/NumberTheory/CubicMoment/Estimates/DivisorNoncubeIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The estimated divisor dyads are exactly the noncube part of the full lattice Poisson sum, with the cube test at d*h.

  1. lemma OAI.CubicFirstMoment.summable_finiteDivisorPoisson_singleton line 13
  2. lemma OAI.CubicFirstMoment.tsum_divisor_noncube_dyads line 36
  3. theorem OAI.CubicFirstMoment.divisorNoncubePoissonContribution_lattice line 67