English
Let s be a subset of natural numbers, and hs a divisibility-closure property. Then for AddCommGroup-valued f,g, the identity ∑_{i|n} f(i) = g(n) for all n in s is equivalent to ∑_{x∈n.divisorsAntidiagonal} μ(x.fst) • g(x.snd) = f(n) for all n in s.
Русский
Пусть s — подмножество натуральных чисел, и hs— свойство замкнутости по делимости. Тогда для функций f,g со значениями в добавочно-группе: ∑_{i|n} f(i) = g(n) при всех n∈s эквивалентно ∑_{x∈n.divisorsAntidiagonal} μ(x.fst) • g(x.snd) = 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) : (∀ n ∈ s, (\sum_{i|n} f(i)) = g(n)) \\iff \\ (∀ n ∈ s, (\sum_{x∈ n.divisorsAntidiagonal} μ(x.fst) \cdot g(x.snd)) = f(n)).$$
Lean4
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) (hs₀ : 0 ∉ s) :
(∀ n ∈ s, (∑ i ∈ n.divisors, f i) = g n) ↔ ∀ n ∈ s, (∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd) = f n :=
by
have : ∀ P : ℕ → Prop, ((∀ n ∈ s, P n) ↔ (∀ n > 0, n ∈ s → P n)) := fun P ↦
by
refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
contrapose! hs₀
simpa [nonpos_iff_eq_zero.mp hs₀] using hn
simpa only [this] using sum_eq_iff_sum_smul_moebius_eq_on s hs
