Abundant, Semi-perfect, Deficient & Weird Numbers

Stream: mathlib4

[Colin Jones ⚛️]

This is an incomplete file that I am currently working on that defines what abundant, semi-perfect, deficient, and weird numbers are.

I don't know how to add to Mathlib, but nonetheless it is not complete anyways. I am welcome to thoughts. I am not a mathematician so let me know if there are any mistakes.

Here are the contents of the file:

import Mathlib

open Nat
open BigOperators
open Finset

/- This file defines abundant, semi-perfect / pseudoperfect, deficient, and weird numbers
  Abundant := A number is called abundant if its proper divisors add to more than itself
  SemiPerfect := A number is semi-perfect / pseudoperfect if at least one subset of its proper divisors adds to itself
  Deficient := A number is deficient if the sum of its proper divisors is less than itself
  Weird := A number is weird if it is abundant and NOT semi-perfect
-/
def Nat.Abundant (n : ℕ) : Prop := ∑ i in Nat.properDivisors n, i > n

def Nat.SemiPerfect (n : ℕ) : Prop := ∃ (s : Finset ℕ), s ∈ Finset.powerset (Nat.properDivisors n) ∧ ∑ i in s, i = n

def Nat.WeirdNumber (n : ℕ) : Prop := Nat.Abundant n ∧ ¬ Nat.SemiPerfect n

def Nat.Deficient (n : ℕ) : Prop := ∀ s ∈ Finset.powerset (Nat.properDivisors n), ∑ i in s, i < n

theorem DeficientNotAbundantOrPerfect (n : ℕ) : Nat.Deficient n ↔ ¬ (Nat.Abundant n ∨ Nat.Perfect n) := by
  rw [not_or]; dsimp [Nat.Deficient, Nat.Abundant, Nat.Perfect]; constructor;
  intro h; constructor; intro h1
  have h2 : ∃ (s : Finset ℕ), s ∈ powerset (properDivisors n) ∧ ∑ i in properDivisors n, i > n := by
    use (properDivisors n); constructor; exact mem_powerset_self (properDivisors n); exact h1
  have h3 : ∀ (s : Finset ℕ),  s ∈ powerset (properDivisors n) → ∑ i in properDivisors n, i < n := by
    sorry
  sorry
  sorry
  sorry

theorem DeficientORPerfectORAbundant (n : ℕ) : Nat.Deficient n ∨ Nat.Abundant n ∨ Nat.Perfect n := by sorry

theorem NotSemiPerfectRw (n : ℕ) :
  ¬ Nat.SemiPerfect n ↔ ∀ (s : Finset ℕ), s ∈ Finset.powerset (Nat.properDivisors n)
  → ∑ i in s, i ≠ n := by
  constructor; intro h; intro s hs; rw [ne_eq]; revert hs; apply not_and.mp; revert s; rw [← not_exists]; exact h
  intro h1; dsimp [SemiPerfect]; rw [not_exists]; intro x; apply not_and.mpr; intro hx; rw [← ne_eq]; revert x; exact fun x hx => h1 x hx

theorem PerfectimpSemiPerfect (n : ℕ) : Nat.Perfect n → Nat.SemiPerfect n := by
  dsimp [Nat.Perfect, Nat.SemiPerfect]; intro h; rcases h with ⟨h1, h2⟩
  use (properDivisors n); refine (and_iff_right ?h.ha).mpr h1
  exact mem_powerset_self (properDivisors n)

theorem PrimeNotAbundant (n : ℕ) : Nat.Prime n → ¬ Nat.Abundant n := by
  dsimp [Nat.Prime, Nat.Abundant]; intro h h1;
  have h3 : ∑ i in properDivisors n, i = 1 := by exact sum_properDivisors_eq_one_iff_prime.mpr h
  have h4 : n > 1 := by exact Prime.one_lt h
  have h5 : ∑ i in properDivisors n, i > 1 := by exact Nat.lt_trans h4 h1
  have h6 : 1 > 1 := by
    calc
      1 = ∑ i in properDivisors n, i := by apply Eq.symm h3
      _ > 1 := by rel [h5]
  contradiction

