diff --git a/archive/100-theorems-list/70_perfect_numbers.lean b/archive/100-theorems-list/70_perfect_numbers.lean index ce08c52150aed..cf5b7a059c17d 100644 --- a/archive/100-theorems-list/70_perfect_numbers.lean +++ b/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 diff --git a/docs/100.yaml b/docs/100.yaml index c3d5a5c8fbafb..85b0429de2609 100644 --- a/docs/100.yaml +++ b/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 diff --git a/src/number_theory/divisors.lean b/src/number_theory/divisors.lean index 25c84f5b86bf9..3ac1aea24db01 100644 --- a/src/number_theory/divisors.lean +++ b/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,14 +125,48 @@ 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 } @@ -139,21 +174,21 @@ lemma divisors_antidiagonal_zero : divisors_antidiagonal 0 = ∅ := by { ext, si 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, @@ -161,7 +196,7 @@ begin 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) :