lean_workbook_plus_73986
ProvedLet . Prove using calculus that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73986 : ∀ a b : ℝ, a > 0 ∧ b > 0 → 8 * (a ^ 4 + b ^ 4) ≥ (a + b) ^ 4 := by sorry
Source
Let . Prove using calculus that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_73986 : ∀ a b : ℝ, a > 0 ∧ b > 0 → 8 * (a ^ 4 + b ^ 4) ≥ (a + b) ^ 4 := by sorry