Prove2Me

lean_workbook_plus_2795

Proved

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

Apply the C.B.S. - inequality : ∣ax+by+cz∣2≤(a2+b2+c2)(x2+y2+z2):\ |ax+by+cz|^2\le \left(a^2+b^2+c^2\right)\left(x^2+y^2+z^2\right) . You have the equality if and only if xa=yb=zc\frac xa=\frac yb=\frac zc . See about the C.B.S. - inequality.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2795 (a b c x y z : ℝ) : (a * x + b * y + c * z) ^ 2 ≤ (a ^ 2 + b ^ 2 + c ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph