Prime arguments in the selected-prefix majorant

Primality supplies the extra sieve condition for X. The value decomposition and its growth bound continue to use the original polynomial system.

noncomputable def NairTenenbaum.PolynomialSystem.primeSmallDivisorSiftedSum {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (g : ℕ) (N : ℕ+) (a b : ℤ) (z : ℝ) : ℝ

The small-divisor sum sifted for the total polynomial times X.

Equations

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

theorem NairTenenbaum.PolynomialSystem.sum_selectedPrimeDivisors_le {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (g : ℕ) (N : ℕ+) (a b : ℤ) (z : ℝ) (T : Finset ℤ) (m : ℤ → Tuple r) (hT : T ⊆ Finset.Ioc a b) (hz : 0 ≤ z) (htPrime : ∀ t ∈ T, Nat.Prime t.natAbs) (htLarge : ∀ t ∈ T, z < ↑t.natAbs) (hm : ∀ t ∈ T, weightedMass P.exponent (m t) ≤ ↑N) (hdiv : ∀ t ∈ T, ∀ (i : Fin r), ↑↑(m t i) ∣ Polynomial.eval t (P.R i)) (hsift : ∀ t ∈ T, (sieveModulus P.total (mass (m t)) z).Coprime (Polynomial.eval t P.total).natAbs) : ∑ t ∈ T, pullback P.exponent F (m t) ≤ P.primeSmallDivisorSiftedSum F g N a b z

Grouping a selected divisor for each integer by its tuple gives the sifted small-divisor majorant. Distinct integers can have the same selected tuple.

theorem NairTenenbaum.PolynomialSystem.sum_primeRoughPrefix_le {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hA : 1 ≤ A) (hB : 0 ≤ B) (g : ℕ) (N : ℕ+) (a b : ℤ) (T : Finset ℤ) (n : ℤ → Tuple r) (q : ℤ → ℕ) (hT : T ⊆ Finset.Ioc a b) (hn : ∀ t ∈ T, ∀ (i : Fin r), ↑(n t i) = (Polynomial.eval t (P.R i)).natAbs) {x α c : ℝ} (hx : 1 < x) (hα : 0 < α) (htPrime : ∀ t ∈ T, Nat.Prime t.natAbs) (htLarge : ∀ t ∈ T, x ^ α < ↑t.natAbs) (hq : ∀ t ∈ T, x ^ α < ↑(q t)) (hsmall : ∀ t ∈ T, weightedMass P.exponent (primeSelect (n t) (Finset.range (q t))) ≤ ↑N) (hvalue : ∀ t ∈ T, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : (∑ t ∈ T, extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs) ≤ A ^ (c / α) * P.primeSmallDivisorSiftedSum F g N a b (x ^ α)

Equation (31), with explicit growth constant and a proven sieve condition. The finite set can be any part of the interval whose selected prefixes are small and whose next-prime cutoffs exceed x^α.