The four contribution classes in arbitrary integer intervals

noncomputable def NairTenenbaum.PolynomialSystem.integerSum {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (a b : ℤ) : ℝ

Sum over the integer interval (a,b], with zero-extension at roots.

Equations

• P.integerSum F a b = ∑ t ∈ Finset.Ioc a b, NairTenenbaum.extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs

theorem NairTenenbaum.PolynomialSystem.shortSum_eq_integerSum {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (x y : ℝ) : shortSum P.Q F x y = P.integerSum F ↑⌊x⌋₊ ↑⌊x + y⌋₊

Natural-number short sums are integer-interval sums after rounding the endpoints.

theorem NairTenenbaum.PolynomialSystem.HasSmallCrossingPrime.mem_exceptionalSet {k r : ℕ} {P : PolynomialSystem k r} {ε x : ℝ} (hε : 0 ≤ ε) (hx : 1 ≤ x) {a b t : ℤ} (ht : t ∈ Finset.Ioc a b) (H : P.HasSmallCrossingPrime ε x t) : t ∈ primePowerExceptionalSet P.R (x ^ (↑P.total.natDegree * ε / 2)) ((x ^ (↑P.total.natDegree * ε / 2)) ^ 3) a b

theorem NairTenenbaum.PolynomialSystem.HasLargeSmoothDivisorTuple.mem_exceptionalSet {k r : ℕ} {P : PolynomialSystem k r} {s : Finset ℕ} {ε x : ℝ} (hε : 0 ≤ ε) (hx : 1 ≤ x) {a b t : ℤ} (ht : t ∈ Finset.Ioc a b) (H : P.HasLargeSmoothDivisorTuple s ε x t) : t ∈ smoothDivisorExceptionalSet P.radical s ⌊x ^ (3 * ↑P.total.natDegree ^ 2 * ε)⌋₊.toPNat' (x ^ (3 * ↑P.total.natDegree * ε / 2)) a b

theorem NairTenenbaum.PolynomialSystem.integerSum_le_four_contributions {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) {ε x w₀ : ℝ} (hε : 0 ≤ ε) (hx : 1 ≤ x) (hw₀ : 1 ≤ w₀) (a b : ℤ) : have N := ⌊x ^ (3 * ↑P.total.natDegree ^ 2 * ε)⌋₊.toPNat'; P.integerSum F a b ≤ P.smallRoughContribution F N a b (x ^ (↑P.total.natDegree * ε / 16)) + P.primePowerContribution F (x ^ (↑P.total.natDegree * ε / 2)) a b + P.smoothDivisorContribution F (Finset.Icc 0 ⌊w₀⌋₊) N (x ^ (3 * ↑P.total.natDegree * ε / 2)) a b + P.intermediatePrefixContribution F N (x ^ (3 * ↑P.total.natDegree ^ 2 * ε / 2)) w₀ x (↑P.total.natDegree * ε / 16) a b

The decomposition depends on the value scale, not on the position of the interval. The exceptional-set classes cover the second and third alternatives.