lean_workbook_plus_9027

Proved

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

If $f(-1)=p,f(0)=q,f(1)=r$ then $a={{p+r-2q}\over 2},b={{r-p}\over 2},c=q$ and $6|a|+|b|+9|c|=3|p+r-2q|+{1\over 2}|p-r|+9|q|=:\alpha$ where $p,q,r\in [-1,1]$ . Note that we may assume $q\ge {{p+r}\over 2}$ , replacing $f$ by $-f$ if necessary and also that $p\le r$ , replacing $f(x)$ by $f(-x)$ , if necessary. Hence $p\le r, {{p+r}\over 2}\le q$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9027  (p q r a b c α : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x ∈ Set.Icc (-1) 1)
  (h₁ : f (-1) = p)
  (h₂ : f 0 = q)
  (h₃ : f 1 = r)
  (h₄ : a = (p + r - 2 * q) / 2)
  (h₅ : b = (r - p) / 2)
  (h₆ : c = q)
  (h₇ : 6 * abs a + abs b + 9 * abs c = α) :
  3 * abs (p + r - 2 * q) + 1 / 2 * abs (r - p) + 9 * abs q = α   :=  by sorry

Source

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

View graph