The four contribution classes restricted to prime arguments

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

Prime arguments above the analytic scale in an integer interval. Absolute values allow the decomposition to be stated independently of interval position.

Equations

• P.primeIntegerSum F x a b = ∑ t ∈ Finset.Ioc a b with Nat.Prime t.natAbs ∧ x < ↑t.natAbs, NairTenenbaum.extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs

theorem NairTenenbaum.PolynomialSystem.primeIntegerSum_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₀) (hcut : x ^ (↑P.total.natDegree * ε / 16) ≤ x) (a b : ℤ) : have N := ⌊x ^ (3 * ↑P.total.natDegree ^ 2 * ε)⌋₊.toPNat'; P.primeIntegerSum F x a b ≤ P.primeSmallRoughContribution 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.primeIntermediatePrefixContribution F N (x ^ (3 * ↑P.total.natDegree ^ 2 * ε / 2)) w₀ x (↑P.total.natDegree * ε / 16) a b