feat(archive/100-theorems-list/70_perfect_numbers): Perfect Number Th…

…eorem, Direction 2 (#4621)

Adds a few extra lemmas about `divisors`, `proper_divisors` and sums of proper divisors
Proves Euler's direction of the Perfect Number theorem, finishing Freek 70

archive/100-theorems-list/70_perfect_numbers.lean

@@ -7,12 +7,12 @@ Author: Aaron Anderson.
 import number_theory.arithmetic_function
 import number_theory.lucas_lehmer
 import algebra.geom_sum
+import ring_theory.multiplicity
 
 /-!
 # Perfect Numbers
 
-This file proves (currently one direction of)
-  Theorem 70 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
+This file proves Theorem 70 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
 The theorem characterizes even perfect numbers.
 
@@ -61,4 +61,68 @@ theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).pr
   even ((2 ^ k) * mersenne (k + 1)) :=
 by simp [ne_zero_of_prime_mersenne k pr] with parity_simps
 
+lemma eq_pow_two_mul_odd {n : ℕ} (hpos : 0 < n) :
+  ∃ (k m : ℕ), n = 2 ^ k * m ∧ ¬ even m :=
+begin
+  have h := (multiplicity.finite_nat_iff.2 ⟨nat.prime_two.ne_one, hpos⟩),
+  cases multiplicity.pow_multiplicity_dvd h with m hm,
+  use [(multiplicity 2 n).get h, m],
+  refine ⟨hm, _⟩,
+  rw even_iff_two_dvd,
+  have hg := multiplicity.is_greatest' h (nat.lt_succ_self _),
+  contrapose! hg,
+  rcases hg with ⟨k, rfl⟩,
+  apply dvd.intro k,
+  rw [pow_succ', mul_assoc, ← hm],
+end
+
+/-- Euler's theorem that even perfect numbers can be factored as a
+  power of two times a Mersenne prime. -/
+theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (perf : perfect n) :
+  ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=
+begin
+  have hpos := perf.2,
+  rcases eq_pow_two_mul_odd hpos with ⟨k, m, rfl, hm⟩,
+  use k,
+  rw [perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
+    is_multiplicative_sigma.map_mul_of_coprime (nat.prime_two.coprime_pow_of_not_dvd hm).symm,
+    sigma_two_pow_eq_mersenne_succ, ← mul_assoc, ← pow_succ] at perf,
+  rcases nat.coprime.dvd_of_dvd_mul_left
+    (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (dvd.intro _ perf) with ⟨j, rfl⟩,
+  rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf,
+  have h := mul_left_cancel' (ne_of_gt (mersenne_pos (nat.succ_pos _))) perf,
+  rw [sigma_one_apply, sum_divisors_eq_sum_proper_divisors_add_self, ← succ_mersenne, add_mul,
+    one_mul, add_comm] at h,
+  have hj := add_left_cancel h,
+  cases sum_proper_divisors_dvd (by { rw hj, apply dvd.intro_left (mersenne (k + 1)) rfl }),
+  { have j1 : j = 1 := eq.trans hj.symm h_1,
+    rw [j1, mul_one, sum_proper_divisors_eq_one_iff_prime] at h_1,
+    simp [h_1, j1] },
+  { have jcon := eq.trans hj.symm h_1,
+    rw [← one_mul j, ← mul_assoc, mul_one] at jcon,
+    have jcon2 := mul_right_cancel' _ jcon,
+    { exfalso,
+      cases k,
+      { apply hm,
+        rw [← jcon2, pow_zero, one_mul, one_mul] at ev,
+        rw [← jcon2, one_mul],
+        exact ev },
+      apply ne_of_lt _ jcon2,
+      rw [mersenne, ← nat.pred_eq_sub_one, lt_pred_iff, ← pow_one (nat.succ 1)],
+      apply pow_lt_pow (nat.lt_succ_self 1) (nat.succ_lt_succ (nat.succ_pos k)) },
+    contrapose! hm,
+    simp [hm] }
+end
+
+/-- The Euclid-Euler theorem characterizing even perfect numbers -/
+theorem even_and_perfect_iff {n : ℕ} :
+  (even n ∧ perfect n) ↔ ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=
+begin
+  split,
+  { rintro ⟨ev, perf⟩,
+    exact eq_two_pow_mul_prime_mersenne_of_even_perfect ev perf },
+  { rintro ⟨k, pr, rfl⟩,
+    exact ⟨even_two_pow_mul_mersenne_of_prime k pr, perfect_two_pow_mul_mersenne_of_prime k pr⟩ }
+end
+
 end nat

docs/100.yaml

@@ -224,6 +224,9 @@
   author : mathlib
 70:
   title  : The Perfect Number Theorem
+  links  :
+    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/70_perfect_numbers.lean
+  author : Aaron Anderson
 71:
   title  : Order of a Subgroup
   decl   : card_subgroup_dvd_card

src/number_theory/divisors.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import algebra.big_operators.basic
+import algebra.big_operators.order
 import tactic
 
 /-!
@@ -29,6 +29,7 @@ divisors, perfect numbers
 
 open_locale classical
 open_locale big_operators
+open finset
 
 namespace nat
 variable (n : ℕ)
@@ -124,44 +125,78 @@ begin
   exact nat.le_of_dvd (nat.succ_pos m),
 end
 
-variable (n)
-
 @[simp]
 lemma divisors_zero : divisors 0 = ∅ := by { ext, simp }
 
 @[simp]
 lemma proper_divisors_zero : proper_divisors 0 = ∅ := by { ext, simp }
 
+lemma proper_divisors_subset_divisors : proper_divisors n ⊆ divisors n :=
+begin
+  cases n,
+  { simp },
+  rw [divisors_eq_proper_divisors_insert_self_of_pos (nat.succ_pos _)],
+  apply subset_insert,
+end
+
+@[simp]
+lemma divisors_one : divisors 1 = {1} := by { ext, simp }
+
+@[simp]
+lemma proper_divisors_one : proper_divisors 1 = ∅ :=
+begin
+  ext,
+  simp only [finset.not_mem_empty, nat.dvd_one, not_and, not_lt, mem_proper_divisors, iff_false],
+  apply ge_of_eq,
+end
+
+lemma pos_of_mem_divisors {m : ℕ} (h : m ∈ n.divisors) : 0 < m :=
+begin
+  cases m,
+  { rw [mem_divisors, zero_dvd_iff] at h,
+    rcases h with ⟨rfl, h⟩,
+    exfalso,
+    apply h rfl },
+  apply nat.succ_pos,
+end
+
+lemma pos_of_mem_proper_divisors {m : ℕ} (h : m ∈ n.proper_divisors) : 0 < m :=
+pos_of_mem_divisors (proper_divisors_subset_divisors h)
+
+lemma one_mem_proper_divisors_iff_one_lt :
+  1 ∈ n.proper_divisors ↔ 1 < n :=
+by rw [mem_proper_divisors, and_iff_right (one_dvd _)]
+
 @[simp]
 lemma divisors_antidiagonal_zero : divisors_antidiagonal 0 = ∅ := by { ext, simp }
 
 @[simp]
 lemma divisors_antidiagonal_one : divisors_antidiagonal 1 = {(1,1)} :=
 by { ext, simp [nat.mul_eq_one_iff, prod.ext_iff], }
 
-lemma swap_mem_divisors_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ divisors_antidiagonal n) :
+lemma swap_mem_divisors_antidiagonal {x : ℕ × ℕ} (h : x ∈ divisors_antidiagonal n) :
   x.swap ∈ divisors_antidiagonal n :=
 begin
   rw [mem_divisors_antidiagonal, mul_comm] at h,
   simp [h.1, h.2],
 end
 
-lemma fst_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ divisors_antidiagonal n) :
+lemma fst_mem_divisors_of_mem_antidiagonal {x : ℕ × ℕ} (h : x ∈ divisors_antidiagonal n) :
   x.fst ∈ divisors n :=
 begin
   rw mem_divisors_antidiagonal at h,
   simp [dvd.intro _ h.1, h.2],
 end
 
