The arithmetic function ζ

We define ζ to be the arithmetic function with ζ n = 1 for 0 < n (whose Dirichlet series is the Riemann zeta function).

Main Definitions

• ArithmeticFunction.zeta is the arithmetic function such that ζ x = 1 for 0 < x. The notation ζ for this function is available by opening ArithmeticFunction.zeta.
• ArithmeticFunction.pmul and ArithmeticFunction.pdiv are the pointwise multiplication and division on ArithmeticFunctions (for which ζ is the identity). These are not the same as the multiplication instance defined by Dirichlet convolution.

Tags

arithmetic functions, dirichlet convolution, divisors

def ArithmeticFunction.zeta : ArithmeticFunction ℕ

ζ 0 = 0, otherwise ζ x = 1. The Dirichlet Series is the Riemann ζ.

Equations

• ArithmeticFunction.zeta = { toFun := fun (x : ℕ) => if x = 0 then 0 else 1, map_zero' := ArithmeticFunction.zeta._proof_1 }

def ArithmeticFunction.zeta.termζ : Lean.ParserDescr

ζ 0 = 0, otherwise ζ x = 1. The Dirichlet Series is the Riemann ζ.

Equations

• ArithmeticFunction.zeta.termζ = Lean.ParserDescr.node `ArithmeticFunction.zeta.termζ 1024 (Lean.ParserDescr.symbol "ζ")

@[simp]

theorem ArithmeticFunction.zeta_apply {x : ℕ} : zeta x = if x = 0 then 0 else 1

theorem ArithmeticFunction.zeta_apply_ne {x : ℕ} (h : x ≠ 0) : zeta x = 1

theorem ArithmeticFunction.zeta_eq_zero {x : ℕ} : zeta x = 0 ↔ x = 0

theorem ArithmeticFunction.zeta_pos {x : ℕ} : 0 < zeta x ↔ 0 < x

theorem ArithmeticFunction.coe_zeta_smul_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [MulAction R M] {f : ArithmeticFunction M} {x : ℕ} : (↑zeta • f) x = ∑ i ∈ x.divisors, f i

@[simp]

theorem ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [MulAction R M] {f : ArithmeticFunction M} {x : ℕ} : (∑ x ∈ x.divisorsAntidiagonal, if x.1 = 0 then 0 • f x.2 else f x.2) = ∑ i ∈ x.divisors, f i

@[simp]-normal form of coe_zeta_smul_apply.

theorem ArithmeticFunction.coe_zeta_mul_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (↑zeta * f) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.coe_mul_zeta_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (f * ↑zeta) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.coe_zeta_mul_comm {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} : ↑zeta * f = f * ↑zeta

theorem ArithmeticFunction.zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (zeta * f) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.mul_zeta_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (f * zeta) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.zeta_mul_comm {f : ArithmeticFunction ℕ} : zeta * f = f * zeta

def ArithmeticFunction.pmul {R : Type u_1} [MulZeroClass R] (f g : ArithmeticFunction R) : ArithmeticFunction R

This is the pointwise product of ArithmeticFunctions.

Equations

• f.pmul g = { toFun := fun (x : ℕ) => f x * g x, map_zero' := ⋯ }

@[simp]

theorem ArithmeticFunction.pmul_apply {R : Type u_1} [MulZeroClass R] {f g : ArithmeticFunction R} {x : ℕ} : (f.pmul g) x = f x * g x

theorem ArithmeticFunction.pmul_comm {R : Type u_1} [CommMonoidWithZero R] (f g : ArithmeticFunction R) : f.pmul g = g.pmul f

theorem ArithmeticFunction.pmul_assoc {R : Type u_1} [SemigroupWithZero R] (f₁ f₂ f₃ : ArithmeticFunction R) : (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

@[simp]

theorem ArithmeticFunction.pmul_zeta {R : Type u_1} [NonAssocSemiring R] (f : ArithmeticFunction R) : f.pmul ↑zeta = f

@[simp]

theorem ArithmeticFunction.zeta_pmul {R : Type u_1} [NonAssocSemiring R] (f : ArithmeticFunction R) : (↑zeta).pmul f = f

def ArithmeticFunction.ppow {R : Type u_1} [Semiring R] (f : ArithmeticFunction R) (k : ℕ) : ArithmeticFunction R

This is the pointwise power of ArithmeticFunctions.

Equations

• f.ppow k = if h0 : k = 0 then ↑ArithmeticFunction.zeta else { toFun := fun (x : ℕ) => f x ^ k, map_zero' := ⋯ }

@[simp]

theorem ArithmeticFunction.ppow_zero {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} : f.ppow 0 = ↑zeta

@[simp]

theorem ArithmeticFunction.ppow_one {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} : f.ppow 1 = f

@[simp]

theorem ArithmeticFunction.ppow_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {k x : ℕ} (kpos : 0 < k) : (f.ppow k) x = f x ^ k

theorem ArithmeticFunction.ppow_succ' {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {k : ℕ} : f.ppow (k + 1) = f.pmul (f.ppow k)

theorem ArithmeticFunction.ppow_succ {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {k : ℕ} {kpos : 0 < k} : f.ppow (k + 1) = (f.ppow k).pmul f

def ArithmeticFunction.pdiv {R : Type u_1} [GroupWithZero R] (f g : ArithmeticFunction R) : ArithmeticFunction R

This is the pointwise division of ArithmeticFunctions.

Equations

• f.pdiv g = { toFun := fun (n : ℕ) => f n / g n, map_zero' := ⋯ }

@[simp]

theorem ArithmeticFunction.pdiv_apply {R : Type u_1} [GroupWithZero R] (f g : ArithmeticFunction R) (n : ℕ) : (f.pdiv g) n = f n / g n

@[simp]

theorem ArithmeticFunction.pdiv_zeta {R : Type u_1} [DivisionSemiring R] (f : ArithmeticFunction R) : f.pdiv ↑zeta = f

This result only holds for DivisionSemirings instead of GroupWithZeros because zeta takes values in ℕ, and hence the coercion requires an AddMonoidWithOne. TODO: Generalise zeta

theorem ArithmeticFunction.isMultiplicative_zeta : zeta.IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.pmul {R : Type u_1} [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) : (f.pmul g).IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.pdiv {R : Type u_1} [CommGroupWithZero R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) : (f.pdiv g).IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.ppow {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {k : ℕ} : (f.ppow k).IsMultiplicative

def Mathlib.Meta.Positivity.evalArithmeticFunctionZeta : PositivityExt

Extension for ArithmeticFunction.zeta.

Equations

• One or more equations did not get rendered due to their size.