lean_workbook_plus_71703

Proved

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

$\sqrt{\frac{y^{2}+z^{2}}{x^{2}}}\leq \frac{{1+\frac{y^{2}+z^{2}}{x^{2}}}}{2}=\frac{x^{2}+y^{2}+z^{2}}{2x^{2}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71703 (x y z : ℝ) (hx : x ≠ 0) : Real.sqrt ((y ^ 2 + z ^ 2) / x ^ 2) ≤ (1 + (y ^ 2 + z ^ 2) / x ^ 2) / 2   :=  by sorry

Source