lean_workbook_plus_7570

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $x, y, z$ be reals satisfying $x^2 + y^2 + z^2 = 1.$ Prove that $1\leq x^2 + 2y^2 + 3z^2\leq 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7570 (x y z : ℝ) (h : x ^ 2 + y ^ 2 + z ^ 2 = 1) : 1 ≤ x ^ 2 + 2 * y ^ 2 + 3 * z ^ 2 ∧ x ^ 2 + 2 * y ^ 2 + 3 * z ^ 2 ≤ 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph