LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

A geometric upper bound for a Poisson right tail

Statement

For $N \sim Pois (μ)$ with $μ \geq 0$ and integer $K \geq 0$ , write $τ_{K} (μ) : = P (N > K)$ . If $μ = 0$ , then $τ_{K} (μ) = 0$ . If $μ > 0$ and $μ < K + 2$ , then

$τ_{K} (μ) \leq \frac{e^{- μ} μ^{K + 1}}{(K + 1)! (1 - μ / (K + 2))} .$

The right side is a geometric majorant computed from a Poisson mass, not a floating-point subtraction of a rounded partial sum from one.

Facts & Assumptions

Given: A finite parameter $μ \geq 0$ and integer $K \geq 0$ .

[F1]

For $μ > 0$ , $P (N = k) = e^{- μ} μ^{k} / k!$ ; at $μ = 0$ the law is concentrated at zero. (The scalar Poisson count law)

[F2]

The masses in The scalar Poisson count law normalize to one, so $P (N > K) = \sum_{k > K} P (N = k)$ . (Normalization, moments, and generating function of the Poisson count law)

[F3]

Factorials satisfy $(k + 1)! = (k + 1) k!$ for $k \geq 0$ . (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ )

[F4]

For $0 \leq ρ < 1$ , the geometric series satisfies $\sum_{j \geq 0} ρ^{j} = 1 / (1 - ρ)$ . (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges)

Proof

technique · direct

1.1givenF1F3algebra

If $μ = 0$ , [F1] gives $N = 0$ almost surely and $K \geq 0$ , so the tail is zero. Now suppose $μ > 0$ and put $w_{k} = e^{- μ} μ^{k} / k!$ and $ρ = μ / (K + 2)$ . The hypothesis gives $0 < ρ < 1$ , and [F1]–[F3] yield $w_{k + 1} / w_{k} = μ / (k + 1) \leq ρ$ for every $k \geq K + 1$ .

2.1step 1.1induction

Iterating the ratio bound gives $w_{K + 1 + j} \leq w_{K + 1} ρ^{j}$ for each integer $j \geq 0$ .

3.1F2F4step 2.1algebra∎

By [F2] and step 2.1, $τ_{K} (μ) = \sum_{j \geq 0} w_{K + 1 + j} \leq w_{K + 1} \sum_{j \geq 0} ρ^{j} = w_{K + 1} / (1 - ρ)$ by [F4]; substituting the values of $w_{K + 1}$ and $ρ$ proves the stated bound.

Depends on

Used by

Dependency tree · two levels

37 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

Bennett L. Fox and Peter W. Glynn, Computing Poisson Probabilities (standard reference, not scraped)