lean_workbook_plus_68135

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Use $AM \ge HM$ to derive the inequality: $\frac{x}{y} + \frac{x}{z} \ge \frac{4x}{y+z}$ , $\frac{y}{z} + \frac{y}{x} \ge \frac{4y}{z+x}$ , $\frac{z}{x} + \frac{z}{y} \ge \frac{4z}{x+y}$ for $x,y,z>1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68135 (x y z : ℝ) (hx : x > 1) (hy : y > 1) (hz : z > 1) : (x / y + x / z) ≥ 4 * x / (y + z) ∧ (y / z + y / x) ≥ 4 * y / (z + x) ∧ (z / x + z / y) ≥ 4 * z / (x + y)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph