Harcos's irreducible sum equals the negative root power sum

The input character is the actual polynomial character. The Euler logarithmic identity is produced by finite factorization, not assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerCoefficient_zero {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) : harcosEulerCoefficient η 0 = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerLogCoefficient_eq_powerSum {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (α β : ℂ) (hA : harcosEulerSeries η = (1 - PowerSeries.C α * PowerSeries.X) * (1 - PowerSeries.C β * PowerSeries.X)) (n : ℕ) (hn : n ≠ 0) : harcosEulerLogCoefficient η n = -(α ^ n + β ^ n)

A quadratic factorization of the actual monic series determines all prime-power sums.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerSeries_character {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) : harcosEulerSeries ↑(harcosEtaHom a b) = harcosLSeries a b

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEuler_character_powerSum {p : ℕ} [Fact (Nat.Prime p)] (a : ZMod p) (b : ℤ) (ha : a ≠ 0) (hb : ↑b ≠ 0) (α β : ℂ) (hsum : α + β = -completeKloosterman p a b) (hprod : α * β = ↑p) (n : ℕ) (hn : n ≠ 0) : harcosEulerLogCoefficient (↑(harcosEtaHom a ↑b)) n = -(α ^ n + β ^ n)

The finite algebraic content of Harcos's equation (10), for the actual character.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEuler_character_reciprocalRoots {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (ha : a ≠ 0) (n : ℕ) (hn : n ≠ 0) : harcosEulerLogCoefficient (↑(harcosEtaHom a b)) n = -(harcosReciprocalRootPlus a b ^ n + harcosReciprocalRootMinus a b ^ n)

The actual irreducible coefficients for the explicitly constructed reciprocal roots.