Theorem 3 for original integer polynomial families

The common irreducible factorization is constructed from the no-fixed-prime hypothesis. No additional factorization data need be supplied by the caller.

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

The prime-argument main term expressed for the original polynomial family.

Equations

• NairTenenbaum.familyPrimeMainTerm Q hQ F x y = NairTenenbaum.primeMainTerm (NairTenenbaum.familySystem Q hQ).snd F x y

theorem NairTenenbaum.theoremThree_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 → Polynomial.eval 0 (∏ j : Fin k, Q j) ≠ 0 → ∀ (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 → primeShortSum Q F x y ≤ C (familyBadDiscriminant Q hQ) * familyPrimeMainTerm Q hQ F x y

Theorem 3 with coefficient-independent constants chosen before the polynomial family. The endpoint range is slightly stronger than the paper's strict inequality in ε.