lean_workbook_plus_18747Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)Prove the final inequality using A.M.-G.M. inequality:\n (∑i=1ntixi+ab∑i=1ntixi)2≥4ab(∑i=1ntixi)(∑i=1ntixi)\Big( \sum_{i=1}^{n}{t_ix_i}+ab\sum_{i=1}^{n}{\frac{t_i}{x_i}}\Big)^2 \geq 4ab\left(\sum_{i=1}^{n}{t_i x_i}\right)\left(\sum_{i=1}^{n}{\frac{t_i}{x_i}}\right)(i=1∑ntixi+abi=1∑nxiti)2≥4ab(i=1∑ntixi)(i=1∑nxiti)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_18747 (n a b : ℕ) (t x : Fin n → ℝ) : (∑ i, t i * x i + a * b * ∑ i, t i / x i) ^ 2 ≥ 4 * a * b * (∑ i, t i * x i) * (∑ i, t i / x i) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph