lean_workbook_plus_55874

Proved

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

The inequality between the arithmetic mean and the quadratic mean gives $\frac{x+y+z}{3}\leq\sqrt{\frac{x^{2}+y^{2}+z^{2}}{3}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55874 (x y z : ℝ) :
  (x + y + z) / 3 ≤ Real.sqrt ((x ^ 2 + y ^ 2 + z ^ 2) / 3)   :=  by sorry

Source