OAI/NumberTheory/CubicMoment/Estimates/NoncubePoissonTotal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full noncube Poisson contribution: the bounded-conductor proof and the actual infinite high-frequency tail give the full contribution.

  1. def OAI.CubicFirstMoment.noncubePoissonContribution line 15
  2. theorem OAI.CubicFirstMoment.noncube_poisson_total_saving line 20