A shifted quadratic upper bound in three real variables

Proved

WorkbookSource.plus_75969

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

lean-workbooksource-checked

Let $a+b+c+\frac{1}{4} (a-c)^2+\frac{1}{2}(3-a^2-b^2-c^2 )\leqslant 3.$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_75969 (a b c : ℝ) : a + b + c + (1 / 4) * (a - c) ^ 2 + (1 / 2) * (3 - a ^ 2 - b ^ 2 - c ^ 2) ≤ 3   :=  by sorry

Source