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