A weighted squared-norm bound at fixed pairwise sum

Proved

WorkbookSource.base_39267

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that: $3x^{2}+3y^{2}+z^{2}\geq 10$ where $x;y;z$ are real numbers satisfying $xy+yz+xz=5$

Source: InternLM Lean-Workbook, record lean_workbook_39267 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_39267 (x y z : ℝ) (h : x * y + y * z + z * x = 5) :
  3 * x ^ 2 + 3 * y ^ 2 + z ^ 2 ≥ 10  :=  by sorry

Source