Bateman-Horn Conjecture

Reference: Wikipedia

def IsIrreducibleWithPosLeading (f : Polynomial ℤ) : Prop

Definition of irreducible polynomial with positive leading coefficient

Equations

• IsIrreducibleWithPosLeading f = (Irreducible f ∧ 0 < f.leadingCoeff)

def SatisfiesCompatibilityCondition (polys : Finset (Polynomial ℤ)) : Prop

The compatibility condition for a finite set S of polynomials in the Bateman-Horn conjecture. This states that for all primes p, there exists an n such that ∏ f ∈ S, f.eval n is non-zero modulo p.

Equations

• SatisfiesCompatibilityCondition polys = ∀ (p : ℕ), Nat.Prime p → ∃ (n : ℤ), ¬↑p ∣ Polynomial.eval n (polys.prod id)

noncomputable def 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

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

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

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

Equations

• BatemanHornConstant polys = ∏' (p : { p : ℕ // Nat.Prime p }), (1 - 1 / ↑↑p) ^ (-↑polys.card) * (1 - ↑(OmegaP polys ↑p) / ↑↑p)

noncomputable def 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

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

theorem bateman_horn_conjecture (polys : Finset (Polynomial ℤ)) (h_nonempty : polys.Nonempty) (h_irreducible : ∀ f ∈ polys, IsIrreducibleWithPosLeading f) (h_compat : SatisfiesCompatibilityCondition 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 f₁, f₂, ..., fₖ ∈ ℤ[X] with positive leading coefficients that satisfy the compatibility condition, the number of positive integers n ≤ x for which all polynomials f₁(n), f₂(n), ..., fₖ(n) are simultaneously prime is asymptotic to:

C(f₁, f₂, ..., fₖ) · x / (log x)^k

where C(f₁, f₂, ..., fₖ) is the Bateman-Horn constant given by the convergent infinite product:

C = ∏ₚ (1 - 1/p)^(-k) · (1 - ωₚ/p)

Here ωₚ is the number of residue classes modulo p for which at least one polynomial vanishes.

The compatibility condition ensures that for each prime p, there exists some integer n such that p does not divide the product f₁(n)·f₂(n)·...·fₖ(n), which guarantees the infinite product converges to a positive value.