lean_workbook_plus_79616

Proved

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

Let $a+b=2u, \: ab=v^2.$ Then the inequality becomes $v^4(4u^2-2v^2-2) \geq 2u(v^2-1) \: \Longleftrightarrow \: 2v^4u^2+(1-v^2)u-v^6-v^4 \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79616 {u v a b : ℝ} (ha : a + b = 2 * u) (hb : a * b = v ^ 2) : v ^ 4 * (4 * u ^ 2 - 2 * v ^ 2 - 2) ≥ 2 * u * (v ^ 2 - 1) ↔ 2 * v ^ 4 * u ^ 2 + (1 - v ^ 2) * u - v ^ 6 - v ^ 4 ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph