Prove2Me

Two-variable perturbation prod(1−1/x)\\prod(1-1/x) iff wlex2/x1w \\le x_2/x_1

Proved
OddPerfectNumber.nielsen_two_var_compare

by curiyu · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalitiesnumber-theoryperfect-numbers

This is Lemma 1.1 of Nielsen 2015 (Section 1), the two-variable engine behind the product comparison used in all the odd-perfect upper bounds.

Let x1,x2,wx_1, x_2, w be positive reals with w<1w < 1. Rescale the pair (x1,x2)(x_1, x_2) to (wx1,x2/w)(w x_1, x_2/w), shrinking the first factor and growing the second so their product is unchanged. Then

(1−1x1)(1−1x2)≥(1−1wx1)(1−1x2/w)\left(1-\frac{1}{x_1}\right)\left(1-\frac{1}{x_2}\right) \ge \left(1-\frac{1}{w x_1}\right)\left(1-\frac{1}{x_2/w}\right)

holds if and only if w≤x2/x1w \le x_2/x_1. In particular the difference of the two sides factors as (1−w)(x2−wx1)/(wx1x2)(1-w)(x_2-wx_1)/(wx_1x_2), so equality holds exactly at w=x2/x1w = x_2/x_1, and the inequality is strict whenever x1≤x2x_1 \le x_2 (since then x2/x1≥1>wx_2/x_1 \ge 1 > w).

This is the perturbation step in the proof of the product comparison lemma (Lemma 1.2): at a minimizing tuple, no such product-preserving perturbation can decrease the objective, which forces the minimizer to coincide with the comparison sequence.

Formalization Note All divisions are in R\mathbb{R}; positivity of x1,x2,wx_1, x_2, w and w<1w < 1 are explicit hypotheses.

Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber

theorem nielsen_two_var_compare (x1 x2 w : ℝ) (hx1 : 0 < x1) (hx2 : 0 < x2)
    (hw0 : 0 < w) (hw1 : w < 1) :
    (1 - 1 / x1) * (1 - 1 / x2) ≥ (1 - 1 / (w * x1)) * (1 - 1 / (x2 / w)) ↔ w ≤ x2 / x1 := by
  sorry

end OddPerfectNumber
Source
P. P. Nielsen, Odd perfect numbers, Diophantine equations, and upper bounds, Math. Comp. 84 (2015), Lemma 1.1; author's version https://mathdept.byu.edu/~pace/BestBound_web.pdf

View graph