lean_workbook_plus_35006
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35006 (a b : ℝ) : a^2 * (1 + b^4) ≤ (a^4 + 1) / 2 * (1 + b^4) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35006 (a b : ℝ) : a^2 * (1 + b^4) ≤ (a^4 + 1) / 2 * (1 + b^4) := by sorry