theorem NotSemiPerfectNotPerfect (n : ℕ) : ¬ Nat.SemiPerfect n → ¬ Nat.Perfect n := by
  rw [not_imp_not]; exact PerfectimpSemiPerfect n

theorem PrimeNotSemiPerfect (n : ℕ) : Nat.Prime n → ¬ Nat.SemiPerfect n := by
  intro h; rw [NotSemiPerfectRw];
  have h1 : powerset (properDivisors n) = {∅, {1}} := by rw [Prime.properDivisors h]; exact rfl
  have h2 : n > 1 := by exact Prime.one_lt h
  rw [h1]; rintro s hs; have hs' : s = ∅ ∨ s = {1} := by exact List.mem_pair.mp hs
  rcases hs' with hs1 | hs2
  repeat (first | simp [hs1]; linarith | simp [hs2]; linarith)

theorem PrimeNotPerfect (n : ℕ) : Nat.Prime n → ¬ Nat.Perfect n := by
  intro h; have h1 : ¬ SemiPerfect n := by exact PrimeNotSemiPerfect n h
  exact NotSemiPerfectNotPerfect n h1

/- ### Examples ### -/
#eval Finset.powerset (Nat.properDivisors 8)
example : SemiPerfect 6 := by
  dsimp [SemiPerfect]
  use {1,2,3}
  constructor
  exact mem_powerset_self {1, 2, 3}
  norm_num
example : SemiPerfect 12 := by
  dsimp [SemiPerfect]; use {2,4,6}; constructor;
  have hn : properDivisors 12 = {1,2,3,4,6} := by exact rfl
  rw [hn]
  apply Finset.mem_powerset.mpr
  simp [*]
  norm_num
#eval Nat.properDivisors 7
#eval ∑ i in Nat.properDivisors 7, i
example : Abundant 70 := by dsimp [Abundant]; norm_num
example : ¬ SemiPerfect 7 := by
  dsimp [SemiPerfect]; rw [not_exists]; intro x; apply not_and.mpr
  have h1 : ¬∑ i in x, i = 7 ↔ ∑ i in x, i ≠ 7 := by exact Iff.rfl
  intro h2; apply h1.mpr
  refine Nat.ne_of_lt ?h
  aesop
  rw [show properDivisors 7 = {1} by exact rfl] at h2
  have h3 : x = ∅ ∨ x = {1} := by exact subset_singleton_iff.mp h2
  rcases h3 with h4 | h5
  rw [h4]; norm_num
  rw [h5]; norm_num
example : ¬ SemiPerfect 4 := by
  dsimp [SemiPerfect]; rw [not_exists]; rintro x; apply not_and.mpr
  have h1 : ¬∑ i in x, i = 4 ↔ ∑ i in x, i ≠ 4 := by exact Iff.rfl
  intro h2; apply h1.mpr; refine Nat.ne_of_lt ?h;
  rw [show properDivisors 4 = {1,2} by exact rfl] at h2
  rw [show powerset {1,2} = {∅, {1}, {2}, {1,2}} by exact rfl] at h2
  have h3 : x ∈ ({∅, {1}, {2}, {1,2}} : Finset (Finset ℕ)) → (x = ∅ ∨ x = {1} ∨ x = {2} ∨ x = {1,2}) := by simp only [mem_singleton, mem_insert, imp_self]
  have h4 := by apply h3 h2
  rcases h4 with (h5 | h6) | (h7 | h8)
  simp [*]; rw [h7]; simp [*]; rcases h8 with h9 | h10
  rw [h9]; simp [*]; rw [h10]; simp [*]
