lean_workbook_plus_30809

Proved

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

Prove the inequality: $2(x^{m+n} + y^{m+n}) \geq (x^m + y^m)(x^n + y^n)$ , given $x^m \geq y^m$ and $x^n \geq y^n$ . Do not use Muirhead's inequality or Hölder's inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30809 (x y : ℝ) (m n : ℕ) (hx : x ^ m ≥ y ^ m) (hn : x ^ n ≥ y ^ n) : 2 * (x ^ (m + n) + y ^ (m + n)) ≥ (x ^ m + y ^ m) * (x ^ n + y ^ n)   :=  by sorry

Source

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

View graph