The finite Euler index for comparison with minimal-polynomial orbits

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

Monic irreducibles with nonzero constant coefficient and degree dividing n.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerNonzeroPrimes p n = {k ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerPrimes p n | k.coeff 0 ≠ 0 ∧ k.natDegree ∣ n}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_harcosEulerNonzeroPrimes {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (hn : n ≠ 0) (k : Polynomial (ZMod p)) : k ∈ harcosEulerNonzeroPrimes p n ↔ k.Monic ∧ Irreducible k ∧ k.coeff 0 ≠ 0 ∧ k.natDegree ∣ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerLogCoefficient_eq_flat {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (n : ℕ) (hn : n ≠ 0) : harcosEulerLogCoefficient η n = ∑ k ∈ harcosEulerPrimes p n with k.natDegree ∣ n, ↑k.natDegree * η k ^ (n / k.natDegree)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEuler_character_eq_nonzeroPrime_sum {p : ℕ} [Fact (Nat.Prime p)] (a b : ZMod p) (n : ℕ) (hn : n ≠ 0) : harcosEulerLogCoefficient (↑(harcosEtaHom a b)) n = ∑ k ∈ harcosEulerNonzeroPrimes p n, ↑k.natDegree * harcosEta a b k ^ (n / k.natDegree)

The exact flat, nonzero-root index used by the finite-field orbit sum.