# Arithmetic Functions and Dirichlet Convolution #

This file defines arithmetic functions, which are functions from `ℕ` to a specified type that map 0 to 0. In the literature, they are often instead defined as functions from `ℕ+`. These arithmetic functions are endowed with a multiplication, given by Dirichlet convolution, and pointwise addition, to form the Dirichlet ring.

## Main Definitions #

- `ArithmeticFunction R` consists of functions `f : ℕ → R` such that `f 0 = 0`.
- An arithmetic function `f` `IsMultiplicative` when `x.Coprime y → f (x * y) = f x * f y`.
- The pointwise operations `pmul` and `ppow` differ from the multiplication and power instances on `ArithmeticFunction R`, which use Dirichlet multiplication.
- `ζ` is the arithmetic function such that `ζ x = 1` for `0 < x`.
- `σ k` is the arithmetic function such that `σ k x = ∑ y ∈ divisors x, y ^ k` for `0 < x`.
- `pow k` is the arithmetic function such that `pow k x = x ^ k` for `0 < x`.
- `id` is the identity arithmetic function on `ℕ`.
- `ω n` is the number of distinct prime factors of `n`.
- `Ω n` is the number of prime factors of `n` counted with multiplicity.
- `μ` is the Möbius function (spelled `moebius` in code).

## Main Results #

- Several forms of Möbius inversion:
- `sum_eq_iff_sum_mul_moebius_eq` for functions to a `CommRing`
- `sum_eq_iff_sum_smul_moebius_eq` for functions to an `AddCommGroup`
- `prod_eq_iff_prod_pow_moebius_eq` for functions to a `CommGroup`
- `prod_eq_iff_prod_pow_moebius_eq_of_nonzero` for functions to a `CommGroupWithZero`
- And variants that apply when the equalities only hold on a set `S : Set ℕ` such that `m ∣ n → n ∈ S → m ∈ S`:
- `sum_eq_iff_sum_mul_moebius_eq_on` for functions to a `CommRing`
- `sum_eq_iff_sum_smul_moebius_eq_on` for functions to an `AddCommGroup`
- `prod_eq_iff_prod_pow_moebius_eq_on` for functions to a `CommGroup`
- `prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero` for functions to a `CommGroupWithZero`

## Notation #

The arithmetic functions `ζ`, `σ`, `ω`, `Ω` and `μ` have Greek letter names. This notation is scpoed to the separate locales `ArithmeticFunction.zeta` for `ζ`, `ArithmeticFunction.sigma` for `σ`, `ArithmeticFunction.omega` for `ω`, `ArithmeticFunction.Omega` for `Ω`, and `ArithmeticFunction.Moebius` for `μ`, to allow for selective access.

The arithmetic function $$n \mapsto \prod_{p \mid n} f(p)$$ is given custom notation `∏ᵖ p ∣ n, f p` when applied to `n`.

## Tags #

arithmetic functions, dirichlet convolution, divisors

source
def ArithmeticFunction (R : Type u_1) [Zero R] :
Type u_1

An arithmetic function is a function from `ℕ` that maps 0 to 0. In the literature, they are often instead defined as functions from `ℕ+`. Multiplication on `ArithmeticFunctions` is by Dirichlet convolution.

Equations

- ArithmeticFunction R = ZeroHom ℕ R

Instances For

source
instance ArithmeticFunction.zero (R : Type u_1) [Zero R] :
Zero (ArithmeticFunction R)
Equations

- ArithmeticFunction.zero R = inferInstanceAs (Zero (ZeroHom ℕ R))

source
instance instInhabitedArithmeticFunction (R : Type u_1) [Zero R] :
Inhabited (ArithmeticFunction R)
Equations

- instInhabitedArithmeticFunction R = inferInstanceAs (Inhabited (ZeroHom ℕ R))

source
instance ArithmeticFunction.instFunLikeNat {R : Type u_1} [Zero R] :
FunLike (ArithmeticFunction R) ℕ R
Equations

- ArithmeticFunction.instFunLikeNat = inferInstanceAs (FunLike (ZeroHom ℕ R) ℕ R)

