lean_workbook_plus_6128

Proved

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

Let $a, b, c, d$ are positive real numbers such that $a+b\geq \frac{1}{3}(c+d)$ and $a^2+b^2=\frac{1}{3}(c^2+d^2).$ Prove that\n\n

a^4+a^2b^2+b^4\leq \frac{4}{27}(c^4+c^2d^2+d^4)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6128 (a b c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) (hab : a + b ≥ 1 / 3 * (c + d)) (h : a^2 + b^2 = 1 / 3 * (c^2 + d^2)) : a^4 + a^2 * b^2 + b^4 ≤ 4 / 27 * (c^4 + c^2 * d^2 + d^4)   :=  by sorry

Source

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

View graph