High level comments on (half-finished) proof

Stream: new members

[Gareth Ma]

Hi! I have been working towards a proof of the Euclid-Euler Theorem, which characterises all even perfect numbers. The proof is quite easy on paper but so far it's been a different story in Lean :tear: (Mostly since I am still quite new). I noticed that the proof does not in mathlib. Where is a good place to put it? Also, maybe once I get more familiar with the codebase, I can contribute to the number theory side, since some elementary things seems missing haha. Anyways, here is what I have. If anyone can give a brief look and see what I should change (apart from formatting / renaming variables), that would be great.

[Gareth Ma]

/-
TODO: Add copyright information
TODO: Add proper documentations
TODO: Decide where to put this file
-/

/-
Additional lemmas added to `src/number_theory/arithmetic_function.lean`:

lemma sigma_apply_prime_pow {n p k : ℕ} (hp : p.prime) :
  σ n (p ^ k) = if n = 0 then k + 1 else ∑ i in range (k + 1), p ^ (i * n) :=
by {
  split_ifs,
  { rw h, exact sigma_zero_apply_prime_pow hp, },
  have : p ^ n ≠ 1,
  {
    simp [(pow_eq_one_iff h).not],
    exact prime.ne_one hp,
  },
  rw [sigma_apply, divisors_prime_pow],
  simp [← pow_mul],
  exact hp,
}
-/

import algebra.geom_sum
import data.finset.basic
import data.nat.prime
import number_theory.arithmetic_function
import number_theory.divisors
import number_theory.lucas_lehmer
import tactic

open finset
open nat.arithmetic_function
open_locale arithmetic_function
open_locale big_operators

variable X : ℤ

/-
Below are results leading up to Euclid-Euler Theorem
-/

-- Thank you to Kevin Buzzard, Niels Voss and Yaël Dillies for helping with this!
theorem mersenne_div {m n : ℕ} (h : m ∣ n) : mersenne m ∣ mersenne n :=
begin
  unfold mersenne,
  rcases h with ⟨k, rfl⟩,
  simpa only [pow_mul, one_pow] using nat_sub_dvd_pow_sub_pow _ 1 _,
end

-- 2^n - 1 is Mersenne prime implies n is prime
theorem mersenne_theorem {n : ℕ} (h : nat.prime (mersenne n)) : nat.prime n :=
begin
  -- Auxillary lemma
  have two_le_n : 2 ≤ n,
  {
    by_contradiction h',
    push_neg at h',
    rw nat.lt_succ_iff at h',
    cases h' with _ h',
    { simp at h, exact nat.not_prime_one h, },
    {
      rw nat.eq_zero_of_le_zero h' at h,
      unfold mersenne at h,
      simp at h,
      exact nat.not_prime_zero h,
    }
  },
  have one_le_pow_two_n : 1 ≤ 2 ^ n,
  { apply nat.one_le_pow, omega, },

  -- Assume n is composite
  by_contradiction n_comp,
  rcases nat.exists_dvd_of_not_prime two_le_n n_comp with ⟨d, d_div, d_ne_one, d_ne_n⟩,
  have d_ne_zero : d ≠ 0,
  { by_contradiction, rw h at d_div, rw zero_dvd_iff at d_div, linarith, },
  have one_le_pow_two_d : 1 ≤ 2 ^ d,
  { apply nat.one_le_pow, omega, },
  have two_le_d : 2 ≤ d,
  { cases d, omega, cases d; omega,},
  have four_sub_one_le_pow_two_sub_one: 4 - 1 ≤ 2 ^ d - 1,
  {
    change 2 ^ 2 - 1 ≤ 2 ^ d - 1,
    rw nat.sub_le_sub_iff_right,
    exact pow_le_pow (by linarith) two_le_d,
    exact nat.one_le_pow d 2 zero_lt_two,
  },

  -- Then mersenne n is not prime
  rcases mersenne_div d_div with ⟨md, hmd⟩,
  have : ¬nat.prime (mersenne n),
  {
    apply nat.not_prime_mul' hmd.symm,
    {
      unfold mersenne,
      calc
      1 < 4 - 1 : by simp
      ... ≤ 2 ^ d - 1 : by { simp, apply four_sub_one_le_pow_two_sub_one },
    },
    {
      by_contradiction,
      push_neg at h,
      cases md,
      {
        -- Disproving (mersenne n / mersenne d) = 0
        simp at hmd,
        have : 0 < mersenne n,
        { apply mersenne_pos, linarith, },
        linarith,
      },
      {
        -- Disproving (mersenne n / mersenne d) = 1
        unfold mersenne at hmd,
        rw [nat.succ_le_iff, nat.lt_one_iff] at h,
        rw h at hmd,
        simp at hmd,
        rw (tsub_left_inj one_le_pow_two_n one_le_pow_two_d) at hmd,
        have : d = n,
        { rw eq_comm at hmd, exact nat.pow_right_injective rfl.ge hmd, },
        exact d_ne_n this,
      }
    }
  },

  exact this h,
end

