lean_workbook_plus_28701
DisprovedHölder's inequality gives , with equality for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28701 : ∀ a b : ℝ, (a^3+b^3)*(1+1)*(1+1) ≥ (a+b)^3 := by sorry
Source
Hölder's inequality gives , with equality for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_28701 : ∀ a b : ℝ, (a^3+b^3)*(1+1)*(1+1) ≥ (a+b)^3 := by sorry