Dirichlet inverses

Stream: Is there code for X?

[Niels Voss]

Has there been any work done on Dirichlet inverses? I know that number_theory.arithmetic_function contains Dirichlet convolutions, but I don't think it contains Dirichlet inverses. I'm currently trying to prove that all arithmetic functions f whose codomain is a field and f 1 ≠ 0 have a Dirichlet inverse.

[Alex J. Best]

Quite a while ago me and @Yaël Dillies wrote some stuff about incidence algebras #11656. We never quite wrote the inversion for arbitrary functions but it should be quite similar to the construction of mu there (its one of the TODOs). We should definitely finish and update this branch, and connect it to the arithmetic functions stuff before mathlib 4 imo!

[Yaël Dillies]

Fully agreed, but currently no time :grinning_face_with_smiling_eyes:

[Niels Voss]

I finished proving that all arithmetic functions to a field where f 1 ≠ 0 have an inverse. The proof, and the rest of my work, is here. I'm fine if this work becomes obsolete once incidence algebras are finished, because it was good practice for me. Here are some of the definitions so far:

import number_theory.arithmetic_function
import tactic.field_simp
open_locale big_operators
namespace nat
namespace arithmetic_function

variables {R : Type*} {M : Type*} [has_zero R] [add_comm_monoid M] [has_smul R M] [has_one M]
variables (f : arithmetic_function R) (g : arithmetic_function M)

def is_dirichlet_inv : Prop := f • g = 1

variable [comm_ring R]

theorem dirichlet_inv_symm (h : is_dirichlet_inv f g) : g • f = 1
def dirichlet_inv_to_unit (h : is_dirichlet_inv f g) : (arithmetic_function R)ˣ
theorem dirichlet_inv_unique {g₁ : arithmetic_function R} {g₂ : arithmetic_function R}
  (h₁ : is_dirichlet_inv f g₁) (h₂ : is_dirichlet_inv f g₂) : g₁ = g₂

variable [field R]

def dirichlet_inv_fun (f : arithmetic_function R) : ℕ → R
| 0 := 0
| 1 := 1 / (f 1)
| n := -1 / (f 1) * ∑ x : (divisors_antidiagonal n).erase ⟨1, n⟩,
  ( have x.val.2 < n := some_proof,
    (f x.val.1) * (dirichlet_inv_fun x.val.2))
def dirichlet_inv (f : arithmetic_function R) : arithmetic_function R :=
{ to_fun := dirichlet_inv_fun f,
  map_zero' := by unfold dirichlet_inv_fun }
instance has_inv : has_inv (arithmetic_function R) := { inv := dirichlet_inv }
theorem dirichlet_inv_is_inv {f : arithmetic_function R} (h : f 1 ≠ 0) : is_dirichlet_inv f f⁻¹
@[simp] lemma dirichlet_inv_mul_cancel {f : arithmetic_function R} (h : f 1 ≠ 0) : f * f⁻¹ = 1