Twin primes and Chowla's conjecture over function fields

TheoremSize of the quotient of \(F(T)\) by a nonzero polynomial#✓fully proved

Let \(F\) be a field and let \(f \in F[T]\) be a nonzero polynomial. Then the cardinality of the quotient ring \(F[T]/(f)\) is \(|F|^{\deg f}\), where cardinalities are natural numbers and an infinite set has cardinality \(0\).

theorem cardQuot_span_eq_pow_natDegree {f : F[X]} (hf : f ≠ 0) :
    (Ideal.span {f}).cardQuot = Nat.card F ^ f.natDegree
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over \(\mathbb{F}_q[T]\), Annals of Math. 196 (2) 2022, Equation (1.1).
Used by 2
Used byNorm of a nonzero polynomial · The norm on \(F(T)\)

DefinitionThe norm on \(F(T)\)#✓fully proved

Let \(F\) be a finite field. The ring norm on the polynomial ring \(F[T]\) sends \(f\) to the number of elements of the quotient ring \(F[T]/(f)\), written \(|f| = |F[T]/(f)|\); for \(f = 0\) the quotient is infinite and \(|0| = 0\). It is a ring norm: \(|f| = 0\) only for \(f = 0\), \(|-f| = |f|\), \(|f + g| \le |f| + |g|\) and \(|fg| \le |f|\,|g|\).

MathlibExt.NumberTheory.ChowlaAndTwinPrimeOverFqTWanted.ChowlaAndTwinPrimeOverFqT.ringNorm · 31 lines 
noncomputable def ringNorm : RingNorm (F[X]) where
  toFun f := (Ideal.span {f}).cardQuot
  map_zero' := by simp
  add_le' f g := by
    norm_cast
    by_cases hf : f = 0
    · simp [hf]
    by_cases hg : g = 0
    · simp [hg]
    by_cases hfg : f + g = 0
    · simp [hfg]
    grw [cardQuot_span_eq_pow_natDegree hf, cardQuot_span_eq_pow_natDegree hg,
      cardQuot_span_eq_pow_natDegree hfg, Polynomial.natDegree_add_le f g, max_def]
    · split_ifs
      · apply self_le_add_left
      · apply self_le_add_right
    · exact Nat.card_pos
  neg' := by simp
  mul_le' f g := by
    norm_cast
    by_cases hf : f = 0
    · simp [hf]
    by_cases hg : g = 0
    · simp [hg]
    have hfg : f * g ≠ 0 := mul_ne_zero hf hg
    rw [cardQuot_span_eq_pow_natDegree hf, cardQuot_span_eq_pow_natDegree hg,
      cardQuot_span_eq_pow_natDegree hfg, Polynomial.natDegree_mul hf hg, pow_add]
  eq_zero_of_map_eq_zero' f hf := by
    contrapose! hf
    rw [cardQuot_span_eq_pow_natDegree hf, Nat.cast_ne_zero]
    exact pow_ne_zero _ Nat.card_pos.ne'
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over \(\mathbb{F}_q[T]\), Annals of Math. 196 (2) 2022, Equation (1.1).
Uses 1 · Used by 5
Statement usesSize of the quotient of \(F(T)\) by a nonzero polynomial
Used byMonic polynomials of bounded norm · The norm of a polynomial is the size of its quotient ring · Norm of a nonzero polynomial · Singular series for twin primes in \(F(T)\) · Twin prime asymptotic over \(\mathbb{F}_q(T)\) for large \(q\)

TheoremThe norm of a polynomial is the size of its quotient ring#✓fully proved

Let \(F\) be a finite field and give \(F[T]\) its ring norm. For every \(f \in F[T]\), the norm \(|f|\) equals the number of elements of the quotient ring \(F[T]/(f)\), where an infinite quotient (the case \(f = 0\)) counts as \(0\).

