A rational product inequality under a triple-product constraint

Proved

WorkbookSource.base_3161

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

lean-workbooksource-checked

In case $abc<1,$ setting $a=\frac{1}{x},$ $b=\frac{1}{y}$ and $c=\frac{1}{z},$ then we have $xyz>1$ and the inequality becomes

${\left(\frac{1}{x}+\frac{1}{y}+\frac{1}{z}+\frac{1}{xyz}-4\right)\left(\frac{1}{xy}+\frac{1}{yz}+\frac{1}{zx}-3\right) \ge 4\left(\frac{1}{xyz}-1\right)\left(\frac{1}{x}+\frac{1}{y}+\frac{1}{z}-3\right),}$

Source: InternLM Lean-Workbook, record lean_workbook_3161 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_3161 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (h : x * y * z > 1) : (1 / x + 1 / y + 1 / z + 1 / (x * y * z) - 4) * (1 / (x * y) + 1 / (y * z) + 1 / (z * x) - 3) ≥ 4 * (1 / (x * y * z) - 1) * (1 / x + 1 / y + 1 / z - 3)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_3161; Apache-2.0

View graph