lean_workbook_plus_1166
Proved2.nd case : \n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1166 (a : ℝ) (ha : 0 < a) : (a + 2) ^ 3 / (27 * a) ≥ 1 / 4 + (a + 2) * (2 * a + 1) / (12 * a) := by sorry
Source
2.nd case : \n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1166 (a : ℝ) (ha : 0 < a) : (a + 2) ^ 3 / (27 * a) ≥ 1 / 4 + (a + 2) * (2 * a + 1) / (12 * a) := by sorry