Peeling

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

proven

Natural Language Statement

Theorem

Let $P_d(s)$ be the product of $1 - s/i$ over $i = 1, \ldots, d$ . It is $1$ at $s = 0$ . At a natural number $s \ge 1$ it is $(-1)^d$ times the binomial coefficient of $s - 1$ and $d$ , so it vanishes for $1 \le s \le d$ . Take numbers $g(s)$ and weights $\omega(s)$ for $s = 0, \ldots, N$ , with $\omega(0) = 1$ , and put $S = \sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ . Then $S - g(0)$ is $(-1)^d$ times the sum of $g(s)\,\omega(s)\binom{s-1}{d}$ over $1 \le s \le N$ . So $S$ keeps $g(0)$ , drops the next $d$ terms, and leaves a remainder that is small when the later terms are small. This is called peeling. It has three consequences.

If all $g(s)$ and $\omega(s)$ are nonnegative, then $(-1)^d (S - g(0)) \ge 0$ .
Let $0 \le y < 1$ and $M \left(\frac{y}{1 - y}\right)^{d+1} < 1$ . If $g(s)\,\omega(s) \le M y^s$ for $1 \le s \le N$ , then $(-1)^d (S - g(0)) < 1$ . This needs no sign condition on $g$ and $\omega$ .
Let $g$ and $g'$ be sequences of natural numbers that both satisfy this bound, with nonnegative weights. If they give the same $S$ , then $g(0) = g'(0)$ .

Concept map

100%

Preparing this local graph with the browser’s fonts…

Proven claimThis concept

Evidence

This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

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.Group.Finset.Defs
7	import Mathlib.Data.Rat.Defs
8	import Mathlib.Order.Interval.Finset.Nat
9
10	/-!
11	---
12	title: Peeling
13	type: theorem
14	---
15	Let $P_d(s)$ be the product of $1 - s/i$ over $i = 1, \ldots, d$ . It is $1$ at $s = 0$ . At a natural
16	number $s \ge 1$ it is $(-1)^d$ times the binomial coefficient of $s - 1$ and $d$ , so it vanishes
17	for $1 \le s \le d$ . Take numbers $g(s)$ and weights $\omega(s)$ for $s = 0, \ldots, N$ , with
18	$\omega(0) = 1$ , and put $S = \sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ . Then $S - g(0)$ is $(-1)^d$
19	times the sum of $g(s)\,\omega(s)\binom{s-1}{d}$ over $1 \le s \le N$ . So $S$ keeps $g(0)$ , drops
20	the next $d$ terms, and leaves a remainder that is small when the later terms are small. This is
21	called peeling. It has three consequences.
22
23	1. If all $g(s)$ and $\omega(s)$ are nonnegative, then $(-1)^d (S - g(0)) \ge 0$ .
24	2. Let $0 \le y < 1$ and $M \left(\frac{y}{1 - y}\right)^{d+1} < 1$ . If
25	$g(s)\,\omega(s) \le M y^s$ for $1 \le s \le N$ , then $(-1)^d (S - g(0)) < 1$ . This needs no
26	sign condition on $g$ and $\omega$ .
27	3. Let $g$ and $g'$ be sequences of natural numbers that both satisfy this bound, with nonnegative
28	weights. If they give the same $S$ , then $g(0) = g'(0)$ .
29	-/
30
31	namespace Lax100001.Peel
32
33	/-- The polynomial $P_d(s) = \prod_{i=1}^{d} (1 - s/i)$ of degree $d$ in $s$ . The index $i + 1$ lets
34	the product range over $\texttt{Finset.range d}$ . For example $P_2(s) = (1 - s)(1 - s/2)$ , which
35	takes the values $1, 0, 0, 1, 3, 6$ at $s = 0, \ldots, 5$ . -/
36	def P (d : ℕ) (s : ℚ) : ℚ := ∏ i ∈ Finset.range d, (1 - s / (i + 1))
37
38	/-- For nonnegative $g$ and $\omega$ with $\omega(0) = 1$ , the weighted sum
39	$\sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ differs from $g(0)$ by $(-1)^d$ times a nonnegative number.
40	So it is at least $g(0)$ if $d$ is even, and at most $g(0)$ if $d$ is odd. -/
41	axiom sign_nonneg (d N : ℕ) (g ω : ℕ → ℚ) (hg : ∀ s ≤ N, 0 ≤ g s) (hω : ∀ s ≤ N, 0 ≤ ω s)
42	(hω₀ : ω 0 = 1) :
43	0 ≤ (-1) ^ d * (∑ s ∈ Finset.range (N + 1), g s * ω s * P d s - g 0)
44
45	/-- Let $0 \le y < 1$ and $M \left(\frac{y}{1 - y}\right)^{d+1} < 1$ . If $g(s)\,\omega(s) \le M y^s$
46	for $1 \le s \le N$ , and $\omega(0) = 1$ , then the weighted sum
47	$\sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ differs from $g(0)$ by $(-1)^d$ times a number that is less
48	than $1$ . No sign condition on $g$ and $\omega$ is needed. -/
49	axiom lt_one (d N : ℕ) (y M : ℚ) (g ω : ℕ → ℚ) (hω₀ : ω 0 = 1) (hy : 0 ≤ y) (hy₁ : y < 1)
50	(hM : M * (y / (1 - y)) ^ (d + 1) < 1) (hgω : ∀ s ∈ Finset.Icc 1 N, g s * ω s ≤ M * y ^ s) :
51	(-1) ^ d * (∑ s ∈ Finset.range (N + 1), g s * ω s * P d s - g 0) < 1
52
53	/-- Two sequences $g$ and $g'$ of natural numbers that satisfy the bounds of $\texttt{lt\_one}$ ,
54	with nonnegative weights $\omega$ , and have the same weighted sum
55	$\sum_{s=0}^{N} g(s)\,\omega(s)\,P_d(s)$ , have the same first entry. -/
56	axiom head_eq (d N : ℕ) (y M : ℚ) (g g' : ℕ → ℕ) (ω : ℕ → ℚ) (hω : ∀ s ≤ N, 0 ≤ ω s)
57	(hω₀ : ω 0 = 1) (hy : 0 ≤ y) (hy₁ : y < 1) (hM : M * (y / (1 - y)) ^ (d + 1) < 1)
58	(hg : ∀ s ∈ Finset.Icc 1 N, g s * ω s ≤ M * y ^ s)
59	(hg' : ∀ s ∈ Finset.Icc 1 N, g' s * ω s ≤ M * y ^ s)
60	(hS : ∑ s ∈ Finset.range (N + 1), g s * ω s * P d s =
61	∑ s ∈ Finset.range (N + 1), g' s * ω s * P d s) :
62	g 0 = g' 0
63
64	end Lax100001.Peel
65

Builds on

none

Used by

none

From Mathlib

Peeling

Natural Language Statement

Theorem

1 head_eq proven

2 lt_one proven

3 sign_nonneg proven

In the paper

Lean source

1 `head_eq` proven

2 `lt_one` proven

3 `sign_nonneg` proven