LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Normalization, moments, and generating function of the Poisson count law

Statement

For finite $λ \geq 0$ , the masses in The scalar Poisson count law sum to one. If $N \sim Pois (λ)$ , then $E [N] = λ, E [N (N - 1)] = λ^{2}, E [N^{2}] = λ^{2} + λ, Var (N) = λ,$ and $E [s^{N}] = \exp (λ (s - 1))$ for $0 \leq s \leq 1$ .

Facts & Assumptions

Given: A finite parameter $λ \geq 0$ and the mass formula in The scalar Poisson count law.

[F1]

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

[F2]

The real exponential is defined by the convergent power series $e^{x} = \sum_{k \geq 0} x^{k} / k!$ and satisfies $e^{a} e^{b} = e^{a + b}$ . (The real exponential function and the number $e$ by a power series, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ )

[F3]

Expectation is integration against the probability law, and variance is $E [(N - E N)^{2}]$ when the second moment is finite. (Expectation of a nonnegative or integrable random variable, Moments, variance, and covariance on a probability space)

Proof

technique · direct

1.1givenF1

If $λ = 0$ , [F1] puts all mass at $0$ , so the masses sum to one and the stated moments and generating function have their asserted values.

1.2givenF1F2algebra

Suppose $λ > 0$ . By [F1] and the defining exponential series [F2], $\sum_{k = 0}^{\infty} e^{- λ} \frac{λ^{k}}{k!} = e^{- λ} e^{λ} = 1.$ Thus the displayed masses normalize to a probability law.

2.1step 1.2F1F2F3algebra

Using [F1] and reindexing the nonnegative series, $E [N] = e^{- λ} \sum_{k = 1}^{\infty} k \frac{λ^{k}}{k!} = λ e^{- λ} \sum_{j = 0}^{\infty} \frac{λ^{j}}{j!} = λ .$

3.1step 2.1F1F2F3algebra

Reindexing with $j = k - 2$ gives $E [N (N - 1)] = e^{- λ} \sum_{k = 2}^{\infty} k (k - 1) λ^{k} / k! = λ^{2} e^{- λ} \sum_{j = 0}^{\infty} λ^{j} / j! = λ^{2}$ by [F2]. Since $N^{2} = N (N - 1) + N$ , this and step 2.1 yield $E [N^{2}] = λ^{2} + λ$ and hence $Var (N) = E [N^{2}] - (E N)^{2} = λ$ .

4.1step 1.1F1F2algebra∎

For $0 \leq s \leq 1$ , [F1] and [F2] give $E [s^{N}] = e^{- λ} \sum_{k = 0}^{\infty} \frac{(λ s)^{k}}{k!} = e^{- λ} e^{λ s} = e^{λ (s - 1)} .$ Together with step 1.1 this proves the generating-function formula also at $λ = 0$ .

Depends on

Used by

Cited to discharge well-definedness by The scalar Poisson count law.

Dependency tree · two levels

36 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

Gunter Last and Mathew Penrose, Lectures on the Poisson Process, author-hosted 2017 version (standard reference, not scraped)
Adrian Baddeley, Spatial Point Processes and their Applications, complete lecture notes (standard reference, not scraped)