example {a b : ℝ} : ¬ (a = b) ↔ a ≠ b := by rw [@not_iff_not]
example : WeirdNumber 70 := by
  constructor
  dsimp [Abundant]
  norm_num
  dsimp [SemiPerfect]; rw [not_exists]; rintro x; apply not_and.mpr
  have h1 : ¬∑ i in x, i = 70 ↔ ∑ i in x, i ≠ 70 := by exact Iff.rfl
  intro h2; apply h1.mpr; refine Nat.ne_of_lt ?h;
  rw [show properDivisors 70 = {1, 2, 5, 7, 10, 14, 35} by exact rfl] at h2
  sorry

example {x : Finset ℕ} : x ∈ ({∅, {1}, {2}, {1,2}} : Finset (Finset ℕ)) ↔ (x = ∅ ∨ x = {1} ∨ x = {2} ∨ x = {1,2}) := by
  simp only [mem_singleton, mem_insert]

example {x : ℕ} : x ∈ ({1, 3} : Finset ℕ) ↔ x = 1 ∨ x = 3 := by simp only [mem_singleton, mem_insert]
#eval powerset (properDivisors 70)
example : Abundant 12 := by
  dsimp [Abundant]
  simp [*]

[Colin Jones ⚛️]

I will update this file on my github : https://github.com/Colin166/Lean4/blob/main/NatNumberCategories

[Colin Jones ⚛️]

I plan to make the definitions based on the fact that zero shouldn't be in the definitions in the near future.

[Kevin Buzzard]

For Deficient, why bother with the finset? And is 0 supposed to be semiperfect?

[Emilie (Shad Amethyst)]

Set.Finite is usually what you want if you just need to check that the set is finite

[Colin Jones ⚛️]

Kevin Buzzard said:

For Deficient, why bother with the finset? And is 0 supposed to be semiperfect?

Should I omit zero from the definitions?

I would think that zero is an abundant number as it technically qualifies; however, it is impossible to prove as Nat.properDivisors 0 returns an empty set. Although thinking on it, zero should not be a semi-perfect number so I will add that requirement in the semi-perfect definition.

[Kim Morrison]

preperfect!

[Colin Jones ⚛️]

I have removed zero from all the definitions since Nat.Perfect does that as well. I have also fixed the Nat.Deficient definition. How can I add this file to Mathlib if you all would want it?

Here are the contents of the file:

import Mathlib

open Nat
open BigOperators
open Finset

/- This file defines abundant, semi-perfect / pseudoperfect, deficient, and weird numbers
  Abundant := A number is called abundant if its proper divisors add to more than itself
  SemiPerfect := A number is semi-perfect / pseudoperfect if at least one subset of its proper divisors adds to itself
  Deficient := A number is deficient if the sum of its proper divisors is less than itself
  Weird := A number is weird if it is abundant and NOT semi-perfect
  I have excluded zero from the definitions because zero is also excluded from the Nat.Perfect definition.
-/
def Nat.Abundant (n : ℕ) : Prop := ∑ i in Nat.properDivisors n, i > n ∧ 0 < n

def Nat.SemiPerfect (n : ℕ) : Prop := ∃ s : Finset ℕ, s ∈ Finset.powerset (Nat.properDivisors n) ∧ ∑ i in s, i = n ∧ 0 < n

def Nat.WeirdNumber (n : ℕ) : Prop := Nat.Abundant n ∧ ¬ Nat.SemiPerfect n

def Nat.Deficient (n : ℕ) : Prop := ∑ i in Nat.properDivisors n, i < n ∧ 0 < n

theorem OneDeficient : Nat.Deficient 1 := by
  dsimp [Deficient]
  norm_num

theorem DeficientNotAbundantOrPerfect (n : ℕ) (hn : 0 < n) : Nat.Deficient n ↔ ¬ (Nat.Abundant n ∨ Nat.Perfect n) := by
  rw [not_or]; dsimp [Nat.Deficient, Nat.Abundant, Nat.Perfect];
  constructor; rintro ⟨h1, h2⟩; rw [not_and_or, not_and_or]
  · constructor;
    left; exact Nat.lt_asymm h1; left; exact Nat.ne_of_lt h1
  · rintro ⟨h1, h2⟩;
    rw [not_and_or] at h1; rw [not_and_or] at h2
    constructor
    have f1 : · i in properDivisors n, i > n := by
      rcases h1 with w1 | w2; assumption; contradiction
    have f2 : · i in properDivisors n, i = n := by
      rcases h2 with w1 | w2; assumption; contradiction
    rw [not_lt] at f1; rw [← ne_eq] at f2
    exact lt_of_le_of_ne f1 f2
    exact hn

