Statement of the main short-sum estimate

This module records the proposition and the uniformity of its constants. LeanPool.NairTenenbaum.Results.TheoremOne proves it as NairTenenbaum.theoremOne; importing this statement module alone does not import that proof. The scope is recorded in README.md.

def NairTenenbaum.TheoremOne : Prop

Theorem 1, equation (18). c₀ is independent of the polynomial coefficients and discriminant. The implicit constant depends on D but not on the remaining polynomial data or on the arithmetic function. Parameters preceding ∃ may influence both constants.

Equations

• One or more equations did not get rendered due to their size.