lean_workbook_plus_79671
ProvedGiven the function , prove that it is concave on the interval .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79671 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (a b : ℝ) (hab : a + b = 1) : (a * x + b * y)^(1/3) ≤ a * x^(1/3) + b * y^(1/3) := by sorry
Source