theorem PerfectNotAbundantOrDeficient (n : ℕ) (hn : 0 < n) : Nat.Perfect n ↔ ¬ (Nat.Abundant n ∨ Nat.Deficient n) := by
  rw [Iff.comm, ← not_iff];
  dsimp [Nat.Abundant, Nat.Perfect, Nat.Deficient]
  rintro ⟨h1, h2⟩
  have f1 : ∑ i in properDivisors n, i > n ∧ 0 < n ↔ ∑ i in properDivisors n, i > n := by
    exact and_iff_left hn
  have f2 : ∑ i in properDivisors n, i < n ∧ 0 < n ↔ ∑ i in properDivisors n, i < n := by
    exact and_iff_left hn
  have f3 : ∑ i in properDivisors n, i = n ∧ 0 < n ↔ ∑ i in properDivisors n, i = n := by
    exact and_iff_left hn
  rw [f1, f2, f3, lt_or_lt_iff_ne] at h1; rw [f1, f2, f3, lt_or_lt_iff_ne] at h2
  have h1' : ∑ i in properDivisors n, i ≠ n → ∑ i in properDivisors n, i = n := by exact fun a => h1 (id (Ne.symm a))
  have h2' : ∑ i in properDivisors n, i = n → ∑ i in properDivisors n, i ≠ n := by exact fun a => (h2 (h1 (h2 a)) (id a.symm)).elim
  by_cases hP : ∑ i in properDivisors n, i = n
  have contra1 := by apply h2' hP; exact hP
  exact contra1
  have contra2 := by apply h1' hP
  rw [← ne_eq] at hP
  contradiction

theorem AbundantNotPerfectOrDeficient (n : ℕ) (hn : 0 < n) : Nat.Abundant n ↔ ¬ (Nat.Perfect n ∨ Nat.Deficient n) := by
  rw [not_or]; dsimp [Nat.Deficient, Nat.Abundant, Nat.Perfect];
  constructor; rintro ⟨h1, h2⟩; rw [not_and_or, not_and_or]
  · constructor;
    left; exact Nat.ne_of_gt h1; left; exact Nat.lt_asymm h1
  · rintro ⟨h1, h2⟩;
    rw [not_and_or] at h1; rw [not_and_or] at h2
    constructor
    rcases h1 with w1 | w2; rcases h2 with f1 | f2
    rw [← ne_eq] at w1; rw [not_lt] at f1
    exact Nat.lt_of_le_of_ne f1 (id (Ne.symm w1))
    repeat contradiction
    exact hn

theorem DeficientOrPerfectOrAbundant (n : ℕ) (hn : 0 < n) : Nat.Deficient n ∨ Nat.Abundant n ∨ Nat.Perfect n := by
  dsimp [Nat.Deficient, Nat.Perfect, Nat.Abundant]
  by_contra hc
  rw [not_or, not_or] at hc
  rcases hc with ⟨hc1, ⟨hc2, hc3⟩⟩
  have f1 : ∑ i in properDivisors n, i > n ∧ 0 < n ↔ ∑ i in properDivisors n, i > n := by
    exact and_iff_left hn
  have f2 : ∑ i in properDivisors n, i < n ∧ 0 < n ↔ ∑ i in properDivisors n, i < n := by
    exact and_iff_left hn
  have f3 : ∑ i in properDivisors n, i = n ∧ 0 < n ↔ ∑ i in properDivisors n, i = n := by
    exact and_iff_left hn
  rw [f1] at hc2; rw [f2] at hc1; rw [f3] at hc3
  rw [not_lt] at hc1; rw [not_lt] at hc2
  have f4 : ∑ i in properDivisors n, i = n := by exact le_antisymm hc2 hc1
  contradiction

