feat(number_theory/arithmetic_function): moebius is the inverse of ze…

…ta (#5001)

Proves the most basic version of moebius inversion: that the moebius function is the inverse of the zeta function



Co-authored-by: jalex-stark <alexmaplegm@gmail.com>

src/algebra/squarefree.lean

@@ -5,6 +5,7 @@ Authors: Aaron Anderson
 -/
 import ring_theory.unique_factorization_domain
 import ring_theory.int.basic
+import number_theory.divisors
 
 /-!
 # Squarefree elements of monoids
@@ -144,4 +145,63 @@ instance : decidable_pred (squarefree : ℕ → Prop)
 | 0 := is_false not_squarefree_zero
 | (n + 1) := decidable_of_iff _ (squarefree_iff_nodup_factors (nat.succ_ne_zero n)).symm
 
+open unique_factorization_monoid
+
+lemma divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :
+  (n.divisors.filter squarefree).val =
+    (unique_factorization_monoid.factors n).to_finset.powerset.val.map (λ x, x.val.prod) :=
+begin
+  rw multiset.nodup_ext (finset.nodup _) (multiset.nodup_map_on _ (finset.nodup _)),
+  { intro a,
+    simp only [multiset.mem_filter, id.def, multiset.mem_map, finset.filter_val, ← finset.mem_def,
+      mem_divisors],
+    split,
+    { rintro ⟨⟨an, h0⟩, hsq⟩,
+      use (unique_factorization_monoid.factors a).to_finset,
+      simp only [id.def, finset.mem_powerset],
+      rcases an with ⟨b, rfl⟩,
+      rw mul_ne_zero_iff at h0,
+      rw unique_factorization_monoid.squarefree_iff_nodup_factors h0.1 at hsq,
+      rw [multiset.to_finset_subset, multiset.to_finset_val, multiset.erase_dup_eq_self.2 hsq,
+        ← associated_iff_eq, factors_mul h0.1 h0.2],
+      exact ⟨multiset.subset_of_le (multiset.le_add_right _ _), factors_prod h0.1⟩ },
+    { rintro ⟨s, hs, rfl⟩,
+      rw [finset.mem_powerset, ← finset.val_le_iff, multiset.to_finset_val] at hs,
+      have hs0 : s.val.prod ≠ 0,
+      { rw [ne.def, multiset.prod_eq_zero_iff],
+        simp only [exists_prop, id.def, exists_eq_right],
+        intro con,
+        apply not_irreducible_zero (irreducible_of_factor 0
+            (multiset.mem_erase_dup.1 (multiset.mem_of_le hs con))) },
+      rw [dvd_iff_dvd_of_rel_right (factors_prod h0).symm],
+      refine ⟨⟨multiset.prod_dvd_prod (le_trans hs (multiset.erase_dup_le _)), h0⟩, _⟩,
+      have h := unique_factorization_monoid.factors_unique irreducible_of_factor
+        (λ x hx, irreducible_of_factor x (multiset.mem_of_le
+          (le_trans hs (multiset.erase_dup_le _)) hx)) (factors_prod hs0),
+      rw [associated_eq_eq, multiset.rel_eq] at h,
+      rw [unique_factorization_monoid.squarefree_iff_nodup_factors hs0, h],
+      apply s.nodup } },
+  { intros x hx y hy h,
+    rw [← finset.val_inj, ← multiset.rel_eq, ← associated_eq_eq],
+    rw [← finset.mem_def, finset.mem_powerset] at hx hy,
+    apply unique_factorization_monoid.factors_unique _ _ (associated_iff_eq.2 h),
+    { intros z hz,
+      apply irreducible_of_factor z,
+      rw ← multiset.mem_to_finset,
+      apply hx hz },
+    { intros z hz,
+      apply irreducible_of_factor z,
+      rw ← multiset.mem_to_finset,
+      apply hy hz } }
+end
+
+open_locale big_operators
+
+lemma sum_divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0)
+  {α : Type*} [add_comm_monoid α] {f : ℕ → α} :
+  ∑ i in (n.divisors.filter squarefree), f i =
+    ∑ i in (unique_factorization_monoid.factors n).to_finset.powerset, f (i.val.prod) :=
+by rw [finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, multiset.map_map,
+    finset.sum_eq_multiset_sum]
+
 end nat

src/number_theory/arithmetic_function.lean

