OAI/NumberTheory/CubicMoment/Estimates/SparseCenteredBilinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The centered sparse late-stop contribution. Both its Gauss part and its squarefree model are proved small; the norm range supplies the cubic-sieve geometry.

  1. theorem OAI.CubicFirstMoment.ordinary_sparse_centered_bilinear line 17