Bateman-Horn Conjecture

Reference: Wikipedia

noncomputable def BatemanHornConjecture.OmegaP (polys : Finset (Polynomial ℤ)) (p : ℕ) : ℕ

OmegaP S p counts the number of residue classes mod p where at least one polynomial in S vanishes.

Equations

• BatemanHornConjecture.OmegaP polys p = {n : ZMod p | ∃ f ∈ polys, Polynomial.eval n (Polynomial.map (Int.castRingHom (ZMod p)) f) = 0}.ncard

def BatemanHornConjecture.DegreesProduct (polys : Finset (Polynomial ℤ)) : ℕ

The product of degrees of polynomials in a finite set.

Equations

• BatemanHornConjecture.DegreesProduct polys = ∏ f ∈ polys, f.natDegree

noncomputable def BatemanHornConjecture.BatemanHornConstant (polys : Finset (Polynomial ℤ)) : ℝ

The Bateman-Horn constant of a set of polynomials S. This is defined as the infinite product over all primes: $$\frac{1}{D} \prod_p (1 - \frac{1}{p})^{-|S|} (1 - \frac{\omega_p(S)}{p})$$ where $D = \prod_{f \in S} \deg(f)$ is the product of degrees and $\omega_p(S)$ is the number of residue classes mod $p$ where at least one polynomial in $S$ vanishes.

Equations

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

noncomputable def BatemanHornConjecture.CountSimultaneousPrimes (polys : Finset (Polynomial ℤ)) (x : ℝ) : ℕ

CountSimultaneousPrimes S x counts the number of n ≤ x at which all polynomials in S attain a prime value.

Equations

• BatemanHornConjecture.CountSimultaneousPrimes polys x = (Finset.filter (fun (n : ℕ) => ∀ f ∈ polys, Nat.Prime (Polynomial.eval (↑n) f).natAbs) (Finset.range (⌊x⌋₊ + 1))).card

theorem BatemanHornConjecture.bateman_horn_conjecture (polys : Finset (Polynomial ℤ)) (h_nonempty : polys.Nonempty) (h_irreducible : ∀ f ∈ polys, BunyakovskyCondition f) (h_compat : SchinzelCondition polys) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑(CountSimultaneousPrimes polys x)) fun (x : ℝ) => BatemanHornConstant polys * x / Real.log x ^ polys.card

The Bateman-Horn Conjecture Given a finite collection of distinct irreducible polynomials non-constant $f_1, f_2, \dots, f_k \in \mathbb{Z}[x]$ with positive leading coefficients that satisfy the Schinzel condition, the number of positive integers n ≤ x for which all polynomials $f_i$ are simultaneously prime is asymptotic to: $$C(f_1, f_2, \dots, f_k) x / (log x)^k$$ where $C$ is the Bateman-Horn constant given by the convergent infinite product: $$C = \frac{1}{D}\prod_{p\in\mathbb{P}} (1 - 1/p)^(-k) · (1 - \omega_p/p)$$ Here $\omega_p/p$ is the number of residue classes modulo $p$ for which at least one polynomial vanishes.

The Schinzel condition ensures that for each prime $p$, there exists some integer $n$ such that $p$ does not divide the product $f_(n) f_2(n) \dotsb f_(n)$, which guarantees the infinite product converges to a positive value.