lean_workbook_plus_60592

Proved

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

My Official ProofBy Cauchy, $\sum\frac{p^4+2q^2r^2}{p^6+q^4+r^4}\leq\sum\frac{p^4+q^4+r^4}{p^6+q^4+r^4}=(p^4+q^4+r^4)\sum\frac{1}{p^6+q^4+r^4}=(p^4+q^4+r^4)\sum\frac{p^2+r^4+r^4}{(p^4+q^4+r^4)^2}=\frac{\sum p^2+2\sum r^4}{p^4+q^4+r^4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60592  (p q r : ℝ) :
  (p^4 + 2 * q^2 * r^2) / (p^6 + q^4 + r^4) ≤ (p^4 + q^4 + r^4) / (p^6 + q^4 + r^4)   :=  by sorry

Source

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

View graph