Prove2Me

lean_workbook_plus_69216

Proved

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

Let a,ba,b are non-negative real numbers such that a2+b2=6.a^2+b^2=6 . Prove that \n\n

αa+βb≤6(α2+β2)\alpha a+\beta b\le\sqrt{6\left({\alpha}^2+{\beta}^2\right)}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69216 (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a^2 + b^2 = 6) (α β : ℝ) : α * a + β * b ≤ Real.sqrt (6 * (α^2 + β^2))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph