Prove2Me

Lean-Workbook Syntax 74095: A nonnegative finite sum of shifted squares

Proved
WorkbookSyntax.plus_74095

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

For real numbers a0,…,an−1a_0,\ldots,a_{n-1}, 4∑i=0n−1(ai−1/2)2≥04\sum_{i=0}^{n-1}(a_i-1/2)^2\ge0.

Source: Lean-Workbook row lean_workbook_plus_74095 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Data.Real.Basic
Formal statement
theorem WorkbookSyntax.plus_74095 (n : ℕ) (a : ℕ → ℝ) : 4 * ∑ i ∈ Finset.range n, (a i - 1 / 2)^2 ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_74095; immutable original Prove2Me node 423d2167-b7c3-4de8-8b37-2f6ef07a4148

View graph