lean_workbook_plus_34501

Proved

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

Using the inequality $\frac{a}{a^{2}+bc}\leq \frac{1}{4}(\frac{1}{b}+\frac{1}{c})$ , prove the given inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34501 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → a / (a ^ 2 + b * c) ≤ (1 / 4) * (1 / b + 1 / c)   :=  by sorry

Source