FormalConjectures/Wikipedia/BatemanHornConjecture.lean

GitHub source file

5 declarations, 1 contain sorry, 0 declared as axioms

1. def BatemanHornConjecture.OmegaP OmegaP S p counts the number of residue classes mod p where at least one polynomial in S vanishes line 38 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Polynomial, Int, Nat

   Proof uses: Set.ncard, ZMod, Set.ofPred, Exists, And, Membership.mem, Eq, Polynomial.eval, Polynomial.map, Int.castRingHom, OfNat.ofNat

   12 instances, coercions and auxiliary constants left out.

   noncomputable def OmegaP (polys : Finset ℤ[X]) (p : ℕ) : ℕ :=
   …

2. def BatemanHornConjecture.DegreesProduct The product of degrees of polynomials in a finite set line 42 source

   Source documentation

   The product of degrees of polynomials in a finite set.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Polynomial, Int, Nat

   Proof uses: Finset.prod, Polynomial.natDegree

   3 instances, coercions and auxiliary constants left out.

   def DegreesProduct (polys : Finset ℤ[X]) : ℕ :=
   …

3. def BatemanHornConjecture.BatemanHornPartialProduct The partial Euler product of the Bateman-Horn constant of a set of polynomials S, taken over the primes line 53 source

   Source documentation

   The partial Euler product of the Bateman-Horn constant of a set of polynomials S, taken over the primes $p < N$: $$\prod_{p < N} (1 - \frac{1}{p})^{-|S|} (1 - \frac{\omega_p(S)}{p})$$ where $\omega_p(S)$ is the number of residue classes mod $p$ where at least one polynomial in $S$ vanishes. The Bateman-Horn constant is the limit of these partial products as $N \to \infty$; the product is only conditionally convergent, so the order of the factors matters.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Polynomial, Int, Nat, Real

   Proof uses: Finset.prod, Nat.primesBelow, HMul.hMul, HPow.hPow, HSub.hSub, OfNat.ofNat, HDiv.hDiv, Neg.neg, Finset.card, BatemanHornConjecture.OmegaP

   19 instances, coercions and auxiliary constants left out.

   noncomputable def BatemanHornPartialProduct (polys : Finset ℤ[X]) (N : ℕ) : ℝ :=
   …

4. def BatemanHornConjecture.CountSimultaneousPrimes CountSimultaneousPrimes S x counts the number of n ≤ x at which all polynomials in S attain a prime value line 58 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Polynomial, Int, Real, Nat

   Proof uses: Finset.card, Finset.filter, Membership.mem, Nat.Prime, Int.natAbs, Polynomial.eval, Finset.range, HAdd.hAdd, Nat.floor, OfNat.ofNat

   17 instances, coercions and auxiliary constants left out.

   noncomputable def CountSimultaneousPrimes (polys : Finset ℤ[X]) (x : ℝ) : ℕ :=
   …

5. theorem BatemanHornConjecture.bateman_horn_conjecture The Bateman-Horn Conjecture Given a finite collection of distinct irreducible polynomials non-constant sorry line 82 source

   Source documentation

   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 \leq x$ for which all polynomials $f_i$ are simultaneously prime is asymptotic to: $$\frac{C}{D} \frac{x}{(\log x)^k}$$ where $D = \prod_i \deg(f_i)$ and $C$ is the Bateman-Horn constant given by the convergent infinite product: $$C = \prod_{p\in\mathbb{P}} (1 - 1/p)^{-k} (1 - \omega_p/p)$$ Here $\omega_p$ is the number of residue classes modulo $p$ for which at least one polynomial vanishes. The product is only conditionally convergent: it is the limit as $N \to \infty$ of the partial products over the primes $p < N$.

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

   depends on sorry what this means

   Statement uses: Finset, Polynomial, Int, Finset.Nonempty, Membership.mem, BunyakovskyCondition, SchinzelCondition, Exists, Real, And, LT.lt, OfNat.ofNat, Filter.Tendsto, Nat, BatemanHornConjecture.BatemanHornPartialProduct, Filter.atTop, nhds, Asymptotics.IsEquivalent, BatemanHornConjecture.CountSimultaneousPrimes, HDiv.hDiv and 5 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   55 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem bateman_horn_conjecture
       (polys : Finset ℤ[X])
       (h_nonempty : polys.Nonempty)
       (h_irreducible : ∀ f ∈ polys, BunyakovskyCondition f)
       (h_compat : SchinzelCondition polys) :
       ∃ C : ℝ, 0 < C ∧ Tendsto (BatemanHornPartialProduct polys) atTop (𝓝 C) ∧
         (fun x : ℝ => (CountSimultaneousPrimes polys x : ℝ)) ~[atTop]
           (fun x : ℝ => C / DegreesProduct polys * x / (Real.log x) ^ polys.card) := by
   …

   Mentions: BunyakovskyCondition, SchinzelCondition, BatemanHornConjecture.BatemanHornPartialProduct, BatemanHornConjecture.CountSimultaneousPrimes, BatemanHornConjecture.DegreesProduct