A quadratic lower bound with an attained equality case

Proved

WorkbookCorrected.base_54977

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

corrected-formalizationlean-workbooksource-checked

Let $x,y,z$ be real numbers satisfying $x+yz=1$ . Then

2x^2+3y^2+4z^2\ge 2.

Equality holds at $x=1,y=z=0$ , so the lower bound is attained.

Formalization Note: This statement includes both the universal inequality and the equality point explicitly stated in the source. The original formalization contained only the inequality.

Source: InternLM Lean-Workbook, record lean_workbook_54977 (Apache-2.0).

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.base_54977 : (∀ (x y z : ℝ) (h : x + y*z = 1), 2*x^2 + 3*y^2 + 4*z^2 ≥ 2) ∧ ((1 : ℝ) + 0*0 = 1 ∧ 2*(1 : ℝ)^2 + 3*0^2 + 4*0^2 = 2) := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_54977; Apache-2.0

View graph