A normalized squared total bounds pairwise quadratic ratios
ProvedWorkbookSource.base_14803lean-workbooksource-checked
Let be positive real numbers. Prove that \begin{align*} \frac{(x+y+z)^2}{x^2+y^2+z^2}\ge \sum \frac{2xy}{x^2+y^2} \end{align*} Please let me know what you think .
Source: InternLM Lean-Workbook, record lean_workbook_14803 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_14803 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x + y + z) ^ 2 / (x ^ 2 + y ^ 2 + z ^ 2) ≥ 2 * x * y / (x ^ 2 + y ^ 2) + 2 * y * z / (y ^ 2 + z ^ 2) + 2 * z * x / (z ^ 2 + x ^ 2) := by sorry
Source