lean_workbook_plus_5420

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $a,b>0.$ Prove that

\frac{a^5+2b^5}{a^2+2b^2}+\frac{a^4+2b^4}{a+2b}\geq \frac{2}{3}(a^3+2b^3)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5420 (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : (a^5 + 2 * b^5) / (a^2 + 2 * b^2) + (a^4 + 2 * b^4) / (a + 2 * b) ≥ 2 / 3 * (a^3 + 2 * b^3)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph