Multiplicative completion and Dirichlet inverses

Values on prime powers determine a multiplicative arithmetic function. Applying this construction to a Dirichlet inverse proves that inversion preserves multiplicativity, without a recurrence over coprime pairs.

noncomputable def NairTenenbaum.multiplicativeCompletion {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) : ArithmeticFunction R

The multiplicative arithmetic function determined by the specified prime-power values.

Equations

• NairTenenbaum.multiplicativeCompletion f = { toFun := fun (n : ℕ) => if n = 0 then 0 else n.factorization.prod fun (p k : ℕ) => f (p ^ k), map_zero' := ⋯ }

theorem NairTenenbaum.multiplicativeCompletion_isMultiplicative {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) : (multiplicativeCompletion f).IsMultiplicative

theorem NairTenenbaum.multiplicativeCompletion_prime_pow {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) (hf : f 1 = 1) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : (multiplicativeCompletion f) (p ^ k) = f (p ^ k)

theorem NairTenenbaum.convolution_prime_pow_congr {R : Type u_1} [CommRing R] {f g g' : ArithmeticFunction R} {p k : ℕ} (hp : Nat.Prime p) (hg : ∀ j ≤ k, g (p ^ j) = g' (p ^ j)) : (f * g) (p ^ k) = (f * g') (p ^ k)

theorem NairTenenbaum.isMultiplicative_of_mul_eq_one {R : Type u_1} [CommRing R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hfg : f * g = 1) : g.IsMultiplicative

theorem NairTenenbaum.dirichletInverse_isMultiplicative {R : Type u_1} [CommRing R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hu : Invertible (f 1)) : (ArithmeticFunction.dirichletInverse (⇑f) hu).IsMultiplicative