The proved estimates for original polynomial families

The factorization data are constructed from the no-fixed-prime hypothesis. The user of these statements supplies only the original integer polynomials. All analytic constants precede both the polynomials and their factorization.

noncomputable def NairTenenbaum.familyBadDiscriminant {k : ℕ} (Q : Fin k → Polynomial ℤ) (hQ : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : ℕ

The restricted discriminant of a selected irreducible factorization.

Equations

• NairTenenbaum.familyBadDiscriminant Q hQ = (NairTenenbaum.familySystem Q hQ).snd.badDiscriminant

noncomputable def NairTenenbaum.familyMainTerm {k : ℕ} (Q : Fin k → Polynomial ℤ) (hQ : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) (F : ArithmeticMap k) (x y : ℝ) : ℝ

The original weight main term, with the factorization constructed.

Equations

• NairTenenbaum.familyMainTerm Q hQ F x y = NairTenenbaum.mainTerm (NairTenenbaum.familySystem Q hQ).snd F x y

noncomputable def NairTenenbaum.familyProgressionMainTerm {k : ℕ} (Q : Fin k → Polynomial ℤ) (hQ : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) (F : ArithmeticMap k) (q : ℕ) (x y : ℝ) : ℝ

The progression main term, with the factorization constructed.

Equations

• NairTenenbaum.familyProgressionMainTerm Q hQ F q x y = NairTenenbaum.progressionMainTerm (NairTenenbaum.familySystem Q hQ).snd F q x y

theorem NairTenenbaum.theoremOne_for_families {g : ℕ} (hg : 0 < g) {A B ε δ : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hδ : 0 < δ) (hδ₁ : δ ≤ 1) : ∃ (c₀ : ℝ), 0 < c₀ ∧ ∃ (C : ℕ → ℝ), (∀ (D : ℕ), 0 < C D) ∧ ∀ (k : ℕ) (Q : Fin k → Polynomial ℤ) (hQ : NoFixedPrimeDivisor (∏ j : Fin k, Q j)), (∏ j : Fin k, Q j).natDegree = g → ∀ (F : ArithmeticMap k), Admissible A B (ε * δ / 3) F → ∀ (x y : ℝ), c₀ * ↑(polynomialHeight (∏ j : Fin k, Q j)) ^ δ < x → x ^ (4 * ↑g ^ 2 * ε) ≤ y → y ≤ x → shortSum Q F x y ≤ C (familyBadDiscriminant Q hQ) * familyMainTerm Q hQ F x y

Theorem 1 for the original integer polynomials, without an additional factorization-data hypothesis. The endpoint range in ε is slightly stronger than the paper's strict inequality.

theorem NairTenenbaum.corollaryOne_for_families {g : ℕ} (hg : 0 < g) {A B ε δ : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hδ : 0 < δ) (hδ₁ : δ ≤ 1 / 2) : ∃ (c₁ : ℝ), 0 < c₁ ∧ ∀ (β : ℝ), 0 < β → β < 1 → ∃ (C : ℕ → ℝ), (∀ (D : ℕ), 0 < C D) ∧ ∀ (k : ℕ) (Q : Fin k → Polynomial ℤ) (hQ : NoFixedPrimeDivisor (∏ j : Fin k, Q j)), (∏ j : Fin k, Q j).natDegree = g → ∀ (F : ArithmeticMap k), Admissible A B (ε * β * δ / 6) F → ∀ (q a : ℕ), 0 < q → q.Coprime (Polynomial.eval (↑a) (∏ j : Fin k, Q j)).natAbs → ∀ (x y : ℝ), c₁ * ↑(polynomialHeight (∏ j : Fin k, Q j)) ^ (2 * δ) < x → x ^ (4 * ↑g ^ 2 * ε) ≤ y → y ≤ x → ↑q ≤ y ^ (1 - β) → progressionSum Q F q a x y ≤ C (familyBadDiscriminant Q hQ) * familyProgressionMainTerm Q hQ F q x y

Corollary 1 for original polynomial families. The threshold is chosen before β, and no factorization data need be supplied. The range δ≤1/2 contains the paper's range δ≤1/(2g).

theorem NairTenenbaum.corollaryThree_for_families {k g : ℕ} (hk : 0 < k) (hg : 0 < g) {A B ε δ : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hsmall : ε < 1 / (8 * ↑g ^ 2)) (hδ : 0 < δ) (hδ₁ : δ ≤ 1) : ∃ (c₀ : ℝ), 0 < c₀ ∧ ∃ (C : ℕ → ℝ), (∀ (D : ℕ), 0 < C D) ∧ ∀ (Q : Fin k → Polynomial ℤ) (hQ : NoFixedPrimeDivisor (∏ j : Fin k, Q j)), (∏ j : Fin k, Q j).natDegree = g → (∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (Q i)) (Polynomial.map (Int.castRingHom ℚ) (Q j))) → ∀ (F : Fin k → ArithmeticMap 1), (∀ (j : Fin k), Admissible A B (ε * δ / 3) (F j)) → ∀ (x y : ℝ), c₀ * ↑(polynomialHeight (∏ j : Fin k, Q j)) ^ δ < x → x ^ (4 * ↑g ^ 2 * ε) ≤ y → y ≤ x → productShortSum Q F x y ≤ C (familyBadDiscriminant Q hQ) * (y * sieveProduct (∏ j : Fin k, Q j) x * ∏ j : Fin k, rootWeightedSum (Q j) (F j) x)

Corollary 3 for original pairwise coprime integer polynomials. Both the factorization and the reduction to the factored root sums are proved.