Prove2Me

Lean-Workbook Syntax 69836: A nonpositive sum under interval bounds

Proved
WorkbookSyntax.plus_69836

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

lean-workbookrepaired-notationsource-checked

If 0≤xi≤a0\le x_i\le a for 0≤i<n0\le i<n, then ∑i=0n−1xi(xi−a)≤0\sum_{i=0}^{n-1}x_i(x_i-a)\le0.

Source: Lean-Workbook row lean_workbook_plus_69836 (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.Analysis.Complex.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
Formal statement
theorem WorkbookSyntax.plus_69836 (n : ℕ) (a : ℝ) (x : ℕ → ℝ) (h₁ : ∀ i ∈ Finset.range n, 0 ≤ x i) (h₂ : ∀ i ∈ Finset.range n, x i ≤ a) : ∑ i ∈ Finset.range n, x i * (x i - a) ≤ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_69836; immutable original Prove2Me node d568f50d-9c56-4740-8ce0-0f9a9f590582

View graph