English
Möbius inversion for additive targets: for any AddCommGroup R, and functions f,g : ℕ → R, the two equivalent Möbius inversion statements hold.
Русский
Инверсия Мёбиуса для функций в аддитивной группе: эквивалентны две формулировки обращения Мёбиуса.
LaTeX
$$Sum equations equivalence via Möbius inversion$$
Lean4
/-- Möbius inversion for functions to an `AddCommGroup`. -/
theorem sum_eq_iff_sum_smul_moebius_eq [AddCommGroup R] {f g : ℕ → R} :
(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd = f n :=
by
let f' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else f x, if_pos rfl⟩
let g' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else g x, if_pos rfl⟩
trans (ζ : ArithmeticFunction ℤ) • f' = g'
· rw [ArithmeticFunction.ext_iff]
apply forall_congr'
intro n
cases n with
| zero => simp
| succ n =>
rw [coe_zeta_smul_apply]
simp only [forall_prop_of_true, succ_pos']
simp only [f', g', coe_mk, succ_ne_zero, ite_false]
rw [sum_congr rfl fun x hx => ?_]
rw [if_neg (Nat.pos_of_mem_divisors hx).ne']
trans μ • g' = f'
· constructor <;> intro h
· rw [← h, ← mul_smul, moebius_mul_coe_zeta, one_smul]
· rw [← h, ← mul_smul, coe_zeta_mul_moebius, one_smul]
· rw [ArithmeticFunction.ext_iff]
apply forall_congr'
intro n
cases n with
| zero => simp
| succ n =>
simp only [forall_prop_of_true, succ_pos', smul_apply, f', g', coe_mk, succ_ne_zero, ite_false]
rw [sum_congr rfl fun x hx => ?_]
simp [if_neg (Nat.pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)).ne']
