lean_workbook_plus_67047

Proved

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

Prove that $(a_{1}^2+a_{2}^2+a_{3}^2)(b_{1}^2+b_{2}^2+b_{3}^2) \geq a_{1}^2b_{1}^2+a_{2}^2b_{2}^2+a_{3}^2b_{3}^2+2a_{1}b_{2}a_{2}b_{1}+2a_{1}b_{3}a_{3}b_{1}+2a_{2}b_{3}a_{3}b_{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph