A binomial tail bound

Lax100001.Tail · concepts/Lax100001/Tail.lean · lax-100001

proven

Natural Language Statement

Theorem

Let $x$ be a rational number with $0 \le x < 1$ . The sum of $x^{j+1}\binom{j}{d}$ over the numbers $j$ below any bound $N$ is at most $\left(\frac{x}{1 - x}\right)^{d+1}$ . The sum over all $j$ has exactly this value, so the bound does not depend on $N$ .

Concept map

100%

Preparing this local graph with the browser’s fonts…

Proven claimThis concept

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax100001.Tail

⊢Lax100001Proofs.tail_le

In the paper

page 5 of this submission's paper

Lean source

Show types on hover

1	/-
2	Copyright (c) 2026 Anonymous. All rights reserved.
3	Released under Apache 2.0 license as described in the file LICENSE.
4	Authors: ChatGPT (OpenAI), Claude (Anthropic)
5	-/
6	import Mathlib.Algebra.BigOperators.Ring.Finset
7	import Mathlib.Data.Nat.Choose.Basic
8	import Mathlib.Data.Rat.Cast.Order
9
10	/-!
11	---
12	title: A binomial tail bound
13	type: theorem
14	---
15	Let $x$ be a rational number with $0 \le x < 1$ . The sum of $x^{j+1}\binom{j}{d}$ over the
16	numbers $j$ below any bound $N$ is at most $\left(\frac{x}{1 - x}\right)^{d+1}$ . The sum over all
17	$j$ has exactly this value, so the bound does not depend on $N$ .
18	-/
19
20	namespace Lax100001.Tail
21
22	/-- A finite weighted sum of binomial coefficients is at most a geometric power. -/
23	axiom tail_le (x : ℚ) (hx : 0 ≤ x) (hx1 : x < 1) (d N : ℕ) :
24	(∑ j ∈ Finset.range N, x ^ (j + 1) * (j.choose d : ℚ)) ≤ (x / (1 - x)) ^ (d + 1)
25
26	end Lax100001.Tail
27

Builds on

none

Used by

none

From Mathlib