A squared pairwise reciprocal upper bound
ProvedWorkbookSource.base_24579lean-workbooksource-checked
Prove or disprove the inequality: $\frac{9(a^{2}+b^{2}+c^{2})}{4(ab+bc+ca)^{2}}\geq \frac{1}{(a+b)^{2}}+\frac{1}{(b+c)^{2}}+\frac{1}{(c+a)^{2}}$ for positive numbers a, b, and c.
Source: InternLM Lean-Workbook, record lean_workbook_24579 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_24579 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (9 * (a ^ 2 + b ^ 2 + c ^ 2)) / (4 * (a * b + b * c + c * a) ^ 2) ≥ 1 / (a + b) ^ 2 + 1 / (b + c) ^ 2 + 1 / (c + a) ^ 2 := by sorry
Source