lean_workbook_plus_64014

Proved

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

Using the Cauchy-Schwarz inequality, we have $(x+y+z)^2\le (x^2+y^2+1)(1+1+z^2)$ inferred $\frac{1}{{x^2 + y^2 + 1}} \le \frac{2+z^2}{(x+y+z)^2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64014  (x y z : ℝ) :
  (x + y + z)^2 ≤ (x^2 + y^2 + 1) * (1 + 1 + z^2)   :=  by sorry

Source