-lemma snd_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ divisors_antidiagonal n) :
+lemma snd_mem_divisors_of_mem_antidiagonal {x : ℕ × ℕ} (h : x ∈ divisors_antidiagonal n) :
   x.snd ∈ divisors n :=
 begin
   rw mem_divisors_antidiagonal at h,
   simp [dvd.intro_left _ h.1, h.2],
 end
 
 @[simp]
-lemma map_swap_divisors_antidiagonal {n : ℕ} :
+lemma map_swap_divisors_antidiagonal :
   (divisors_antidiagonal n).map ⟨prod.swap, prod.swap_right_inverse.injective⟩
   = divisors_antidiagonal n :=
 begin
@@ -190,10 +225,10 @@ end
   is positive. -/
 def perfect (n : ℕ) : Prop := (∑ i in proper_divisors n, i = n) ∧ 0 < n
 
-theorem perfect_iff_sum_proper_divisors {n : ℕ} (h : 0 < n) :
+theorem perfect_iff_sum_proper_divisors (h : 0 < n) :
   perfect n ↔ ∑ i in proper_divisors n, i = n := and_iff_left h
 
-theorem perfect_iff_sum_divisors_eq_two_mul {n : ℕ} (h : 0 < n) :
+theorem perfect_iff_sum_divisors_eq_two_mul (h : 0 < n) :
   perfect n ↔ ∑ i in divisors n, i = 2 * n :=
 begin
   rw [perfect_iff_sum_proper_divisors h, sum_divisors_eq_sum_proper_divisors_add_self, two_mul],
