The sifted small-divisor sum bounded by the original main term

noncomputable def NairTenenbaum.primeMainTerm {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (x y : ℝ) : ℝ

The main term for prime arguments, including the logarithm and constant-term correction.

Equations

• NairTenenbaum.primeMainTerm P F x y = NairTenenbaum.mainTerm P F x y * NairTenenbaum.primeArgumentFactor P.total x

theorem NairTenenbaum.primeMainTerm_eq {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (x y : ℝ) : primeMainTerm P F x y = ↑(Polynomial.eval 0 P.total).natAbs / ↑(Polynomial.eval 0 P.total).natAbs.totient * (y / Real.log x) * sieveProduct P.total x * ∑ n ∈ positiveUpTo x, P.weight F n

The main expression in Theorem 3, with its constant-term correction and reciprocal logarithm displayed explicitly.

theorem NairTenenbaum.primeArgumentFactor_rpow (Q : Polynomial ℤ) {x : ℝ} (hx : 0 < x) (α : ℝ) : primeArgumentFactor Q (x ^ α) = primeArgumentFactor Q x / α

theorem NairTenenbaum.primeMainTerm_nonneg {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) {x y : ℝ} (hx : 1 ≤ x) (hy : 0 ≤ y) : 0 ≤ primeMainTerm P F x y

theorem NairTenenbaum.exists_powerSaving_le_primeMainTerm (g : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree ≤ g → Polynomial.eval 0 P.total ≠ 0 → ∀ (F : ArithmeticMap k), (∀ (n : Tuple k), 0 ≤ F n) → ∀ (x y : ℝ), 2 ≤ x → 0 ≤ y → y * x ^ (-δ) * F 1 ≤ C * primeMainTerm P F x y

The power-saving exceptional classes remain negligible after introducing the reciprocal logarithm. The constant is independent of Q(0).

theorem NairTenenbaum.primeArgumentSmallSieveCost_pos {B : ℝ} (hB : 0 < B) (σ : ℝ) {g D : ℕ} (hg : 0 < g) (hD : 0 < D) : 0 < primeArgumentSmallSieveCost B σ g D

theorem NairTenenbaum.exists_primeSmallDivisorSiftedSum_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) : ∃ (K : ℝ) (x₀ : ℝ), 0 < K ∧ 1 ≤ x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → Polynomial.eval 0 P.total ≠ 0 → ∀ (A B σ : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 0 ≤ A → 1 ≤ B → 0 < σ → ↑g ^ 2 * σ ≤ 1 / 8 → ∀ (x y : ℝ) (N : ℕ+) (a b : ℤ), x₀ ≤ x → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → P.primeSmallDivisorSiftedSum F g N a b (x ^ (↑g * ε / 16)) ≤ K * primeArgumentSmallSieveCost B σ g P.badDiscriminant * primeMainTerm P F x y

The sifted small-divisor sum is bounded by the paper's original main term. The constants precede the polynomial family and arithmetic function. The interval endpoint hypotheses allow the natural rounding of a real interval.