Prove2Me

lean_workbook_plus_50698

Proved

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

Prove that (ax+by)2+(cx+dy)2≤(a2+b2+c2+d2)(x2+y2)(ax+by)^2+(cx+dy)^2\leq(a^2+b^2+c^2+d^2)(x^2+y^2).

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

View graph