lean_workbook_plus_2941

Proved

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

Since, $\frac{x^{2}y + x^{2}z + z^{2}y + y^{2}z}{4} \geq \sqrt[4]{x^{2}y.x^{2}z.z^{2}y.y^{2}z} = xyz$ . So, $(x^{2}+yz)(y+z) \geq 4xyz$ , which reduces to give $\frac{4}{x^{2}+yz} \leq \frac{1}{xy} + \frac{1}{xz}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2941  (x y z : ℝ)
  (h₀ : 0 < x ∧ 0 < y ∧ 0 < z) :
  4 / (x^2 + y * z) ≤ 1 / (x * y) + 1 / (x * z)   :=  by sorry

Source

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

View graph