Documentation

Mathlib.NumberTheory.FactorisationProperties

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 : ℕ) :

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

Equations

n.Abundant = (n < ∑ i ∈ n.properDivisors, i)

Instances For

instance Nat.instDecidableAbundant (n : ℕ) :

Decidable n.Abundant

Equations

n.instDecidableAbundant = n.decLt (∑ i ∈ n.properDivisors, i)

def Nat.Deficient (n : ℕ) :

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

Equations

n.Deficient = (∑ i ∈ n.properDivisors, i < n)

Instances For

instance Nat.instDecidableDeficient (n : ℕ) :

Decidable n.Deficient

Equations

n.instDecidableDeficient = (∑ i ∈ n.properDivisors, i).decLt n

def Nat.Pseudoperfect (n : ℕ) :

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.

Equations

n.Pseudoperfect = (0 < n ∧ ∃ s ⊆ n.properDivisors, ∑ i ∈ s, i = n)

Instances For

instance Nat.instDecidablePseudoperfect (n : ℕ) :

Decidable n.Pseudoperfect

Equations

n.instDecidablePseudoperfect = instDecidableAnd

def Nat.Weird (n : ℕ) :

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

Equations

n.Weird = (n.Abundant ∧ ¬n.Pseudoperfect)

Instances For

instance Nat.instDecidableWeird (n : ℕ) :

Decidable n.Weird

Equations

n.instDecidableWeird = instDecidableAnd

def Nat.abundancyIndex (n : ℕ) :

abundancyIndex n is the sum of the divisors of n divided by n.

Equations

n.abundancyIndex = ↑(∑ i ∈ n.divisors, i) / ↑n

Instances For

theorem Nat.not_pseudoperfect_iff_forall {n : ℕ} :

¬n.Pseudoperfect ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

theorem Nat.deficient_one :

theorem Nat.deficient_two :

theorem Nat.deficient_three :

theorem Nat.not_abundant_zero :

theorem Nat.abundant_twelve :

theorem Nat.weird_seventy :

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) :

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

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

¬p.Pseudoperfect

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

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) :

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

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

theorem Nat.abundant_iff_sum_divisors {n : ℕ} :

n.Abundant ↔ 2 * n < ∑ i ∈ n.divisors, i

theorem Nat.abundant_iff_two_lt_abundancyIndex {n : ℕ} :

n.Abundant ↔ 2 < n.abundancyIndex

theorem Nat.abundancyIndex_le_of_dvd {n m : ℕ} (hn : n ≠ 0) (hd : m ∣ n) :

m.abundancyIndex ≤ n.abundancyIndex

theorem Nat.Abundant.of_dvd {n m : ℕ} (h : m.Abundant) (hd : m ∣ n) (hn : n ≠ 0) :

theorem Nat.Abundant.mul_left {n m : ℕ} (h : n.Abundant) (hm : m ≠ 0) :

(m * n).Abundant

theorem Nat.infinite_even_abundant :

{n : ℕ | Even n ∧ n.Abundant}.Infinite

theorem Nat.infinite_odd_abundant :

{n : ℕ | Odd n ∧ n.Abundant}.Infinite