lean_workbook_plus_18507

Proved

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

By Cauchy-Schwarz inequality, we have: $\frac {9}{3a + 2b + c}\le \frac {2}{a + b} + \frac {1}{a + c}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18507 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → 9 / (3 * a + 2 * b + c) ≤ 2 / (a + b) + 1 / (a + c)   :=  by sorry

Source