lean_workbook_plus_11756

Proved

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

Prove the inequality: $2\sqrt{1+2(x-3)^2}\sqrt{(x-2)^2+1}\geq -3x^2+16x-\frac{87}{4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11756 : ∀ x : ℝ, 2 * Real.sqrt (1 + 2 * (x - 3) ^ 2) * Real.sqrt ((x - 2) ^ 2 + 1) ≥ -3 * x ^ 2 + 16 * x - 87 / 4   :=  by sorry

Source

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

View graph