source
@[simp]
theorem ArithmeticFunction.toFun_eq {R : Type u_1} [Zero R] (f : ArithmeticFunction R) :
f.toFun = ⇑f
source
@[simp]
theorem ArithmeticFunction.coe_mk {R : Type u_1} [Zero R] (f : ℕ → R) (hf : f 0 = 0) :
⇑{ toFun := f, map_zero' := hf } = f
source
@[simp]
theorem ArithmeticFunction.map_zero {R : Type u_1} [Zero R] {f : ArithmeticFunction R} :
f 0 = 0
source
theorem ArithmeticFunction.coe_inj {R : Type u_1} [Zero R] {f g : ArithmeticFunction R} :
⇑f = ⇑g ↔ f = g
source
@[simp]
theorem ArithmeticFunction.zero_apply {R : Type u_1} [Zero R] {x : ℕ} :
0 x = 0
source
theorem ArithmeticFunction.ext {R : Type u_1} [Zero R] ⦃f g : ArithmeticFunction R⦄ (h : ∀ (x : ℕ), f x = g x) :
f = g
source
theorem ArithmeticFunction.ext_iff {R : Type u_1} [Zero R] {f g : ArithmeticFunction R} :
f = g ↔ ∀ (x : ℕ), f x = g x
source
instance ArithmeticFunction.one {R : Type u_1} [Zero R] [One R] :
One (ArithmeticFunction R)
Equations

- ArithmeticFunction.one = { one := { toFun := fun (x : ℕ) => if x = 1 then 1 else 0, map_zero' := ⋯ } }

source
theorem ArithmeticFunction.one_apply {R : Type u_1} [Zero R] [One R] {x : ℕ} :
1 x = if x = 1 then 1 else 0
source
@[simp]
theorem ArithmeticFunction.one_one {R : Type u_1} [Zero R] [One R] :
1 1 = 1
source
@[simp]
theorem ArithmeticFunction.one_apply_ne {R : Type u_1} [Zero R] [One R] {x : ℕ} (h : x ≠ 1) :
1 x = 0
source
def ArithmeticFunction.natToArithmeticFunction {R : Type u_1} [AddMonoidWithOne R] :
ArithmeticFunction ℕ → ArithmeticFunction R

Coerce an arithmetic function with values in `ℕ` to one with values in `R`. We cannot inline this in `natCoe` because it gets unfolded too much.

Equations

- ↑f = { toFun := fun (n : ℕ) => ↑(f n), map_zero' := ⋯ }

Instances For

source
instance ArithmeticFunction.natCoe {R : Type u_1} [AddMonoidWithOne R] :
Coe (ArithmeticFunction ℕ) (ArithmeticFunction R)
Equations

- ArithmeticFunction.natCoe = { coe := ArithmeticFunction.natToArithmeticFunction }

source
@[simp]
theorem ArithmeticFunction.natCoe_nat (f : ArithmeticFunction ℕ) :
↑f = f
source
@[simp]
theorem ArithmeticFunction.natCoe_apply {R : Type u_1} [AddMonoidWithOne R] {f : ArithmeticFunction ℕ} {x : ℕ} :
↑f x = ↑(f x)
source
def ArithmeticFunction.ofInt {R : Type u_1} [AddGroupWithOne R] :
ArithmeticFunction ℤ → ArithmeticFunction R

Coerce an arithmetic function with values in `ℤ` to one with values in `R`. We cannot inline this in `intCoe` because it gets unfolded too much.

Equations

- ↑f = { toFun := fun (n : ℕ) => ↑(f n), map_zero' := ⋯ }

Instances For

source
instance ArithmeticFunction.intCoe {R : Type u_1} [AddGroupWithOne R] :
Coe (ArithmeticFunction ℤ) (ArithmeticFunction R)
Equations

- ArithmeticFunction.intCoe = { coe := ArithmeticFunction.ofInt }

source
@[simp]
theorem ArithmeticFunction.intCoe_int (f : ArithmeticFunction ℤ) :
↑f = f
source
@[simp]
theorem ArithmeticFunction.intCoe_apply {R : Type u_1} [AddGroupWithOne R] {f : ArithmeticFunction ℤ} {x : ℕ} :
↑f x = ↑(f x)
source
@[simp]
theorem ArithmeticFunction.coe_coe {R : Type u_1} [AddGroupWithOne R] {f : ArithmeticFunction ℕ} :
↑↑f = ↑f
source
@[simp]
theorem ArithmeticFunction.natCoe_one {R : Type u_1} [AddMonoidWithOne R] :
↑1 = 1
source
@[simp]
theorem ArithmeticFunction.intCoe_one {R : Type u_1} [AddGroupWithOne R] :
↑1 = 1
source
instance ArithmeticFunction.add {R : Type u_1} [AddMonoid R] :
Add (ArithmeticFunction R)
Equations

- ArithmeticFunction.add = { add := fun (f g : ArithmeticFunction R) => { toFun := fun (n : ℕ) => f n + g n, map_zero' := ⋯ } }

source
@[simp]
theorem ArithmeticFunction.add_apply {R : Type u_1} [AddMonoid R] {f g : ArithmeticFunction R} {n : ℕ} :
(f + g) n = f n + g n
source
instance ArithmeticFunction.instAddMonoid {R : Type u_1} [AddMonoid R] :
AddMonoid (ArithmeticFunction R)
Equations

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

source
instance ArithmeticFunction.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] :
AddMonoidWithOne (ArithmeticFunction R)
Equations

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

source
instance ArithmeticFunction.instAddCommMonoid {R : Type u_1} [AddCommMonoid R] :
AddCommMonoid (ArithmeticFunction R)
Equations

- ArithmeticFunction.instAddCommMonoid = { toAddMonoid := ArithmeticFunction.instAddMonoid, add_comm := ⋯ }

source
instance ArithmeticFunction.instNeg {R : Type u_1} [NegZeroClass R] :
Neg (ArithmeticFunction R)
Equations

- ArithmeticFunction.instNeg = { neg := fun (f : ArithmeticFunction R) => { toFun := fun (n : ℕ) => -f n, map_zero' := ⋯ } }

source
instance ArithmeticFunction.instAddGroup {R : Type u_1} [AddGroup R] :
AddGroup (ArithmeticFunction R)
Equations

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

source
instance ArithmeticFunction.instAddCommGroup {R : Type u_1} [AddCommGroup R] :
AddCommGroup (ArithmeticFunction R)
Equations

- ArithmeticFunction.instAddCommGroup = { toAddGroup := have this := inferInstance; this, add_comm := ⋯ }

source
instance ArithmeticFunction.instSMul {R : Type u_1} {M : Type u_2} [Zero R] [AddCommMonoid M] [SMul R M] :
SMul (ArithmeticFunction R) (ArithmeticFunction M)

The Dirichlet convolution of two arithmetic functions `f` and `g` is another arithmetic function such that `(f * g) n` is the sum of `f x * g y` over all `(x,y)` such that `x * y = n`.

Equations

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

source
@[simp]
theorem ArithmeticFunction.smul_apply {R : Type u_1} {M : Type u_2} [Zero R] [AddCommMonoid M] [SMul R M] {f : ArithmeticFunction R} {g : ArithmeticFunction M} {n : ℕ} :
(f • g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 • g x.2
source
instance ArithmeticFunction.instMul {R : Type u_1} [Semiring R] :
Mul (ArithmeticFunction R)

The Dirichlet convolution of two arithmetic functions `f` and `g` is another arithmetic function such that `(f * g) n` is the sum of `f x * g y` over all `(x,y)` such that `x * y = n`.

Equations

- ArithmeticFunction.instMul = { mul := fun (x1 x2 : ArithmeticFunction R) => x1 • x2 }

source
@[simp]
theorem ArithmeticFunction.mul_apply {R : Type u_1} [Semiring R] {f g : ArithmeticFunction R} {n : ℕ} :
(f * g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2
source
theorem ArithmeticFunction.mul_apply_one {R : Type u_1} [Semiring R] {f g : ArithmeticFunction R} :
(f * g) 1 = f 1 * g 1
source
@[simp]
theorem ArithmeticFunction.natCoe_mul {R : Type u_1} [Semiring R] {f g : ArithmeticFunction ℕ} :
↑(f * g) = ↑f * ↑g
source
@[simp]
theorem ArithmeticFunction.intCoe_mul {R : Type u_1} [Ring R] {f g : ArithmeticFunction ℤ} :
↑(f * g) = ↑f * ↑g
source
theorem ArithmeticFunction.mul_smul' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f g : ArithmeticFunction R) (h : ArithmeticFunction M) :
(f * g) • h = f • g • h
source
theorem ArithmeticFunction.one_smul' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (b : ArithmeticFunction M) :
1 • b = b
source
instance ArithmeticFunction.instMonoid {R : Type u_1} [Semiring R] :
Monoid (ArithmeticFunction R)
Equations

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

source
instance ArithmeticFunction.instSemiring {R : Type u_1} [Semiring R] :
Semiring (ArithmeticFunction R)
Equations

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

source
instance ArithmeticFunction.instCommSemiring {R : Type u_1} [CommSemiring R] :
CommSemiring (ArithmeticFunction R)
Equations

- ArithmeticFunction.instCommSemiring = { toSemiring := ArithmeticFunction.instSemiring, mul_comm := ⋯ }

source
instance ArithmeticFunction.instCommRing {R : Type u_1} [CommRing R] :
CommRing (ArithmeticFunction R)
Equations

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

source
instance ArithmeticFunction.instModule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
Module (ArithmeticFunction R) (ArithmeticFunction M)
Equations

- ArithmeticFunction.instModule = { toSMul := ArithmeticFunction.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
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 }

Instances For

source
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 "ζ")

Instances For

source
@[simp]
theorem ArithmeticFunction.zeta_apply {x : ℕ} :
zeta x = if x = 0 then 0 else 1
source
theorem ArithmeticFunction.zeta_apply_ne {x : ℕ} (h : x ≠ 0) :
zeta x = 1
source
theorem ArithmeticFunction.zeta_eq_zero {x : ℕ} :
zeta x = 0 ↔ x = 0
source
theorem ArithmeticFunction.zeta_pos {x : ℕ} :
0 < zeta x ↔ 0 < x
source
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
source
@[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`.

source
theorem ArithmeticFunction.coe_zeta_mul_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
(↑zeta * f) x = ∑ i ∈ x.divisors, f i
source
theorem ArithmeticFunction.coe_mul_zeta_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
(f * ↑zeta) x = ∑ i ∈ x.divisors, f i
source
theorem ArithmeticFunction.coe_zeta_mul_comm {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} :
↑zeta * f = f * ↑zeta
source
theorem ArithmeticFunction.zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} :
(zeta * f) x = ∑ i ∈ x.divisors, f i
source
theorem ArithmeticFunction.mul_zeta_apply {f : ArithmeticFunction ℕ} {x : ℕ} :
(f * zeta) x = ∑ i ∈ x.divisors, f i
source
theorem ArithmeticFunction.zeta_mul_comm {f : ArithmeticFunction ℕ} :
zeta * f = f * zeta
source
def ArithmeticFunction.pmul {R : Type u_1} [MulZeroClass R] (f g : ArithmeticFunction R) :
ArithmeticFunction R

This is the pointwise product of `ArithmeticFunction`s.

Equations

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

Instances For

source
@[simp]
theorem ArithmeticFunction.pmul_apply {R : Type u_1} [MulZeroClass R] {f g : ArithmeticFunction R} {x : ℕ} :
(f.pmul g) x = f x * g x
source
theorem ArithmeticFunction.pmul_comm {R : Type u_1} [CommMonoidWithZero R] (f g : ArithmeticFunction R) :
f.pmul g = g.pmul f
source
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₃)
source
@[simp]
theorem ArithmeticFunction.pmul_zeta {R : Type u_1} [NonAssocSemiring R] (f : ArithmeticFunction R) :
f.pmul ↑zeta = f
source
@[simp]
theorem ArithmeticFunction.zeta_pmul {R : Type u_1} [NonAssocSemiring R] (f : ArithmeticFunction R) :
(↑zeta).pmul f = f
source
def ArithmeticFunction.ppow {R : Type u_1} [Semiring R] (f : ArithmeticFunction R) (k : ℕ) :
ArithmeticFunction R

This is the pointwise power of `ArithmeticFunction`s.

Equations

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

Instances For

source
@[simp]
theorem ArithmeticFunction.ppow_zero {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} :
f.ppow 0 = ↑zeta
source
@[simp]
theorem ArithmeticFunction.ppow_one {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} :
f.ppow 1 = f
source
@[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
source
theorem ArithmeticFunction.ppow_succ' {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {k : ℕ} :
f.ppow (k + 1) = f.pmul (f.ppow k)
source
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
source
def ArithmeticFunction.pdiv {R : Type u_1} [GroupWithZero R] (f g : ArithmeticFunction R) :
ArithmeticFunction R

This is the pointwise division of `ArithmeticFunction`s.

Equations

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

Instances For

source
@[simp]
theorem ArithmeticFunction.pdiv_apply {R : Type u_1} [GroupWithZero R] (f g : ArithmeticFunction R) (n : ℕ) :
(f.pdiv g) n = f n / g n
source
@[simp]
theorem ArithmeticFunction.pdiv_zeta {R : Type u_1} [DivisionSemiring R] (f : ArithmeticFunction R) :
f.pdiv ↑zeta = f

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

source
def ArithmeticFunction.prodPrimeFactors {R : Type u_1} [CommMonoidWithZero R] (f : ℕ → R) :
ArithmeticFunction R

The map $n \mapsto \prod_{p \mid n} f(p)$ as an arithmetic function

Equations

- ArithmeticFunction.prodPrimeFactors f = { toFun := fun (d : ℕ) => if d = 0 then 0 else ∏ p ∈ d.primeFactors, f p, map_zero' := ⋯ }

Instances For

source
def ArithmeticFunction.bigproddvd :
Lean.ParserDescr

`∏ᵖ p ∣ n, f p` is custom notation for `prodPrimeFactors f n`

Equations

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

Instances For

source
@[simp]
theorem ArithmeticFunction.prodPrimeFactors_apply {R : Type u_1} [CommMonoidWithZero R] {f : ℕ → R} {n : ℕ} (hn : n ≠ 0) :
(prodPrimeFactors fun (p : ℕ) => f p) n = ∏ p ∈ n.primeFactors, f p
source
def ArithmeticFunction.IsMultiplicative {R : Type u_1} [MonoidWithZero R] (f : ArithmeticFunction R) :
Prop

Multiplicative functions

Equations

- f.IsMultiplicative = (f 1 = 1 ∧ ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n)

Instances For

source
@[simp]
theorem ArithmeticFunction.IsMultiplicative.map_one {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (h : f.IsMultiplicative) :
f 1 = 1
source
@[simp]
theorem ArithmeticFunction.IsMultiplicative.map_mul_of_coprime {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ} (h : m.gcd n = 1) :
f (m * n) = f m * f n
source
theorem ArithmeticFunction.IsMultiplicative.map_prod {R : Type u_1} {ι : Type u_2} [CommMonoidWithZero R] (g : ι → ℕ) {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (s : Finset ι) (hs : (↑s).Pairwise (Function.onFun Nat.Coprime g)) :
f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)
source
theorem ArithmeticFunction.IsMultiplicative.map_prod_of_prime {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) (t : Finset ℕ) (ht : ∀ p ∈ t, Nat.Prime p) :
f (∏ a ∈ t, a) = ∏ a ∈ t, f a
source
theorem ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) (l : ℕ) (t : Finset ℕ) (ht : t ⊆ l.primeFactors) :
f (∏ a ∈ t, a) = ∏ a ∈ t, f a
source
theorem ArithmeticFunction.IsMultiplicative.prod_primeFactors {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {l : ℕ} (hl : Squarefree l) :
∏ a ∈ l.primeFactors, f a = f l
source
theorem ArithmeticFunction.IsMultiplicative.map_div_of_coprime {R : Type u_1} [GroupWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {l d : ℕ} (hdl : d ∣ l) (hl : (l / d).Coprime d) (hd : f d ≠ 0) :
f (l / d) = f l / f d
source
theorem ArithmeticFunction.IsMultiplicative.natCast {R : Type u_1} {f : ArithmeticFunction ℕ} [Semiring R] (h : f.IsMultiplicative) :
(↑f).IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.intCast {R : Type u_1} {f : ArithmeticFunction ℤ} [Ring R] (h : f.IsMultiplicative) :
(↑f).IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.mul {R : Type u_1} [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
(f * g).IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.pmul {R : Type u_1} [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
(f.pmul g).IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.pdiv {R : Type u_1} [CommGroupWithZero R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
(f.pdiv g).IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.multiplicative_factorization {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ} (hn : n ≠ 0) :
f n = n.factorization.prod fun (p k : ℕ) => f (p ^ k)

For any multiplicative function `f` and any `n > 0`, we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n`

source
theorem ArithmeticFunction.IsMultiplicative.iff_ne_zero {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} :
f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n

A recapitulation of the definition of multiplicative that is simpler for proofs

source
theorem ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) (g : ArithmeticFunction R) (hg : g.IsMultiplicative) :
f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)

Two multiplicative functions `f` and `g` are equal if and only if they agree on prime powers

source
theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors {R : Type u_1} [CommMonoidWithZero R] (f : ℕ → R) :
(ArithmeticFunction.prodPrimeFactors f).IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree {R : Type u_1} [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) {n : ℕ} (hn : Squarefree n) :
(ArithmeticFunction.prodPrimeFactors fun (p : ℕ) => (f + g) p) n = (f * g) n
source
theorem ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x y : ℕ} :
f (x.lcm y) * f (x.gcd y) = f x * f y
source
theorem ArithmeticFunction.IsMultiplicative.map_gcd {R : Type u_1} [CommGroupWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x y : ℕ} (hf_lcm : f (x.lcm y) ≠ 0) :
f (x.gcd y) = f x * f y / f (x.lcm y)
source
theorem ArithmeticFunction.IsMultiplicative.map_lcm {R : Type u_1} [CommGroupWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x y : ℕ} (hf_gcd : f (x.gcd y) ≠ 0) :
f (x.lcm y) = f x * f y / f (x.gcd y)
source
theorem ArithmeticFunction.IsMultiplicative.eq_zero_of_squarefree_of_dvd_eq_zero {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ} (hn : Squarefree n) (hmn : m ∣ n) (h_zero : f m = 0) :
f n = 0
source
def ArithmeticFunction.id :
ArithmeticFunction ℕ

The identity on `ℕ` as an `ArithmeticFunction`.

Equations

- ArithmeticFunction.id = { toFun := id, map_zero' := ArithmeticFunction.id._proof_1 }

Instances For

source
@[simp]
theorem ArithmeticFunction.id_apply {x : ℕ} :
id x = x
source
def ArithmeticFunction.pow (k : ℕ) :
ArithmeticFunction ℕ

`pow k n = n ^ k`, except `pow 0 0 = 0`.

Equations

- ArithmeticFunction.pow k = ArithmeticFunction.id.ppow k

Instances For

source
@[simp]
theorem ArithmeticFunction.pow_apply {k n : ℕ} :
(pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k
source
theorem ArithmeticFunction.pow_zero_eq_zeta :
pow 0 = zeta
source
theorem ArithmeticFunction.pow_one_eq_id :
pow 1 = id
source
def ArithmeticFunction.sigma (k : ℕ) :
ArithmeticFunction ℕ

`σ k n` is the sum of the `k`th powers of the divisors of `n`

Equations

- ArithmeticFunction.sigma k = { toFun := fun (n : ℕ) => ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ }

Instances For

source
def ArithmeticFunction.sigma.termσ :
Lean.ParserDescr

`σ k n` is the sum of the `k`th powers of the divisors of `n`

Equations

- ArithmeticFunction.sigma.termσ = Lean.ParserDescr.node `ArithmeticFunction.sigma.termσ 1024 (Lean.ParserDescr.symbol "σ")

Instances For

source
theorem ArithmeticFunction.sigma_apply {k n : ℕ} :
(sigma k) n = ∑ d ∈ n.divisors, d ^ k
source
@[simp]
theorem ArithmeticFunction.sigma_eq_zero {k n : ℕ} :
(sigma k) n = 0 ↔ n = 0
source
@[simp]
theorem ArithmeticFunction.sigma_pos_iff {k n : ℕ} :
0 < (sigma k) n ↔ 0 < n
source
theorem ArithmeticFunction.sigma_apply_prime_pow {k p i : ℕ} (hp : Nat.Prime p) :
(sigma k) (p ^ i) = ∑ j ∈ Finset.range (i + 1), p ^ (j * k)
source
theorem ArithmeticFunction.sigma_one_apply (n : ℕ) :
(sigma 1) n = ∑ d ∈ n.divisors, d
source
theorem ArithmeticFunction.sigma_one_apply_prime_pow {p i : ℕ} (hp : Nat.Prime p) :
(sigma 1) (p ^ i) = ∑ k ∈ Finset.range (i + 1), p ^ k
source
theorem ArithmeticFunction.sigma_eq_sum_div (k n : ℕ) :
(sigma k) n = ∑ d ∈ n.divisors, (n / d) ^ k
source
theorem ArithmeticFunction.sigma_zero_apply (n : ℕ) :
(sigma 0) n = n.divisors.card
source
theorem ArithmeticFunction.sigma_zero_apply_prime_pow {p i : ℕ} (hp : Nat.Prime p) :
(sigma 0) (p ^ i) = i + 1
source
@[simp]
theorem ArithmeticFunction.sigma_one (k : ℕ) :
(sigma k) 1 = 1
source
theorem ArithmeticFunction.sigma_pos (k n : ℕ) (hn0 : n ≠ 0) :
0 < (sigma k) n
source
theorem ArithmeticFunction.sigma_mono (k k' n : ℕ) (hk : k ≤ k') :
(sigma k) n ≤ (sigma k') n
source
theorem ArithmeticFunction.zeta_mul_pow_eq_sigma {k : ℕ} :
zeta * pow k = sigma k
source
theorem ArithmeticFunction.isMultiplicative_one {R : Type u_1} [MonoidWithZero R] :
IsMultiplicative 1
source
theorem ArithmeticFunction.isMultiplicative_zeta :
zeta.IsMultiplicative
source
theorem ArithmeticFunction.isMultiplicative_id :
id.IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.ppow {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {k : ℕ} :
(f.ppow k).IsMultiplicative
source
theorem ArithmeticFunction.isMultiplicative_pow {k : ℕ} :
(pow k).IsMultiplicative
source
theorem ArithmeticFunction.isMultiplicative_sigma {k : ℕ} :
(sigma k).IsMultiplicative
source
theorem Nat.card_divisors {n : ℕ} (hn : n ≠ 0) :
n.divisors.card = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
source
@[simp]
theorem Nat.divisors_card_eq_one_iff (n : ℕ) :
n.divisors.card = 1 ↔ n = 1
source
@[simp]
theorem ArithmeticFunction.sigma_eq_one_iff (k n : ℕ) :
(sigma k) n = 1 ↔ n = 1
source
theorem ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul {k n : ℕ} (hn : n ≠ 0) :
(sigma k) n = ∏ p ∈ n.primeFactors, ∑ i ∈ Finset.range (n.factorization p + 1), p ^ (i * k)
source
theorem Nat.sum_divisors {n : ℕ} (hn : n ≠ 0) :
∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ Finset.range (n.factorization p + 1), p ^ k
source
def ArithmeticFunction.cardFactors :
ArithmeticFunction ℕ

`Ω n` is the number of prime factors of `n`.

Equations

- ArithmeticFunction.cardFactors = { toFun := fun (n : ℕ) => n.primeFactorsList.length, map_zero' := ArithmeticFunction.cardFactors._proof_1 }

Instances For

source
def ArithmeticFunction.Omega.termΩ :
Lean.ParserDescr

`Ω n` is the number of prime factors of `n`.

Equations

- ArithmeticFunction.Omega.termΩ = Lean.ParserDescr.node `ArithmeticFunction.Omega.termΩ 1024 (Lean.ParserDescr.symbol "Ω")

Instances For

source
theorem ArithmeticFunction.cardFactors_apply {n : ℕ} :
cardFactors n = n.primeFactorsList.length
source
theorem ArithmeticFunction.cardFactors_zero :
cardFactors 0 = 0
source
@[simp]
theorem ArithmeticFunction.cardFactors_one :
cardFactors 1 = 0
source
@[simp]
theorem ArithmeticFunction.cardFactors_eq_zero_iff_eq_zero_or_one {n : ℕ} :
cardFactors n = 0 ↔ n = 0 ∨ n = 1
source
@[simp]
theorem ArithmeticFunction.cardFactors_pos_iff_one_lt {n : ℕ} :
0 < cardFactors n ↔ 1 < n
source
@[simp]
theorem ArithmeticFunction.cardFactors_eq_one_iff_prime {n : ℕ} :
cardFactors n = 1 ↔ Nat.Prime n
source
theorem ArithmeticFunction.cardFactors_mul {m n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) :
cardFactors (m * n) = cardFactors m + cardFactors n
source
theorem ArithmeticFunction.cardFactors_multiset_prod {s : Multiset ℕ} (h0 : s.prod ≠ 0) :
cardFactors s.prod = (Multiset.map (⇑cardFactors) s).sum
source
@[simp]
theorem ArithmeticFunction.cardFactors_apply_prime {p : ℕ} (hp : Nat.Prime p) :
cardFactors p = 1
source
theorem ArithmeticFunction.cardFactors_pow {m k : ℕ} :
cardFactors (m ^ k) = k * cardFactors m
source
@[simp]
theorem ArithmeticFunction.cardFactors_apply_prime_pow {p k : ℕ} (hp : Nat.Prime p) :
cardFactors (p ^ k) = k
source
theorem ArithmeticFunction.cardFactors_eq_sum_factorization {n : ℕ} :
cardFactors n = n.factorization.sum fun (x k : ℕ) => k
source
def ArithmeticFunction.cardDistinctFactors :
ArithmeticFunction ℕ

`ω n` is the number of distinct prime factors of `n`.

Equations

- ArithmeticFunction.cardDistinctFactors = { toFun := fun (n : ℕ) => n.primeFactorsList.dedup.length, map_zero' := ArithmeticFunction.cardDistinctFactors._proof_1 }

Instances For

source
def ArithmeticFunction.omega.termω :
Lean.ParserDescr

`ω n` is the number of distinct prime factors of `n`.

Equations

- ArithmeticFunction.omega.termω = Lean.ParserDescr.node `ArithmeticFunction.omega.termω 1024 (Lean.ParserDescr.symbol "ω")

Instances For

source
theorem ArithmeticFunction.cardDistinctFactors_zero :
cardDistinctFactors 0 = 0
source
@[simp]
theorem ArithmeticFunction.cardDistinctFactors_one :
cardDistinctFactors 1 = 0
source
theorem ArithmeticFunction.cardDistinctFactors_apply {n : ℕ} :
cardDistinctFactors n = n.primeFactorsList.dedup.length
source
@[simp]
theorem ArithmeticFunction.cardDistinctFactors_eq_zero {n : ℕ} :
cardDistinctFactors n = 0 ↔ n ≤ 1
source
@[simp]
theorem ArithmeticFunction.cardDistinctFactors_pos {n : ℕ} :
0 < cardDistinctFactors n ↔ 1 < n
source
theorem ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree {n : ℕ} (h0 : n ≠ 0) :
cardDistinctFactors n = cardFactors n ↔ Squarefree n
source
theorem ArithmeticFunction.cardDistinctFactors_eq_one_iff {n : ℕ} :
cardDistinctFactors n = 1 ↔ IsPrimePow n
source
@[simp]
theorem ArithmeticFunction.cardDistinctFactors_apply_prime_pow {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) :
cardDistinctFactors (p ^ k) = 1
source
@[simp]
theorem ArithmeticFunction.cardDistinctFactors_apply_prime {p : ℕ} (hp : Nat.Prime p) :
cardDistinctFactors p = 1
source
theorem ArithmeticFunction.cardDistinctFactors_mul {m n : ℕ} (h : m.Coprime n) :
cardDistinctFactors (m * n) = cardDistinctFactors m + cardDistinctFactors n
source
theorem ArithmeticFunction.cardDistinctFactors_prod {ι : Type u_2} {s : Finset ι} {f : ι → ℕ} (h : (↑s).Pairwise (Function.onFun Nat.Coprime f)) :
cardDistinctFactors (∏ i ∈ s, f i) = ∑ i ∈ s, cardDistinctFactors (f i)
source
def ArithmeticFunction.moebius :
ArithmeticFunction ℤ

`μ` is the Möbius function. If `n` is squarefree with an even number of distinct prime factors, `μ n = 1`. If `n` is squarefree with an odd number of distinct prime factors, `μ n = -1`. If `n` is not squarefree, `μ n = 0`.

Equations

- ArithmeticFunction.moebius = { toFun := fun (n : ℕ) => if Squarefree n then (-1) ^ ArithmeticFunction.cardFactors n else 0, map_zero' := ArithmeticFunction.moebius._proof_1 }

Instances For

source
def ArithmeticFunction.Moebius.termμ :
Lean.ParserDescr

`μ` is the Möbius function. If `n` is squarefree with an even number of distinct prime factors, `μ n = 1`. If `n` is squarefree with an odd number of distinct prime factors, `μ n = -1`. If `n` is not squarefree, `μ n = 0`.

Equations

- ArithmeticFunction.Moebius.termμ = Lean.ParserDescr.node `ArithmeticFunction.Moebius.termμ 1024 (Lean.ParserDescr.symbol "μ")

Instances For

source
@[simp]
theorem ArithmeticFunction.moebius_apply_of_squarefree {n : ℕ} (h : Squarefree n) :
moebius n = (-1) ^ cardFactors n
source
@[simp]
theorem ArithmeticFunction.moebius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬Squarefree n) :
moebius n = 0
source
theorem ArithmeticFunction.moebius_apply_one :
moebius 1 = 1
source
theorem ArithmeticFunction.moebius_ne_zero_iff_squarefree {n : ℕ} :
moebius n ≠ 0 ↔ Squarefree n
source
theorem ArithmeticFunction.moebius_eq_or (n : ℕ) :
moebius n = 0 ∨ moebius n = 1 ∨ moebius n = -1
source
theorem ArithmeticFunction.moebius_ne_zero_iff_eq_or {n : ℕ} :
moebius n ≠ 0 ↔ moebius n = 1 ∨ moebius n = -1
source
theorem ArithmeticFunction.moebius_sq_eq_one_of_squarefree {l : ℕ} (hl : Squarefree l) :
moebius l ^ 2 = 1
source
theorem ArithmeticFunction.abs_moebius_eq_one_of_squarefree {l : ℕ} (hl : Squarefree l) :
|moebius l| = 1
source
theorem ArithmeticFunction.moebius_sq {n : ℕ} :
moebius n ^ 2 = if Squarefree n then 1 else 0
source
theorem ArithmeticFunction.abs_moebius {n : ℕ} :
|moebius n| = if Squarefree n then 1 else 0
source
theorem ArithmeticFunction.abs_moebius_le_one {n : ℕ} :
|moebius n| ≤ 1
source
theorem ArithmeticFunction.moebius_apply_prime {p : ℕ} (hp : Nat.Prime p) :
moebius p = -1
source
theorem ArithmeticFunction.moebius_apply_prime_pow {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) :
moebius (p ^ k) = if k = 1 then -1 else 0
source
theorem ArithmeticFunction.moebius_apply_isPrimePow_not_prime {n : ℕ} (hn : IsPrimePow n) (hn' : ¬Nat.Prime n) :
moebius n = 0
source
theorem ArithmeticFunction.isMultiplicative_moebius :
moebius.IsMultiplicative
source
theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) :
∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d
source
theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) :
∏ p ∈ n.primeFactors, (1 - f p) = ∑ d ∈ n.divisors, ↑(moebius d) * f d
source
@[simp]
theorem ArithmeticFunction.moebius_mul_coe_zeta :
moebius * ↑zeta = 1
source
@[simp]
theorem ArithmeticFunction.coe_zeta_mul_moebius :
↑zeta * moebius = 1
source
@[simp]
theorem ArithmeticFunction.coe_moebius_mul_coe_zeta {R : Type u_1} [Ring R] :
↑moebius * ↑zeta = 1
source
@[simp]
theorem ArithmeticFunction.coe_zeta_mul_coe_moebius {R : Type u_1} [Ring R] :
↑zeta * ↑moebius = 1
source
instance ArithmeticFunction.instInvertibleNatToArithmeticFunctionZeta {R : Type u_1} [CommRing R] :
Invertible ↑zeta
Equations

- ArithmeticFunction.instInvertibleNatToArithmeticFunctionZeta = { invOf := ↑ArithmeticFunction.moebius, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

source
def ArithmeticFunction.zetaUnit {R : Type u_1} [CommRing R] :
(ArithmeticFunction R)ˣ

A unit in `ArithmeticFunction R` that evaluates to `ζ`, with inverse `μ`.

Equations

- ArithmeticFunction.zetaUnit = { val := ↑ArithmeticFunction.zeta, inv := ↑ArithmeticFunction.moebius, val_inv := ⋯, inv_val := ⋯ }

Instances For

source
@[simp]
theorem ArithmeticFunction.coe_zetaUnit {R : Type u_1} [CommRing R] :
↑zetaUnit = ↑zeta
source
@[simp]
theorem ArithmeticFunction.inv_zetaUnit {R : Type u_1} [CommRing R] :
↑zetaUnit⁻¹ = ↑moebius
source
theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq {R : Type u_1} [AddCommGroup R] {f g : ℕ → R} :
(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, moebius x.1 • g x.2 = f n

Möbius inversion for functions to an `AddCommGroup`.

source
theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq {R : Type u_1} [NonAssocRing R] {f g : ℕ → R} :
(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(moebius x.1) * g x.2 = f n

Möbius inversion for functions to a `Ring`.

source
theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq {R : Type u_1} [CommGroup R] {f g : ℕ → R} :
(∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ moebius x.1 = f n

Möbius inversion for functions to a `CommGroup`.

source
theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero {R : Type u_1} [CommGroupWithZero R] {f g : ℕ → R} (hf : ∀ (n : ℕ), 0 < n → f n ≠ 0) (hg : ∀ (n : ℕ), 0 < n → g n ≠ 0) :
(∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ moebius x.1 = f n

Möbius inversion for functions to a `CommGroupWithZero`.

source
theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on {R : Type u_1} [AddCommGroup R] {f g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) :
(∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, moebius x.1 • g x.2 = f n

Möbius inversion for functions to an `AddCommGroup`, where the equalities only hold on a well-behaved set.

source
theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on' {R : Type u_1} [AddCommGroup R] {f g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) (hs₀ : 0 ∉ s) :
(∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, moebius x.1 • g x.2 = f n
source
theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on {R : Type u_1} [NonAssocRing R] {f g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) :
(∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(moebius x.1) * g x.2 = f n

Möbius inversion for functions to a `Ring`, where the equalities only hold on a well-behaved set.

source
theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on {R : Type u_1} [CommGroup R] {f g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) :
(∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ moebius x.1 = f n

Möbius inversion for functions to a `CommGroup`, where the equalities only hold on a well-behaved set.

source
theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero {R : Type u_1} [CommGroupWithZero R] (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) {f g : ℕ → R} (hf : ∀ n > 0, f n ≠ 0) (hg : ∀ n > 0, g n ≠ 0) :
(∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ moebius x.1 = f n

Möbius inversion for functions to a `CommGroupWithZero`, where the equalities only hold on a well-behaved set.

source
theorem Nat.Coprime.card_divisors_mul {m n : ℕ} (hmn : m.Coprime n) :
(m * n).divisors.card = m.divisors.card * n.divisors.card
source
theorem Nat.Coprime.sum_divisors_mul {m n : ℕ} (hmn : m.Coprime n) :
∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d
source
def Mathlib.Meta.Positivity.evalArithmeticFunctionSigma :
PositivityExt

Extension for `ArithmeticFunction.sigma`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalArithmeticFunctionZeta :
PositivityExt

Extension for `ArithmeticFunction.zeta`.

Equations

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

Instances For