A sum of quadratic ratios bounds a shifted triple sum

Proved

WorkbookSource.base_22268

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let $x,y,z,k > 0$ . Prove that $\frac {x^2 + y^2}{z + k} + \frac {y^2 + z^2}{x + k} + \frac {z^2 + x^2}{y + k} \geq \frac {3}{2} (x + y + z - k).$

Source: InternLM Lean-Workbook, record lean_workbook_22268 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_22268 (x y z k : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (hk : 0 < k) : (x^2 + y^2)/(z + k) + (y^2 + z^2)/(x + k) + (z^2 + x^2)/(y + k) ≥ 3/2 * (x + y + z - k)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_22268; Apache-2.0

View graph