@@ -206,7 +241,7 @@ lemma mem_divisors_prime_pow {p : ℕ} (pp : p.prime) (k : ℕ) {x : ℕ} :
   x ∈ divisors (p ^ k) ↔ ∃ (j : ℕ) (H : j ≤ k), x = p ^ j :=
 by rw [mem_divisors, nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]
 
-lemma divisors_prime {p : ℕ} (pp : p.prime) :
+lemma prime.divisors {p : ℕ} (pp : p.prime) :
   divisors p = {1, p} :=
 begin
   ext,
@@ -217,26 +252,100 @@ begin
   apply one_dvd,
 end
 
+lemma prime.proper_divisors {p : ℕ} (pp : p.prime) :
+  proper_divisors p = {1} :=
+by rw [← erase_insert (proper_divisors.not_self_mem),
+    ← divisors_eq_proper_divisors_insert_self_of_pos pp.pos,
+    pp.divisors, insert_singleton_comm, erase_insert (λ con, pp.ne_one (mem_singleton.1 con))]
+
 lemma divisors_prime_pow {p : ℕ} (pp : p.prime) (k : ℕ) :
   divisors (p ^ k) = (finset.range (k + 1)).map ⟨pow p, pow_right_injective pp.two_le⟩ :=
 by { ext, simp [mem_divisors_prime_pow, pp, nat.lt_succ_iff, @eq_comm _ a] }
 
