Finite Euler coefficient identities for actual monic polynomials

This is the algebraic, coefficientwise version of the Euler-product argument in Harcos, §3, Lemma 7 and Theorem 6 (pages/harcos-lpolynomial-05.png–07.png). The multiplicities below are those of the actual polynomial factorization.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerCoefficient {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (n : ℕ) : ℂ

The coefficient obtained by summing a multiplicative weight over actual monics.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerCoefficient η n = ∑ f ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonicPolynomials p n, η f

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerMarked {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (k : Polynomial (ZMod p)) (n : ℕ) : ℂ

A coefficient with one marked occurrence of an irreducible factor.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerMarked η k n = ∑ f ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonicPolynomials p n, ↑(Multiset.count k (UniqueFactorizationMonoid.normalizedFactors f)) * η f

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerPrimes (p n : ℕ) [Fact (Nat.Prime p)] : Finset (Polynomial (ZMod p))

Every monic irreducible of degree at most the cutoff, with no duplicates.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerPrimes p n = (Finset.range (n + 1)).biUnion fun (d : ℕ) => Finset.filter Irreducible (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonicPolynomials p d)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_harcosEulerPrimes {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (k : Polynomial (ZMod p)) : k ∈ harcosEulerPrimes p n ↔ k.Monic ∧ Irreducible k ∧ k.natDegree ≤ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerMarked_eq_zero {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (k : Polynomial (ZMod p)) (n : ℕ) (hn : n < k.natDegree) : harcosEulerMarked η k n = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerMarked_add_degree {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (k : Polynomial (ZMod p)) (hk : k.Monic) (hi : Irreducible k) (n : ℕ) : harcosEulerMarked η k (k.natDegree + n) = η k * (harcosEulerCoefficient η n + harcosEulerMarked η k n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEuler_degree_marked {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (n : ℕ) : ↑n * harcosEulerCoefficient η n = ∑ k ∈ harcosEulerPrimes p n, ↑k.natDegree * harcosEulerMarked η k n