lean_workbook_plus_16352

Proved

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

Using C-S, $(\frac{x^2}{y^2}+\frac{y^2}{z^2}+\frac{z^2}{x^2})(1+1+1) \geq (\frac{x}{y}+\frac{y}{z}+\frac{z}{x})^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16352 (x y z : ℝ) : (x^2 / y^2 + y^2 / z^2 + z^2 / x^2) * (1 + 1 + 1) ≥ (x / y + y / z + z / x)^2   :=  by sorry

Source