Prove2Me

lean_workbook_plus_16042

Proved

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

Using Cauchy Schwarz inequality we observe: \n\n 1a2+bc=b(a2+bc)(b+c)+c(a2+bc)(b+c)≤b(ab+cb)2+c(ac+bc)2=1(a+b)2+1(a+c)2\frac{1}{a^2+bc}=\frac{b}{(a^2+bc)(b+c)}+\frac{c}{(a^2+bc)(b+c)} \le \frac{b}{(a\sqrt{b}+c\sqrt{b})^2} + \frac{c}{(a\sqrt{c}+b\sqrt{c})^2}=\frac{1}{(a+b)^2}+\frac{1}{(a+c)^2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16042  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
  1 / (a^2 + b * c) ≤ 1 / (a + b)^2 + 1 / (a + c)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph