A weighted norm lower bound under a linear constraint

Proved

WorkbookSource.plus_63009

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

lean-workbooksource-checked

Let $a,b,c$ be real numbers such that $2a+b+3c=20$ . $a^2+4b^2+c^2\geq\frac{1600}{53}$ .

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_63009 (a b c : ℝ) (h : 2*a + b + 3*c = 20) : a^2 + 4*b^2 + c^2 ≥ 1600/53   :=  by sorry

Source