lean_workbook_plus_38702

Proved

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

Show that $\alpha|x| + (1 - \alpha)|y|\geq |\alpha x + (1 - \alpha)y|$ for all $\alpha\in(0,1)$ and all real numbers $x,y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38702 (α : ℝ) (x y : ℝ) (hα : 0 < α ∧ α < 1) :
  α * |x| + (1 - α) * |y| ≥ |α * x + (1 - α) * y|   :=  by sorry

Source