theorem NotSemiPerfectRw (n : ℕ) :
  (¬ Nat.SemiPerfect n) ↔ ∀ (s : Finset ℕ), s ∈ Finset.powerset (Nat.properDivisors n)
  → (∑ i in s, i ≠ n ∨ 0 ≥ n) := by
  dsimp [Nat.SemiPerfect]; rw [not_exists]; constructor;
  intro h s;
  have hs : ¬(s ∈ powerset (properDivisors n) ∧ ∑ i in s, i = n ∧ 0 < n) := by apply h s
  rw [not_and, not_and_or, not_lt] at hs; exact hs
  intro h x;
  have hx : x ∈ powerset (properDivisors n) → ¬∑ i in x, i = n ∨ 0 ≥ n := by apply h x
  rw [not_and, not_and_or, not_lt]; exact fun a => h x a

theorem PerfectImpSemiPerfect (n : ℕ) : Nat.Perfect n → Nat.SemiPerfect n := by
  intro h; obtain ⟨h1, h2⟩ := h; use properDivisors n;
  constructor; exact mem_powerset_self (properDivisors n)
  constructor <;> assumption

theorem PrimeNotAbundant (n : ℕ) : Nat.Prime n → ¬ Nat.Abundant n := by
  intro h h1; rcases h1 with ⟨h1, h2⟩
  have h3 : ∑ i in properDivisors n, i = 1 := by exact sum_properDivisors_eq_one_iff_prime.mpr h
  have h4 : n > 1 := by exact Prime.one_lt h
  have h5 : ∑ i in properDivisors n, i > 1 := by exact Nat.lt_trans h4 h1
  have h6 : 1 > 1 := by
    calc
      1 = ∑ i in properDivisors n, i := by apply Eq.symm h3
      _ > 1 := by rel [h5]
  contradiction

theorem NotSemiPerfectNotPerfect (n : ℕ) : ¬ Nat.SemiPerfect n → ¬ Nat.Perfect n := by
  rw [not_imp_not]; exact PerfectImpSemiPerfect n

theorem PrimeNotSemiPerfect (n : ℕ) : Nat.Prime n → ¬ Nat.SemiPerfect n := by
  intro h; rw [NotSemiPerfectRw]
  have h1 : powerset (properDivisors n) = {∅, {1}} := by rw [Prime.properDivisors h]; exact rfl
  have h2 : n > 1 := by exact Prime.one_lt h
  rw [h1]; rintro s hs; have hs' : s = ∅ ∨ s = {1} := by exact List.mem_pair.mp hs
  rcases hs' with hs1 | hs2
  <;> {left; repeat (first | simp [hs1]; linarith | simp [hs2]; linarith)}

theorem PrimeNotPerfect (n : ℕ) : Nat.Prime n → ¬ Nat.Perfect n := by
  intro h; have h1 : ¬ SemiPerfect n := by exact PrimeNotSemiPerfect n h
  exact NotSemiPerfectNotPerfect n h1

There should be no errors and it should be complete.

[Damiano Testa]

Using a little of the available automation, you can simplify some of the proofs (note that I changed the defs to abbrevs in order not to have to unfold them all the times):

import Mathlib

open Nat
open BigOperators
open Finset

/- This file defines abundant, semi-perfect / pseudoperfect, deficient, and weird numbers
  Abundant := A number is called abundant if its proper divisors add to more than itself
  SemiPerfect := A number is semi-perfect / pseudoperfect if at least one subset of its proper divisors adds to itself
  Deficient := A number is deficient if the sum of its proper divisors is less than itself
  Weird := A number is weird if it is abundant and NOT semi-perfect
  I have excluded zero from the definitions because zero is also excluded from the Nat.Perfect definition.
-/
abbrev Nat.Abundant (n : ℕ) : Prop := ∑ i in Nat.properDivisors n, i > n ∧ 0 < n

