Convergence under a preceding-sum bound
ProvedWorkbookCorrected.plus_34093corrected-formalizationlean-workbooksequencessource-checked
Let x₁,x₂,… be positive real numbers satisfying xₙ₊₁ ≤ (x₁+⋯+xₙ)/n² for every integer n ≥ 1. Then xₙ converges to zero.
Formalization Note: Restores the source’s positive indexing and its sum of exactly the first n terms, with denominator n².
Source: InternLM Lean-Workbook, record lean_workbook_plus_34093 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_34093 (x : ℕ → ℝ) (hx : ∀ n : ℕ, 1 ≤ n → 0 < x n)
(h : ∀ n : ℕ, 1 ≤ n → x (n+1) ≤ (∑ i ∈ Finset.range n, x (i+1))/(n:ℝ)^2) :
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |x n| < ε := by sorrySource