lean_workbook_plus_11910

Proved

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

Prove that for $x, y, z > 0$ with $xyz = 1$ , $x^2 + y^2 + z^2 \geq \frac{1}{x} + \frac{1}{y} + \frac{1}{z}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11910 (x y z : ℝ) (hx : x > 0 ∧ y > 0 ∧ z > 0 ∧ x*y*z = 1) : x^2 + y^2 + z^2 >= 1/x + 1/y + 1/z   :=  by sorry

Source