OAI/NumberTheory/CubicMoment/Estimates/HuxleySchur.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The finite Schur estimate used for the Gaussian additive-sieve kernel.
- lemma
OAI.CubicFirstMoment.huxley_finite_schurline 10