lean_workbook_plus_69201

Proved

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

Prove that $(a_1^2 + a_2^2)(b_1^2 + b_2^2) \geq (a_1b_1 + a_2b_2)^2$ using Cauchy-Schwarz inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69201 (a₁ a₂ b₁ b₂ : ℝ) :
  (a₁^2 + a₂^2) * (b₁^2 + b₂^2) ≥ (a₁ * b₁ + a₂ * b₂)^2   :=  by sorry

Source