Prove2Me

A quadratic bound for a sum of linear and pairwise terms

Proved
WorkbookSource.base_11517

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

lean-workbooksource-checked

By Cauchy-Shwarz Inequality, we have: (a+b+c+2(ab+bc+ca))2≤3((a+b+c)2+2(ab+bc+ca)2)≤9(a2+b2+c2+2(a2b2+b2c2+c2a2))(a+b+c+2(ab+bc+ca))^{2}\le 3((a+b+c)^{2}+2(ab+bc+ca)^{2}) \le 9(a^{2}+b^{2}+c^{2}+2(a^{2}b^{2}+b^{2}c^{2}+c^{2}a^{2}))

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_11517 {a b c : ℝ} : (a + b + c + 2 * (a * b + b * c + c * a)) ^ 2 ≤ 9 * (a ^ 2 + b ^ 2 + c ^ 2 + 2 * (a ^ 2 * b ^ 2 + b ^ 2 * c ^ 2 + c ^ 2 * a ^ 2))  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_11517; Apache-2.0

View graph