English
Let s be a subset of natural numbers and suppose the divisibility-closed condition holds: whenever m | n and n ∈ s, then m ∈ s. Then for Additive-Group-valued functions f, g on N, the relation ∑_{i|n} f(i) = g(n) for all n in s is equivalent to the Möbius inversion formula ∑_{x∈n.divisorsAntidiagonal} μ(x.fst) • g(x.snd) = f(n) for all n in s.
Русский
Пусть s ⊆ N и если m делит n и n∈s, то m∈s. Тогда для значимых в ADD-Group функций f,g: сумма по делителям ∑_{i|n} f(i) = g(n) для всех n∈s эквивалентна формуле Моебиуса ∑_{(d,e): de=n} μ(d)·g(e) = f(n) для всех n∈s.
LaTeX
$$$\forall f,g : \mathbb{N} \to R\, (s:Set\mathbb{N})\ (hs : ∀ m n, m \mid n → n ∈ s → m ∈ s) : (\forall n>0, n\in s → (\sum_{i\in n.divisors} f(i)) = g(n)) \\iff \\ (\forall n>0, n\in s → \sum_{x\in n.divisorsAntidiagonal} μ(x.fst) \cdot g(x.snd) = f(n)).$$
Lean4
/-- Möbius inversion for functions to an `AddCommGroup`, where the equalities only hold on a
well-behaved set. -/
theorem sum_eq_iff_sum_smul_moebius_eq_on [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, μ x.fst • g x.snd) = f n :=
by
constructor
· intro h
let G := fun (n : ℕ) => (∑ i ∈ n.divisors, f i)
intro n hn hnP
suffices ∑ d ∈ n.divisors, μ (n / d) • G d = f n
by
rw [Nat.sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
intro d hd
rw [← h d (Nat.pos_of_mem_divisors hd) <| hs d n (Nat.dvd_of_mem_divisors hd) hnP]
rw [← Nat.sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)]
apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn
intro _ _; rfl
· intro h
let F := fun (n : ℕ) => ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd
intro n hn hnP
suffices ∑ d ∈ n.divisors, F d = g n by
rw [← this, sum_congr rfl]
intro d hd
rw [← h d (Nat.pos_of_mem_divisors hd) <| hs d n (Nat.dvd_of_mem_divisors hd) hnP]
apply sum_eq_iff_sum_smul_moebius_eq.mpr _ n hn
intro _ _; rfl
