OAI/NumberTheory/CubicMoment/Estimates/CubeUniformError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform cube error on a norm annulus. The first term is the lattice error; the second records the actual reciprocal-prime exclusion loss.

  1. lemma OAI.CubicFirstMoment.cube_pair_norm_bounds line 12
  2. theorem OAI.CubicFirstMoment.cubePoissonContribution_uniform_error line 25