OAI/NumberTheory/CubicMoment/Estimates/NoncubePoissonIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded dyadic sum is the literal noncube part of the lattice Poisson identity. No frequency terms or coprimality conditions are dropped.

  1. theorem OAI.CubicFirstMoment.noncubePoissonContribution_lattice line 13