Theorems · Theorem · number theory

ArithmeticFunction.tendsTo_eulerProduct_ofPowerSeries

∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (q : ι → ℕ) [hq : Northcott q] (f : ι → PowerSeries R),
  (∀ (i : ι), PowerSeries.constantCoeff (f i) = 1) →
    ∀ (n : ℕ),
      ∀ᶠ (s : Finset ι) in Filter.atTop,
        (∏ i ∈ s, (ArithmeticFunction.ofPowerSeries (q i)) (f i)) n =
          (ArithmeticFunction.eulerProduct fun i => (ArithmeticFunction.ofPowerSeries (q i)) (f i)) n

Given arithmetic functions f(q⁻ˢ) with q → ∞, the partial products ∏ i ∈ s, f i converge to the Euler product pointwise.

Defined in

Mathlib.NumberTheory.ArithmeticFunction.LFunction

Cited by

0 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringNorthcott