Global sigma cross bound

Proved

OddPerfectNumber.sigma_cross_bound

by WillR · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

abundancyodd-perfectsigmasupport

For every natural number n greater than one, the product of q minus one over the prime support times sigma(n) is strictly less than the product of q over the prime support times n.

Preamble

import Mathlib

Formal statement

theorem OddPerfectNumber.sigma_cross_bound (n : Nat) (hn : 1 < n) :
    (∏ q ∈ n.primeFactors, (q - 1)) * ArithmeticFunction.sigma 1 n <
      (∏ q ∈ n.primeFactors, q) * n := by sorry

View graph