Vibe Proof

Proof of Peeling (2nd statement)

groundedproofs/Lax100001Proofs/Results.lean · lax-100001

What this proof establishes

no assumptions

thm✓Lax100001.Peel (2nd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

In the paper

  • page 6 of this submission's paper

Description

The remainder (−1)d(S−g(0))(-1)^d (S - g(0)) is at most MM times a tail sum of the binomial series, which Lax100001.Tail.tail_le\texttt{Lax100001.Tail.tail\_le} bounds by (y1−y)d+1\left(\frac{y}{1 - y}\right)^{d+1}.