-- Euclid-Euler Theorem
theorem euclid_euler {n : ℕ} :
nat.perfect n ∧ even n ↔
(∃ (p : ℕ), nat.prime (2 ^ p - 1) ∧ n = 2 ^ (p - 1) * (2 ^ p - 1)) :=
begin
  split,

  -- If n is perfect and even, then
  -- n = 2^(p - 1) (2^p - 1) and (2^p - 1) is prime
  {
    contrapose!,
    intro h,
    contrapose!,
    intro n_even,
    sorry
  },
  {
    -- If (2^p - 1) is prime, then n = 2^(p - 1) (2^p - 1) is perfect and even
    rintros ⟨p, hp₁, hp₂⟩,
    let n₁ := 2 ^ (p - 1),
    let n₂ := 2 ^ p - 1,
    have n₁_pos : 0 < n₁, { exact ne_zero.pos n₁, },
    have n₂_pos : 1 ≤ 2 ^ p, { exact nat.one_le_two_pow p, },
    have h₁ : n = n₁ * n₂, { exact hp₂, },
    have hp : nat.prime p, { exact mersenne_theorem hp₁, },
    have n₁_even : even n₁,
    {
      dsimp [n₁],
      rw nat.even_pow' ; simp,
      apply nat.prime.two_le hp,
    },

    split,
    {
      have h₂ : n₁.coprime n₂, { sorry },
      have h : σ 1 n = σ 1 n₁ * σ 1 n₂,
      { rw [h₁, is_multiplicative.map_mul_of_coprime is_multiplicative_sigma h₂], },
      have hσ₁ : ∀ (n : ℕ), σ 1 (2 ^ n) = 2 ^ (n + 1) - 1,
      {
        intro n,
        rw sigma_apply_prime_pow nat.prime_two,
        simp [nat.sub_add_cancel (nat.prime.pos hp)],

        -- Why is it so hard to prove (range p).sum (pow 2)?
        induction n with n n_ih,
        simp,
        rw [range_succ, sum_insert, n_ih, nat.succ_eq_add_one],
        rw ← nat.add_sub_assoc ((one_le_pow_iff _).2 one_le_two),
        ring_exp,
        exact ne_zero.ne (n + 1),
        exact list.not_mem_range_self,
      },
      have hσ₂ : ∀ (p : ℕ), nat.prime p → σ 1 p = 1 + p,
      {
        intros p hp,
        rw sigma_one_apply,
        rw nat.prime.sum_divisors hp,
        exact add_comm p 1,
      },
      rw nat.perfect_iff_sum_divisors_eq_two_mul,

      -- I plan to make evaluating arithmetic functions easier
      calc ∑ (i : ℕ) in n.divisors, i
            = n.divisors.sum (λ (d : ℕ), d)   : by exact rfl
        ... = σ 1 n                          : by rw sigma_one_apply
        ... = σ 1 n₁ * σ 1 n₂                 : by rw h
        ... = (2 ^ p - 1) * σ 1 n₂            : by rw [hσ₁ (p - 1),
                                                       nat.sub_add_cancel (nat.prime.pos hp)]
        ... = (2 ^ p - 1) * (1 + n₂)          : by rw [hσ₂ n₂ hp₁]
        ... = (2 ^ p - 1) * 2 ^ p             : by { dsimp [n₂] ,
                                                     rw ← nat.add_sub_assoc n₂_pos,
                                                     rw nat.add_sub_cancel_left 1 (2 ^ p), }
        ... = (2 ^ p - 1) * (2 * 2 ^ (p - 1)) : by { rw ← nat.pow_div,
                                                     simp,
                                                     left,
                                                     rw nat.mul_div_cancel',
                                                     apply nat.dvd_of_pow_dvd,
                                                     apply (nat.prime.pos hp),
                                                     apply dvd_rfl,
                                                     apply (nat.prime.pos hp),
                                                     simp, }
        ... = 2 * n                           : by { rw hp₂, ring_exp_eq },

      -- Prove n > 0
      rw hp₂,
      apply mul_pos (ne_zero.pos n₁),
      simp,
      exact nat.le_self_pow (nat.prime.ne_zero hp) 2,
    },
    {
      -- If (2^p - 1) is prime, then n = 2^(p - 1) (2^p - 1) is even
      rw [h₁, nat.even_mul],
      left,
      apply n₁_even,
    },
  },
end

[Gareth Ma]

There are a lot of random lemmas flying around since I can't find a way to do them easily or directly
Edit: I found that it's already implemented in mathlib. Oops.

[Eric Wieser]

What's the name of the lemma in mathlib?

[Kevin Buzzard]

How does the mathlib version compare to your version?

[Gareth Ma]

It's inside archives, the 100 problem archives, #70

[Gareth Ma]

Their implementation is way better than mine :joy: I'm learning from it, they use a lot of simp instead of explicitly rw everywhere

[Eric Wieser]

The file in question is here

[Eric Wieser]

Does mathlib have your mersenne_div (which should be named with dvd not div) or mersenne_theorem (which should be called prime_of_prime_mersenne or similar)?

[Gareth Ma]

The first one exists in a more general form nat_sub_dvd_pow_sub_pow, stating x - y | x^n - y^n.
The second one does not exist though, it is quite narrow, as in the theorem doesn't even generalise for base that is not 2, since X - 1 | X^n - 1.

[Eric Wieser]

I think it's still worth having even though it's a special case; you can't use that lemma without unfolding mersenne first.

[Eric Wieser]

The fact we decided hat docs#mersenne was a useful definition (even though it's a "special case" of X^n-1) means that we decided it was reasonable to state theorems about this restricted special case

[Junyan Xu]

This theorem should be in mathlib rather than the archive; and it's a shame that archive entries don't show up in generated docs.