@@ -6,6 +6,7 @@ Authors: Aaron Anderson
 import algebra.big_operators.ring
 import number_theory.divisors
 import algebra.squarefree
+import algebra.invertible
 
 /-!
 # Arithmetic Functions and Dirichlet Convolution
@@ -543,6 +544,9 @@ localized "notation `Ω` := card_factors" in arithmetic_function
 lemma card_factors_apply {n : ℕ} :
   Ω n = n.factors.length := rfl
 
+@[simp]
+lemma card_factors_one : Ω 1 = 0 := rfl
+
 lemma card_factors_eq_one_iff_prime {n : ℕ} :
   Ω n = 1 ↔ n.prime :=
 begin
@@ -618,6 +622,61 @@ begin
   { simp [h, pow_ne_zero] }
 end
 
+lemma moebius_ne_zero_iff_eq_or {n : ℕ} : μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1 :=
+begin
+  split; intro h,
+  { rw moebius_ne_zero_iff_squarefree at h,
+    rw moebius_apply_of_squarefree h,
+    apply neg_one_pow_eq_or },
+  { rcases h with h | h; simp [h] }
+end
+
+open unique_factorization_monoid
+
+/-- Moebius Inversion -/
+@[simp] lemma moebius_mul_zeta : μ * ζ = 1 :=
+begin
+  ext x,
+  cases x, simp,
+  cases x, simp,
+  rw [mul_zeta_apply, one_apply_ne (ne_of_gt (succ_lt_succ (nat.succ_pos _)))],
+  rw ← sum_filter_ne_zero,
+  simp only [moebius_ne_zero_iff_squarefree],
+  transitivity,
+  convert (sum_divisors_filter_squarefree (nat.succ_ne_zero _)),
+  apply eq.trans (sum_congr rfl _) (sum_powerset_neg_one_pow_card_of_nonempty _),
+  { intros y hy,
+    rw [finset.mem_powerset, ← finset.val_le_iff, multiset.to_finset_val] at hy,
+    have h : unique_factorization_monoid.factors y.val.prod = y.val,
+    { apply factors_multiset_prod_of_irreducible,
+      intros z hz,
+      apply irreducible_of_factor _ (multiset.subset_of_le
+        (le_trans hy (multiset.erase_dup_le _)) hz) },
+    rw [if_pos],
+    { rw [card_factors_apply, ← multiset.coe_card, ← factors_eq, h, finset.card] },
+    rw [unique_factorization_monoid.squarefree_iff_nodup_factors, h],
+    { apply y.nodup },
+    rw [ne.def, multiset.prod_eq_zero_iff],
+    intro con,
+    rw ← h at con,
+    exact not_irreducible_zero (irreducible_of_factor 0 con) },
+  { rw finset.nonempty,
+    rcases wf_dvd_monoid.exists_irreducible_factor _ (nat.succ_ne_zero _) with ⟨i, hi⟩,
+    { rcases exists_mem_factors_of_dvd (nat.succ_ne_zero _) hi.1 hi.2 with ⟨j, hj, hj2⟩,
+      use j,
+      apply multiset.mem_to_finset.2 hj },
+    rw nat.is_unit_iff,
+    omega },
+end
+
+@[simp] lemma zeta_mul_moebius : ζ * μ = 1 :=
+by rw [mul_comm, moebius_mul_zeta]
+
+instance : invertible ζ :=
+{ inv_of := μ,
+  inv_of_mul_self := moebius_mul_zeta,
+  mul_inv_of_self := zeta_mul_moebius}
+
 end special_functions
 end arithmetic_function
 end nat

src/ring_theory/int/basic.lean

@@ -300,6 +300,17 @@ begin
     apply nat.mem_factors hx, }
 end
 
+lemma nat.factors_multiset_prod_of_irreducible
+  {s : multiset ℕ} (h : ∀ (x : ℕ), x ∈ s → irreducible x) :
+  unique_factorization_monoid.factors (s.prod) = s :=
+begin
+  rw [← multiset.rel_eq, ← associated_eq_eq],
+  apply (unique_factorization_monoid.factors_unique irreducible_of_factor h (factors_prod _)),
+  rw [ne.def, multiset.prod_eq_zero_iff],
+  intro con,
+  exact not_irreducible_zero (h 0 con),
+end
+
 namespace multiplicity
 
 lemma finite_int_iff_nat_abs_finite {a b : ℤ} : finite a b ↔ finite a.nat_abs b.nat_abs :=