lean_workbook_plus_35597

Proved

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

$\frac{1}{2y^2} + \frac{2}{z^2} \geq \frac{2}{yz}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35597 : ∀ y z : ℝ, (y * z ≠ 0 → 1 / (2 * y ^ 2) + 2 / z ^ 2 ≥ 2 / (y * z))   :=  by sorry

Source