An asymmetric weighted pair-product ratio inequality

Proved

WorkbookSource.plus_51739

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

lean-workbooksource-checked

Let $x,y,z>0,$ prove that: $\frac{2yz}{x^2}+\frac{2xz}{y^2}+\frac{5xy}{z^2}\geq \frac{3x}{z}+\frac{3y}{z}+3.$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_51739 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : 2 * y * z / x ^ 2 + 2 * x * z / y ^ 2 + 5 * x * y / z ^ 2 ≥ 3 * x / z + 3 * y / z + 3   :=  by sorry

Source

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

View graph