A linear-form bound on a weighted ellipsoid

Proved

WorkbookSource.plus_6754

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

lean-workbooksource-checked

Prove that $(4x-3y-2z)^2 \le 12$ under the given condition $2x^2+3y^2+4z^2=1$ and $x,y,z\in \mathbb{R}$ .

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_6754 (x y z : ℝ) (h : 2*x^2 + 3*y^2 + 4*z^2 = 1) :
  (4*x - 3*y - 2*z)^2 ≤ 12   :=  by sorry

Source