lean_workbook_plus_28481

Proved

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

Let $a,b>0$ Prove that:\n $\frac{2ab}{a^{2}+4b^{2}}+\frac{b^{2}}{3a^{2}+2b^{2}}\leq \frac{3}{5}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph