A strict partial-sum bound for a rational multiplier recurrence

Proved

WorkbookCorrected.plus_15359

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Let $\{a_n \}_{n=1}^{\infty}$ be a sequence such that $a_1=\frac 12$ and $a_n=\biggl( \frac{2n-3}{2n} \biggr) a_{n-1} \qquad \forall n \geq 2.$ Prove that for every positive integer $n,$ we have $\sum_{k=1}^n a_k <1.$

Formalization Note: The source starts at a1=1/2 and has a_n=(2n−3)/(2n)a_(n−1) for n≥2. This correction uses the equivalent forward recurrence a_(n+1)=(2n−1)/(2(n+1))a_n for n≥1, real arithmetic, and sums terms1 throughn. The original formalization shifted the initial value and sum without shifting the coefficient correctly.

Source: InternLM Lean-Workbook, record lean_workbook_plus_15359 (Apache-2.0).

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.plus_15359 (a : ℕ → ℝ) (h0 : a 1=1/2)
    (h : ∀ n : ℕ, 1≤n → a (n+1)=(2*(n:ℝ)-1)/(2*((n:ℝ)+1))*a n) :
    ∀ n : ℕ, 1≤n → ∑ k ∈ Finset.range n, a (k+1) < 1 := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_15359; Apache-2.0

View graph