A reciprocal form of the three-variable quadratic mean bound
ProvedWorkbookSource.problem_6963lean-workbooksource-checked
prove that $ \frac {(a + b + c)}{S + \frac {1}{9}(a + b + c)^2}\le\frac {9}{4(a + b + c)} $, where $ S = a^2 + b^2 + c^2 $
Source: InternLM Lean-Workbook, record lean_workbook_6963 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_6963 (a b c : ℝ) (h : a > 0 ∧ b > 0 ∧ c > 0) : (a + b + c) / (a ^ 2 + b ^ 2 + c ^ 2 + (1 / 9) * (a + b + c) ^ 2) ≤ 9 / (4 * (a + b + c)) := by sorry
Source