Prove2Me

lean_workbook_plus_54037

Proved

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

Let a+b=s, ab=ta+b=s,\ ab=t with s, t>0s,\ t>0 and s2≥4ts^2\geq 4t , thus \n\n (x2+ab)2(a+b)2−4ab(x2+a2)(x2+b2)(x^2+ab)^2(a+b)^2-4ab(x^2+a^2)(x^2+b^2) \n\n =s2(x2+t2)2−4t{x4+(s2−2t)x2+4t2}=s^2(x^2+t^2)^2-4t\{x^4+(s^2-2t)x^2+4t^2\} \n\n =(s2−4t)x4−2t(s2−4t)x2+t2(s2−4t)=(s^2-4t)x^4-2t(s^2-4t)x^2+t^2(s^2-4t) \n\n =(s2−4t)(x2−t)2≥0.=(s^2-4t)(x^2-t)^2\geq 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54037  (a b s t x : ℝ)
  (h₀ : 0 < a ∧ 0 < b)
  (h₁ : a + b = s)
  (h₂ : a * b = t)
  (h₃ : s^2 ≥ 4 * t)
  : (x^2 + a * b)^2 * (a + b)^2 - 4 * a * b * (x^2 + a^2) * (x^2 + b^2) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph