The coefficientwise Euler logarithmic derivative

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerGeometric (d : ℕ) (c : ℂ) : PowerSeries ℂ

The geometric formal series in c T^d; no convergence is involved.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerGeometric d c = PowerSeries.mk fun (n : ℕ) => if d ∣ n then c ^ (n / d) else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerGeometric_step (d : ℕ) (hd : 0 < d) (c : ℂ) : harcosEulerGeometric d c = 1 + PowerSeries.C c * PowerSeries.X ^ d * harcosEulerGeometric d c

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerGeometric_mul (d : ℕ) (hd : 0 < d) (c : ℂ) : (1 - PowerSeries.C c * PowerSeries.X ^ d) * harcosEulerGeometric d c = 1

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

The formal series of the actual monic coefficient sums.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerSeries η = PowerSeries.mk (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerCoefficient η)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerMarked_series {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (k : Polynomial (ZMod p)) (hk : k.Monic) (hi : Irreducible k) : PowerSeries.mk (harcosEulerMarked η k) = (harcosEulerGeometric k.natDegree (η k) - 1) * harcosEulerSeries η

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

A finite logarithmic-derivative series, containing all irreducibles up to the cutoff.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerLog η N = ∑ k ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerPrimes p N, PowerSeries.C ↑k.natDegree * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerGeometric k.natDegree (η k) - 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerLog_mul_coeff {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (N n : ℕ) (hn : n ≤ N) : (PowerSeries.coeff n) (harcosEulerLog η N * harcosEulerSeries η) = ↑n * harcosEulerCoefficient η n

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

The actual irreducible divisor sum appearing in Harcos's equation (10).

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerLogCoefficient η n = ∑ d ∈ n.divisors, ↑d * ∑ k ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMonicPolynomials p d with Irreducible k, η k ^ (n / d)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEulerLog_coeff {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (N n : ℕ) (hn : n ≤ N) : (PowerSeries.coeff n) (harcosEulerLog η N) = harcosEulerLogCoefficient η n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEuler_recurrence {p : ℕ} [Fact (Nat.Prime p)] (η : Polynomial (ZMod p) →* ℂ) (n : ℕ) : ↑n * harcosEulerCoefficient η n = ∑ j ∈ Finset.range (n + 1), harcosEulerLogCoefficient η j * harcosEulerCoefficient η (n - j)

The finite Euler logarithmic recurrence, proved from polynomial UFD factorization.