abbrev Nat.SemiPerfect (n : ℕ) : Prop := ∃ s : Finset ℕ, s ∈ Finset.powerset (Nat.properDivisors n) ∧ ∑ i in s, i = n ∧ 0 < n

abbrev Nat.WeirdNumber (n : ℕ) : Prop := Nat.Abundant n ∧ ¬ Nat.SemiPerfect n

abbrev Nat.Deficient (n : ℕ) : Prop := ∑ i in Nat.properDivisors n, i < n ∧ 0 < n

theorem OneDeficient : Nat.Deficient 1 := by norm_num [Nat.Deficient]

theorem DeficientNotAbundantOrPerfect (n : ℕ) (hn : 0 < n) : Nat.Deficient n ↔ ¬ (Nat.Abundant n ∨ Nat.Perfect n) := by
  unfold Nat.Perfect
  omega

theorem PerfectNotAbundantOrDeficient (n : ℕ) (hn : 0 < n) : Nat.Perfect n ↔ ¬ (Nat.Abundant n ∨ Nat.Deficient n) := by
  unfold Nat.Perfect
  omega

theorem AbundantNotPerfectOrDeficient (n : ℕ) (hn : 0 < n) : Nat.Abundant n ↔ ¬ (Nat.Perfect n ∨ Nat.Deficient n) := by
  unfold Nat.Perfect
  omega

theorem DeficientOrPerfectOrAbundant (n : ℕ) (hn : 0 < n) : Nat.Deficient n ∨ Nat.Abundant n ∨ Nat.Perfect n := by
  unfold Nat.Perfect
  omega

theorem NotSemiPerfectRw (n : ℕ) :
  (¬ Nat.SemiPerfect n) ↔ ∀ (s : Finset ℕ), s ∈ Finset.powerset (Nat.properDivisors n)
  → (∑ i in s, i ≠ n ∨ 0 ≥ n) := by
  dsimp [Nat.SemiPerfect]; rw [not_exists];
  constructor;
  intro h s;
  have hs : ¬(s ∈ powerset (properDivisors n) ∧ ∑ i in s, i = n ∧ 0 < n) := h s
  rwa [not_and, not_and_or, not_lt] at hs
  intro h x;
  rw [not_and, not_and_or, not_lt]; exact h x

theorem PerfectImpSemiPerfect (n : ℕ) : Nat.Perfect n → Nat.SemiPerfect n := by
  unfold Nat.Perfect SemiPerfect
  aesop

theorem PrimeNotAbundant (n : ℕ) : Nat.Prime n → ¬ Nat.Abundant n := by
  unfold Nat.Abundant
  aesop

theorem NotSemiPerfectNotPerfect (n : ℕ) : ¬ Nat.SemiPerfect n → ¬ Nat.Perfect n :=
  not_imp_not.mpr (PerfectImpSemiPerfect n)

theorem PrimeNotSemiPerfect (n : ℕ) : Nat.Prime n → ¬ Nat.SemiPerfect n := by
  intro h; rw [NotSemiPerfectRw]
  have h1 : powerset (properDivisors n) = {∅, {1}} := by rw [Prime.properDivisors h]; exact rfl
  aesop

theorem PrimeNotPerfect (n : ℕ) : Nat.Prime n → ¬ Nat.Perfect n := by
  unfold Nat.Perfect
  aesop

[Colin Jones ⚛️]

That’s very cool! I did not know you could do that.

[Colin Jones ⚛️]

I would like to add these theorems to Mathlib if possible. How would I do this?

[Emilie (Shad Amethyst)]

The wiki gives you a step-by-step introduction on how to do that; you will need a github account, and send your github username here or in the github permission to receive permission to create your branch on the mathlib repository, so that you get all of the benefits of the automation set up there :)

[Emilie (Shad Amethyst)]

There's also a couple of pages on the left tab of that link with guidelines on how to format your contribution to match mathlib's style

[Colin Jones ⚛️]

Thank you!