theorem norm_eq_cardQuot (f : F[X]) : ‖f‖ = (Ideal.span {f}).cardQuot
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over \(\mathbb{F}_q[T]\), Annals of Math. 196 (2) 2022, Equation (1.1).
Uses 1 · Used by 1
Statement usesThe norm on \(F(T)\)
Used byNorm of a nonzero polynomial

TheoremNorm of a nonzero polynomial#✓fully proved

Let \(F\) be a finite field and give \(F[T]\) its ring norm. For every nonzero \(f \in F[T]\), the norm of \(f\) is \(|f| = |F|^{\deg f}\), where \(|F|\) is the number of elements of \(F\).

theorem norm_eq_pow_natDegree {f : F[X]} (hf : f ≠ 0) : ‖f‖ = Nat.card F ^ f.natDegree
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over \(\mathbb{F}_q[T]\), Annals of Math. 196 (2) 2022, Equation (1.1).
Uses 3
Statement usesThe norm on \(F(T)\)
Proof usesSize of the quotient of \(F(T)\) by a nonzero polynomial · The norm of a polynomial is the size of its quotient ring

DefinitionPrimes of \(F(T)\)#✓fully proved

Let \(F\) be a finite field. The primes of the polynomial ring \(F[T]\) are its monic irreducible polynomials.

def primes : Set F[X] :=
  {P : F[X] | P.Monic ∧ Irreducible P}
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over \(\mathbb{F}_q[T]\), Annals of Math. 196 (2) 2022, the sentence after Equation (1.4).
Used by 2
Used bySingular series for twin primes in \(F(T)\) · Twin prime asymptotic over \(\mathbb{F}_q(T)\) for large \(q\)

DefinitionIndicator of a statement#✓fully proved

For a proposition \(P\), the indicator \(\mathbf{1}_P\) is the real number \(1\) if \(P\) holds and \(0\) otherwise.

noncomputable def indicator (pred : Prop) : ℝ := if pred then 1 else 0
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over \(\mathbb{F}_q[T]\), Annals of Math. 196 (2) 2022, Equation (1.4).
Used by 1
Used bySingular series for twin primes in \(F(T)\)

DefinitionSingular series for twin primes in \(F(T)\)#✓fully proved

Let \(F\) be a finite field with \(q\) elements and let \(h \in F[T]\). The Hardy–Littlewood constant of the prime pair \(\{f, f + h\}\) is the infinite product over all primes \(P\) of \(F[T]\) (the monic irreducible polynomials)

\[\mathfrak{S}_q(h) = \prod_P \frac{1 - |P|^{-1} - |P|^{-1}\,\mathbf{1}_{P \nmid h}}{(1 - |P|^{-1})^2},\]

where \(|P|\) is the norm of \(P\) and \(\mathbf{1}_{P \nmid h}\) is \(1\) if \(P\) does not divide \(h\) and \(0\) otherwise.

The product is an unconditional infinite product of real numbers; when it does not converge its value is taken to be \(1\).

noncomputable def 𝔖_q (h : F[X]) : ℝ :=
  ∏' P : primes F, (1 - ‖P‖⁻¹ - ‖P‖⁻¹ * indicator (¬ (P : F[X]) ∣ h)) / (1 - ‖P‖⁻¹) ^ 2
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over \(\mathbb{F}_q[T]\), Annals of Math. 196 (2) 2022, Equation (1.4).
Uses 3 · Used by 1
Statement usesIndicator of a statement · Primes of \(F(T)\) · The norm on \(F(T)\)
Used byTwin prime asymptotic over \(\mathbb{F}_q(T)\) for large \(q\)

TheoremTwin prime asymptotic over \(\mathbb{F}_q(T)\) for large \(q\)#●ready to prove

Let \(p\) be an odd prime and let \(q\) be a power of \(p\) with \(q > 685090\,p^2\); write \(\mathbb{F}_q\) for the finite field with \(q\) elements. Then there is a real number \(\varepsilon > 0\) such that for every nonzero \(h \in \mathbb{F}_q[T]\), as \(X \to \infty\) through the powers of \(q\),

