Prove2Me

Strict majorization inequality for ∏(1−1/xi)\prod (1-1/x_i) (Nielsen, Lemma 1.2)

Proved
OddPerfectNumber.prod_one_sub_inv_lt_of_prod_lt

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

inequalitiesnumber-theoryperfect-numbers

Strict form of the majorization inequality for products ∏(1−1/xi)\prod (1 - 1/x_i).

Let n≥1n \ge 1 and let x0,…,xn−1x_0,\dots,x_{n-1} and y0,…,yn−1y_0,\dots,y_{n-1} be real numbers greater than 11, with yy non-decreasing and

∏i<mxi  ≤  ∏i<myi(0≤m≤n).\prod_{i<m} x_i \;\le\; \prod_{i<m} y_i \qquad (0 \le m \le n).

If moreover the full products are separated, ∏i<nxi<∏i<nyi\prod_{i<n} x_i < \prod_{i<n} y_i, then the conclusion is strict:

∏i<n(1−1xi)  <  ∏i<n(1−1yi).\prod_{i<n}\Bigl(1-\frac{1}{x_i}\Bigr)\;<\;\prod_{i<n}\Bigl(1-\frac{1}{y_i}\Bigr).

This is the form in which Nielsen's Lemma 1.2 is used: the equality case of that lemma occurs only when the two sequences coincide, so a strict inequality between the total products forces a strict inequality between the two products of 1−1/xi1 - 1/x_i.

Formalization Note. Sequences are functions ℕ → ℝ; only their values on Finset.range n matter.

Preamble
import Mathlib
open Finset
Formal statement
namespace OddPerfectNumber

theorem prod_one_sub_inv_lt_of_prod_lt (n : ℕ) (x y : ℕ → ℝ) (hn : 0 < n)
    (hx : ∀ i < n, 1 < x i) (hy : ∀ i < n, 1 < y i)
    (hymono : ∀ i, i + 1 < n → y i ≤ y (i + 1))
    (hle : ∀ m ≤ n, ∏ i ∈ Finset.range m, x i ≤ ∏ i ∈ Finset.range m, y i)
    (hlt : ∏ i ∈ Finset.range n, x i < ∏ i ∈ Finset.range n, y i) :
    ∏ i ∈ Finset.range n, (1 - 1 / x i) < ∏ i ∈ Finset.range n, (1 - 1 / y i) := by
  sorry

end OddPerfectNumber
Source
P. P. Nielsen, Odd perfect numbers, Diophantine equations, and upper bounds, Math. Comp. 84 (2015), no. 295, 2549-2567; Section 1. Author's copy: https://mathdept.byu.edu/~pace/BestBound_web.pdf . Lemma 1.2 (inequality (4) together with its equality characterisation), p. 2.

View graph