Harcos's polynomial character

The coefficient formula in Harcos, §3, Definition 4 and Lemma 6 (pages/harcos-lpolynomial-05.png). nextCoeff is zero on constants; this includes the degree-zero endpoint in the multiplicativity statement.

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

The actual polynomial character, with zero at polynomials divisible by X.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta a b f = if f.coeff 0 = 0 then 0 else ZMod.stdAddChar (-a * (f.nextCoeff / f.leadingCoeff) - b * (f.coeff 1 / f.coeff 0))

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta_C {p : ℕ} [Fact (Nat.Prime p)] (a b c : ZMod p) : harcosEta a b (Polynomial.C c) = if c = 0 then 0 else 1

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta_norm_le_one {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (f : Polynomial (ZMod p)) : ‖harcosEta a b f‖ ≤ 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta_mul {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (f g : Polynomial (ZMod p)) : harcosEta a b (f * g) = harcosEta a b f * harcosEta a b g

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

The multiplicative source object for a later Euler-product construction.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEtaHom a b = { toFun := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta a b, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta_X_add_C {p : ℕ} [Fact (Nat.Prime p)] (a b c : ZMod p) : harcosEta a b (Polynomial.X + Polynomial.C c) = if c = 0 then 0 else ZMod.stdAddChar (-a * c - b * c⁻¹)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta_X_sub_C {p : ℕ} [Fact (Nat.Prime p)] (a b t : ZMod p) : harcosEta a b (Polynomial.X - Polynomial.C t) = if t = 0 then 0 else ZMod.stdAddChar (a * t + b * t⁻¹)