Factorisation properties of natural numbers

This file defines abundant, pseudoperfect, deficient, and weird numbers and formalizes their relations with prime and perfect numbers.

Main Definitions

• Nat.Abundant: a natural number n is abundant if the sum of its proper divisors is greater than n
• Nat.Pseudoperfect: a natural number n is pseudoperfect if the sum of a subset of its proper divisors equals n
• Nat.Deficient: a natural number n is deficient if the sum of its proper divisors is less than n
• Nat.Weird: a natural number is weird if it is abundant but not pseudoperfect

Main Results

• Nat.deficient_or_perfect_or_abundant: A positive natural number is either deficient, perfect, or abundant.
• Nat.Prime.deficient: All prime natural numbers are deficient.
• Nat.infinite_deficient: There are infinitely many deficient numbers.
• Nat.Prime.deficient_pow: Any natural number power of a prime is deficient.

Implementation Notes

• Zero is not included in any of the definitions and these definitions only apply to natural numbers greater than zero.

References

• [R. W. Prielipp, PERFECT NUMBERS, ABUNDANT NUMBERS, AND DEFICIENT NUMBERS][Prielipp1970]

Tags

abundant, deficient, weird, pseudoperfect

def Nat.Abundant (n : ℕ) : Prop

n : ℕ is abundant if the sum of the proper divisors of n is greater than n.

def Nat.Deficient (n : ℕ) : Prop

n : ℕ is deficient if the sum of the proper divisors of n is less than n.

def Nat.Pseudoperfect (n : ℕ) : Prop

A positive natural number n is pseudoperfect if there exists a subset of the proper divisors of n such that the sum of that subset is equal to n.

def Nat.Weird (n : ℕ) : Prop

n : ℕ is a weird number if and only if it is abundant but not pseudoperfect.

theorem Nat.not_pseudoperfect_iff_forall {n : ℕ} : ¬n.Pseudoperfect ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

theorem Nat.deficient_one : Deficient 1

theorem Nat.deficient_two : Deficient 2

theorem Nat.deficient_three : Deficient 3

theorem Nat.abundant_twelve : Abundant 12

theorem Nat.weird_seventy : Weird 70

theorem Nat.deficient_iff_not_abundant_and_not_perfect {n : ℕ} (hn : n ≠ 0) : n.Deficient ↔ ¬n.Abundant ∧ ¬n.Perfect

theorem Nat.perfect_iff_not_abundant_and_not_deficient {n : ℕ} (hn : 0 ≠ n) : n.Perfect ↔ ¬n.Abundant ∧ ¬n.Deficient

theorem Nat.abundant_iff_not_perfect_and_not_deficient {n : ℕ} (hn : 0 ≠ n) : n.Abundant ↔ ¬n.Perfect ∧ ¬n.Deficient

theorem Nat.deficient_or_perfect_or_abundant {n : ℕ} (hn : 0 ≠ n) : n.Deficient ∨ n.Abundant ∨ n.Perfect

A positive natural number is either deficient, perfect, or abundant

theorem Nat.Perfect.pseudoperfect {n : ℕ} (h : n.Perfect) : n.Pseudoperfect

theorem Nat.Prime.not_abundant {n : ℕ} (h : Prime n) : ¬n.Abundant

theorem Nat.Prime.not_weird {n : ℕ} (h : Prime n) : ¬n.Weird

theorem Nat.Prime.not_pseudoperfect {p : ℕ} (h : Prime p) : ¬p.Pseudoperfect

theorem Nat.Prime.not_perfect {p : ℕ} (h : Prime p) : ¬p.Perfect

theorem Nat.Prime.deficient_pow {n m : ℕ} (h : Prime n) : (n ^ m).Deficient

Any natural number power of a prime is deficient

theorem IsPrimePow.deficient {n : ℕ} (h : IsPrimePow n) : n.Deficient

theorem Nat.Prime.deficient {n : ℕ} (h : Prime n) : n.Deficient

theorem Nat.infinite_deficient : {n : ℕ | n.Deficient}.Infinite

There exists infinitely many deficient numbers

theorem Nat.infinite_even_deficient : {n : ℕ | Even n ∧ n.Deficient}.Infinite

theorem Nat.infinite_odd_deficient : {n : ℕ | Odd n ∧ n.Deficient}.Infinite