\[\#\{f \in \mathbb{F}_q[T] : |f| = X,\ f \text{ and } f + h \text{ are prime}\} = \frac{\mathfrak{S}_q(h)\, X}{(\log_q X)^2} + O\bigl(X^{1 - \varepsilon}\bigr),\]

where \(|f| = |\mathbb{F}_q[T]/(f)|\) is the norm of \(f\), the primes of \(\mathbb{F}_q[T]\) are its monic irreducible polynomials, \(\mathfrak{S}_q(h)\) is the singular series for twin primes, and the implied constant may depend on \(h\) (but \(\varepsilon\) does not).

public theorem_wanted theorem_1_1 (hp : Odd p) (hq : q > 685090 * p ^ 2) :
    ∃ ε > (0 : ℝ), -- there exists a power saving such that ...
      ∀ h ≠ 0, (fun X : powers q ↦ Set.ncard {f | ‖f‖ = X ∧ f ∈ primes 𝔽_q ∧ f + h ∈ primes 𝔽_q} -
        𝔖_q h * X / (Real.logb q X) ^ 2) =O[Filter.atTop] (fun X : powers q ↦ (X : ℝ) ^ (1 - ε))
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over 𝔽_q[T], Annals of Math, 196 (2) 2022. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_chowla_and_twin_prime_over_fq_t of the lean-eval benchmark.
Uses 3
Statement usesPrimes of \(F(T)\) · The norm on \(F(T)\) · Singular series for twin primes in \(F(T)\)

DefinitionMonic polynomials of bounded norm#✓fully proved

Let \(F\) be a finite field and let \(X\) be a real number. This is the set of monic polynomials \(f \in F[T]\) whose norm \(|f| = |F[T]/(f)|\), the number of elements of the quotient ring \(F[T]/(f)\), satisfies \(|f| \le X\).

def monicBounded (X : ℝ) : Set (F[X]) :=
  {f : F[X] | f.Monic ∧ ‖f‖ ≤ X}
Uses 1 · Used by 1
Statement usesThe norm on \(F(T)\)
Used byChowla's conjecture over \(\mathbb{F}_q(T)\) for large \(q\)

TheoremChowla's conjecture over \(\mathbb{F}_q(T)\) for large \(q\)#●ready to prove

Let \(p\) be an odd prime, let \(k \ge 1\) be a natural number, and let \(q\) be a power of \(p\) with \(q > p^2 k^2 e^2\), where \(e\) is Euler's number; write \(\mathbb{F}_q\) for the finite field with \(q\) elements. Let \(h_1, \dots, h_k \in \mathbb{F}_q[T]\) be distinct polynomials. Then, as the real number \(X\) tends to \(\infty\),

\[\sum_{f \text{ monic},\ |f| \le X} \mu(f + h_1)\,\mu(f + h_2) \cdots \mu(f + h_k) = o(X),\]

where the sum runs over the monic \(f \in \mathbb{F}_q[T]\) of norm \(|f| = |\mathbb{F}_q[T]/(f)|\) at most \(X\), and \(\mu\) is the Möbius function of \(\mathbb{F}_q[T]\): \(\mu(g) = (-1)^r\) if \(g\) is squarefree with \(r\) irreducible factors, and \(\mu(g) = 0\) otherwise.

public theorem_wanted theorem_1_3 (hp : Odd p) (k : ℕ) (hk : k ≥ 1) (hq : q > p ^ 2 * k ^ 2 * e ^ 2)
    (h : Fin k → 𝔽_q[X]) (h_distinct : Function.Injective h) :
    (fun X : ℝ ↦ ∑' f : monicBounded 𝔽_q X, ∏ i, moebius (f + h i)) =o[Filter.atTop] id
Sources
  • W. Sawin and M. Shusterman, On the Chowla and twin primes conjectures over 𝔽_q[T], Annals of Math, 196 (2) 2022. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_chowla_and_twin_prime_over_fq_t of the lean-eval benchmark.
Uses 1
Statement usesMonic polynomials of bounded norm
8 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.