LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n

Statement

Let $n \in N$ with $n \geq 1$ , let $u \geq 0$ , let $δ_{0}, \dots, δ_{n - 1} \in R$ satisfy $∣ δ_{i} ∣ \leq u$ for every $i < n$ , and suppose $n u < 1$ . Then

$\prod_{i < n} (1 + δ_{i}) = 1 + θ_{n} with ∣ θ_{n} ∣ \leq γ_{n} : = \frac{n u}{1 - n u} .$

Facts & Assumptions

Given: A natural number $n \geq 1$ , a real $u \geq 0$ with $n u < 1$ , and reals $δ_{0}, \dots, δ_{n - 1}$ with $∣ δ_{i} ∣ \leq u$ ; write $γ_{n} : = n u / (1 - n u)$ .

[L1]

The hypothesis $n u < 1$ gives $u < 1$ , hence $1 - u > 0$ and $1 + u > 0$ ; the unit roundoff vocabulary comes from The standard relative floating-point model and unit roundoff.

[L2]

Binomial expansion over the reals: $(1 + t)^{n} = \sum_{k \leq n} (\binom{n}{k}) t^{k}$ (The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ ), and the binomial coefficient satisfies $(\binom{n}{k}) \leq n^{k}$ for every $k \leq n$ .

[L3]

Geometric series: for a real $r$ with $0 \leq r < 1$ , $\sum_{k = 0}^{\infty} r^{k} = 1 / (1 - r)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

Proof

technique · direct

1.1L1algebra

Since $∣ δ_{i} ∣ \leq u$ , each factor satisfies $1 - u \leq 1 + δ_{i} \leq 1 + u$ , and the factors $1 \pm u$ are nonnegative by [L1]; multiplying the inequalities across $i < n$ gives $(1 - u)^{n} \leq \prod_{i < n} (1 + δ_{i}) \leq (1 + u)^{n}$ .

1.2L2algebra

Upper deviation. By [L2], $(1 + u)^{n} - 1 = \sum_{k = 1}^{n} (\binom{n}{k}) u^{k} \leq \sum_{k = 1}^{n} n^{k} u^{k}$ , since $(\binom{n}{k}) \leq n^{k}$ and $u \geq 0$ .

2.1step 1.2L3algebra

The geometric series of [L3] at $r = n u$ , where $0 \leq n u < 1$ , gives $\sum_{k = 1}^{\infty} (n u)^{k} = n u / (1 - n u) = γ_{n}$ , so step 1.2 gives $(1 + u)^{n} - 1 \leq γ_{n}$ .

3.1L2step 1.2step 2.1algebra

Lower deviation. By [L2], $1 - (1 - u)^{n} = - \sum_{k = 1}^{n} (\binom{n}{k}) (- u)^{k} = \sum_{k = 1}^{n} (\binom{n}{k}) (- 1)^{k + 1} u^{k} \leq \sum_{k = 1}^{n} (\binom{n}{k}) u^{k} \leq γ_{n}$ , the last estimate being step 1.2 and step 2.1; hence $(1 - u)^{n} \geq 1 - γ_{n}$ .

4.1step 1.1step 2.1step 3.1algebra

Define $θ_{n} : = \prod_{i < n} (1 + δ_{i}) - 1$ . Step 1.1 gives $(1 - u)^{n} - 1 \leq θ_{n} \leq (1 + u)^{n} - 1$ , and steps 2.1 and 3.1 give $(1 - u)^{n} - 1 \geq - γ_{n}$ and $(1 + u)^{n} - 1 \leq γ_{n}$ , so $- γ_{n} \leq θ_{n} \leq γ_{n}$ , that is $∣ θ_{n} ∣ \leq γ_{n}$ .

5.1step 4.1∎

Step 4.1 is exactly the claim.

Depends on

Used by

Dependency tree · two levels

27 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

James Demmel, Math 221 Lecture 2: Floating Point Arithmetic (standard reference, not scraped)
David Bindel, CS 6210: Floating Point and Error Analysis (standard reference, not scraped)