lean_workbook_plus_2804
ProvedCase 2. . We now cannot set , as . We need to set and to get as large as possible. This gives , which has maximum at , ( ) so in this case.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2804 (x y z : ℝ) (h₀ : 2 ≤ x ∧ x ≤ 3) (h₁ : y = 4 - x) (h₂ : z = -1) : x^2 + y^2 + z^2 ≤ 11 := by sorry
Source