A quadratic inequality with one weighted pairwise product

Proved

WorkbookSource.base_15043

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

lean-workbooksource-checked

Prove that $3r_ar_b + r_br_c + r_cr_a\le\left(r_a + r_b + r_c\right)^2$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_15043 (r_a r_b r_c : ℝ) : 3 * r_a * r_b + r_b * r_c + r_c * r_a ≤ (r_a + r_b + r_c) ^ 2  :=  by sorry

Source