Ideal norm counts as a multiplicative arithmetic function with positive mean

noncomputable def NairTenenbaum.idealNormArithmetic (K : Type u_1) [Field K] [NumberField K] : ArithmeticFunction ℝ

Zero at zero, since arithmetic functions encode only positive integers.

Equations

• NairTenenbaum.idealNormArithmetic K = { toFun := fun (n : ℕ) => if n = 0 then 0 else ↑(NairTenenbaum.idealNormCount K n), map_zero' := ⋯ }

theorem NairTenenbaum.idealNormArithmetic_apply_pos (K : Type u_1) [Field K] [NumberField K] {n : ℕ} (hn : 0 < n) : (idealNormArithmetic K) n = ↑(idealNormCount K n)

theorem NairTenenbaum.idealNormArithmetic_isMultiplicative (K : Type u_1) [Field K] [NumberField K] : (idealNormArithmetic K).IsMultiplicative

theorem NairTenenbaum.idealNormArithmetic_mean (K : Type u_1) [Field K] [NumberField K] : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, (idealNormArithmetic K) k) / ↑n) Filter.atTop (nhds (NumberField.dedekindZeta_residue K))

theorem NairTenenbaum.idealNormArithmetic_convolution_mean (K : Type u_1) [Field K] [NumberField K] {g : ArithmeticFunction ℝ} (hg : Summable fun (d : ℕ) => |g d| / ↑d) : Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory (⇑(g * idealNormArithmetic K)) x / x) Filter.atTop (nhds (NumberField.dedekindZeta_residue K * ∑' (d : ℕ), g d / ↑d))