Actual coefficient sums for Harcos's L-polynomial

The monic polynomials are parametrized by all their lower coefficients, not by an assumed list of L-function coefficients. Source: Harcos, §3, Theorem 5, pages/harcos-lpolynomial-06.png.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (v : Fin n → ZMod p) : Polynomial (ZMod p)

A monic polynomial with the given vector of lower coefficients.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic n v = Polynomial.X ^ n + (Polynomial.ofFn n) v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic_monic {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (v : Fin n → ZMod p) : (harcosMonic n v).Monic

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic_natDegree {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (v : Fin n → ZMod p) : (harcosMonic n v).natDegree = n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic_coeff_lt {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (v : Fin n → ZMod p) (i : ℕ) (hi : i < n) : (harcosMonic n v).coeff i = v ⟨i, hi⟩

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic_unique {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (f : Polynomial (ZMod p)) (hm : f.Monic) (hd : f.natDegree = n) : ∃! v : Fin n → ZMod p, harcosMonic n v = f

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic_injective {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : Function.Injective (harcosMonic n)

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

Exactly the finite set of monic polynomials of degree n.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonicPolynomials p n = Finset.image (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic n) Finset.univ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_harcosMonicPolynomials {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (f : Polynomial (ZMod p)) : f ∈ harcosMonicPolynomials p n ↔ f.Monic ∧ f.natDegree = n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonicPolynomials_card {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : (harcosMonicPolynomials p n).card = p ^ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic_zero {p : ℕ} [Fact (Nat.Prime p)] (v : Fin 0 → ZMod p) : harcosMonic 0 v = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic_one {p : ℕ} [Fact (Nat.Prime p)] (v : Fin 1 → ZMod p) : harcosMonic 1 v = Polynomial.X + Polynomial.C (v 0)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (n : ℕ) : ℂ

The genuine finite monic-degree coefficient sum of the polynomial character.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b n = ∑ v : Fin n → ZMod p, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta a b (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonic n v)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_eq_sum_monic {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (n : ℕ) : harcosCoefficient a b n = ∑ f ∈ harcosMonicPolynomials p n, harcosEta a b f

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_eq_sum_monicDegreeEq {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (n : ℕ) [Fintype (Polynomial.MonicDegreeEq (ZMod p) n)] : harcosCoefficient a b n = ∑ f : Polynomial.MonicDegreeEq (ZMod p) n, harcosEta a b ↑f

Interface to finite-UFD sums indexed by Mathlib's degree-exact monic subtype.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_norm_le {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (n : ℕ) : ‖harcosCoefficient a b n‖ ≤ ↑p ^ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_zero {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosCoefficient a b 0 = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_one {p : ℕ} [Fact (Nat.Prime p)] (a : ZMod p) (b : ℤ) : harcosCoefficient a (↑b) 1 = completeKloosterman p a b

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta_monic_coefficients {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (n : ℕ) (hn : 2 ≤ n) (v : Fin n → ZMod p) : harcosEta a b (harcosMonic n v) = if v ⟨0, ⋯⟩ = 0 then 0 else ZMod.stdAddChar (-a * v ⟨n - 1, ⋯⟩ - b * (v ⟨1, ⋯⟩ / v ⟨0, ⋯⟩))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_ge_three {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) (n : ℕ) (hn : 3 ≤ n) : harcosCoefficient a b n = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_two_sum {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosCoefficient a b 2 = ∑ c : ZMod p, if c = 0 then 0 else ∑ t : ZMod p, ZMod.stdAddChar ((-a - b / c) * t)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_two {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) : harcosCoefficient a b 2 = ↑p

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLSeries {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : PowerSeries ℂ

The formal generating series, before any coefficient evaluation.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLSeries a b = PowerSeries.mk (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLPolynomial {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : Polynomial ℂ

The polynomial assembled from the actual degree-zero, one, and two sums.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLPolynomial a b = ∑ n ∈ Finset.range 3, (Polynomial.monomial n) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLPolynomial_coeff {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) (n : ℕ) : (harcosLPolynomial a b).coeff n = harcosCoefficient a b n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLPolynomial_eq {p : ℕ} [Fact (Nat.Prime p)] (a : ZMod p) (b : ℤ) (ha : a ≠ 0) (hb : ↑b ≠ 0) : harcosLPolynomial a ↑b = 1 + Polynomial.C (completeKloosterman p a b) * Polynomial.X + Polynomial.C ↑p * Polynomial.X ^ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLSeries_eq_polynomial {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) : harcosLSeries a b = ↑(harcosLPolynomial a b)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient_one_residue {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosCoefficient a b 1 = completeKloosterman p a ↑b.val

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLPolynomial_eq_coefficients {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosLPolynomial a b = 1 + Polynomial.C (harcosCoefficient a b 1) * Polynomial.X + Polynomial.C (harcosCoefficient a b 2) * Polynomial.X ^ 2

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRootPlus {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : ℂ

The first reciprocal root, constructed from the actual coefficient sums.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRootPlus a b = (-MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b 1 + (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b 1 ^ 2 - 4 * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b 2).sqrt) / 2

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRootMinus {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : ℂ

The second reciprocal root; the two choices may coincide.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRootMinus a b = (-MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b 1 - (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b 1 ^ 2 - 4 * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCoefficient a b 2).sqrt) / 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRoots_add {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosReciprocalRootPlus a b + harcosReciprocalRootMinus a b = -harcosCoefficient a b 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRoots_mul {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosReciprocalRootPlus a b * harcosReciprocalRootMinus a b = harcosCoefficient a b 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLPolynomial_factorization {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosLPolynomial a b = (1 - Polynomial.C (harcosReciprocalRootPlus a b) * Polynomial.X) * (1 - Polynomial.C (harcosReciprocalRootMinus a b) * Polynomial.X)

Factorization of the polynomial obtained from the monic-degree sums.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLSeries_factorization {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) : harcosLSeries a b = (1 - PowerSeries.C (harcosReciprocalRootPlus a b) * PowerSeries.X) * (1 - PowerSeries.C (harcosReciprocalRootMinus a b) * PowerSeries.X)

The root factorization is an identity of the actual coefficient generating series.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRoots_add_kloosterman {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosReciprocalRootPlus a b + harcosReciprocalRootMinus a b = -completeKloosterman p a ↑b.val

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRoots_mul_prime {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) : harcosReciprocalRootPlus a b * harcosReciprocalRootMinus a b = ↑p

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosReciprocalRoots_ne_zero {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) : harcosReciprocalRootPlus a b ≠ 0 ∧ harcosReciprocalRootMinus a b ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosLPolynomial_roots {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) : (harcosLPolynomial a b).IsRoot (harcosReciprocalRootPlus a b)⁻¹ ∧ (harcosLPolynomial a b).IsRoot (harcosReciprocalRootMinus a b)⁻¹

The inverses are actual complex zeros of the coefficient-generated polynomial.