lean_workbook_plus_13248

Proved

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

Let $A_0, A_1,$ and $A_2$ be real numbers such that $-1\le A_0 + A_1x + A_2 x^2 \le 2$ holds for all real numbers $x$ that satisfies $-1\le x \le 1$ . Prove that $-3\le A_2 \le 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13248 (A0 A1 A2 : ℝ) (hA : ∀ x : ℝ, -1 ≤ x ∧ x ≤ 1 → -1 ≤ A0 + A1 * x + A2 * x ^ 2 ∧ A0 + A1 * x + A2 * x ^ 2 ≤ 2) : -3 ≤ A2 ∧ A2 ≤ 3   :=  by sorry

Source

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

View graph