-open finset
+lemma eq_proper_divisors_of_subset_of_sum_eq_sum {s : finset ℕ} (hsub : s ⊆ n.proper_divisors) :
+  ∑ x in s, x = ∑ x in n.proper_divisors, x → s = n.proper_divisors :=
+begin
+  cases n,
+  { rw [proper_divisors_zero, subset_empty] at hsub,
+    simp [hsub] },
+  classical,
+  rw [← sum_sdiff hsub],
+  intros h,
+  apply subset.antisymm hsub,
+  rw [← sdiff_eq_empty_iff_subset],
+  contrapose h,
+  rw [← ne.def, ← nonempty_iff_ne_empty] at h,
+  apply ne_of_lt,
+  rw [← zero_add (∑ x in s, x), ← add_assoc, add_zero],
+  apply add_lt_add_right,
+  have hlt := sum_lt_sum_of_nonempty h (λ x hx, pos_of_mem_proper_divisors (sdiff_subset _ _ hx)),
+  simp only [sum_const_zero] at hlt,
+  apply hlt
+end
+
+lemma sum_proper_divisors_dvd (h : ∑ x in n.proper_divisors, x ∣ n) :
+  (∑ x in n.proper_divisors, x = 1) ∨ (∑ x in n.proper_divisors, x = n) :=
+begin
+  cases n,
+  { simp },
+  cases n,
+  { contrapose! h,
+    simp, },
+  rw or_iff_not_imp_right,
+  intro ne_n,
+  have hlt : ∑ x in n.succ.succ.proper_divisors, x < n.succ.succ :=
+    lt_of_le_of_ne (nat.le_of_dvd (nat.succ_pos _) h) ne_n,
+  symmetry,
+  rw [← mem_singleton, eq_proper_divisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
+        (mem_proper_divisors.2 ⟨h, hlt⟩)) sum_singleton, mem_proper_divisors],
+  refine ⟨one_dvd _, nat.succ_lt_succ (nat.succ_pos _)⟩,
+end
 
 @[simp]
-lemma sum_divisors_prime {α : Type*} [add_comm_monoid α] {p : ℕ} {f : ℕ → α} (h : p.prime) :
+lemma prime.sum_proper_divisors {α : Type*} [add_comm_monoid α] {p : ℕ} {f : ℕ → α} (h : p.prime) :
+  ∑ x in p.proper_divisors, f x = f 1 :=
+by simp [h.proper_divisors]
+
+@[simp]
+lemma prime.sum_divisors {α : Type*} [add_comm_monoid α] {p : ℕ} {f : ℕ → α} (h : p.prime) :
   ∑ x in p.divisors, f x = f p + f 1 :=
+by rw [divisors_eq_proper_divisors_insert_self_of_pos h.pos,
+       sum_insert proper_divisors.not_self_mem, h.sum_proper_divisors]
+
+lemma proper_divisors_eq_singleton_one_iff_prime :
+  n.proper_divisors = {1} ↔ n.prime :=
+⟨λ h, begin
+  have h1 := mem_singleton.2 rfl,
+  rw [← h, mem_proper_divisors] at h1,
+  refine ⟨h1.2, _⟩,
+  intros m hdvd,
+  rw [← mem_singleton, ← h, mem_proper_divisors],
+  cases lt_or_eq_of_le (nat.le_of_dvd (lt_trans (nat.succ_pos _) h1.2) hdvd),
+  { left,
+    exact ⟨hdvd, h_1⟩ },
+  { right,
+    exact h_1 }
+end, prime.proper_divisors⟩
+
+lemma sum_proper_divisors_eq_one_iff_prime :
+  ∑ x in n.proper_divisors, x = 1 ↔ n.prime :=
 begin
-  simp only [h, divisors_prime],
-  rw [sum_insert, sum_singleton, add_comm],
-  rw mem_singleton,
-  apply h.ne_one.symm,
+  cases n,
+  { simp [nat.not_prime_zero] },
+  cases n,
+  { simp [nat.not_prime_one] },
+  rw [← proper_divisors_eq_singleton_one_iff_prime],
+  refine ⟨λ h, _, λ h, h.symm ▸ sum_singleton⟩,
+  rw [@eq_comm (finset ℕ) _ _],
+  apply eq_proper_divisors_of_subset_of_sum_eq_sum
+    (singleton_subset_iff.2 (one_mem_proper_divisors_iff_one_lt.2 (succ_lt_succ (nat.succ_pos _))))
+    (eq.trans sum_singleton h.symm)
 end
 
 @[simp]
 lemma prod_divisors_prime {α : Type*} [comm_monoid α] {p : ℕ} {f : ℕ → α} (h : p.prime) :
   ∏ x in p.divisors, f x = f p * f 1 :=
-@sum_divisors_prime (additive α) _ _ _ h
+@prime.sum_divisors (additive α) _ _ _ h
 
 @[simp]
 lemma sum_divisors_prime_pow {α : Type*} [add_comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : p.prime) :