Probability generating functions

DefinitionProbability generating function#✓fully proved

For a measure \(\mu\) on \(\Omega\) and a function \(X : \Omega \to \mathbb{N}\), the probability generating function of \(X\) under \(\mu\) is the function \(G_X : \mathbb{R} \to \mathbb{R}\) given by

\[G_X(s) = \int_\Omega s^{X(\omega)} \, d\mu(\omega),\]

which is the expectation \(\mathbb{E}[s^X]\) when \(\mu\) is a probability measure.

For a finite measure \(\mu\) and measurable \(X\) the integral converges whenever \(|s| \le 1\). Where \(s^X\) is not integrable, the integral is taken to be \(0\).

noncomputable def pgf (X : Ω → ℕ) (μ : Measure Ω) (s : ℝ) : ℝ :=
  ∫ ω, s ^ X ω ∂μ

Used by 22

Used byComparison principle for Galton–Watson extinction · Superspreading raises the extinction probability · Negative-binomial extinction probability is the least fixed point · Generating function of the negative-binomial law in closed form · Haldane's equation for the survival probability · Generating function of the Poisson distribution · Survival probability is less than one · Nonnegativity of the survival probability · Beneficial mutant survives with positive probability · Galton–Watson extinction criterion · Least fixed point equals one iff mean offspring is at most one · Extinction probability is the least fixed point · Limit of generating-function iterates is the least fixed point · Iterates of the offspring generating function stay in (0, 1) · Probability of extinction by generation n · Iterates of the generating function at zero are nondecreasing · Extinction by generation n is nondecreasing in n · Generating function of the n-th generation size · Generating function of a sum of independent variables · Series form of the probability generating function · The generating function at \(s = 1\) · The generating function at \(s = 0\)

TheoremIntegrability of \(s^X\) for \(|s| \le 1\)#✓fully proved

Let \(\mu\) be a finite measure on \(\Omega\), let \(X : \Omega \to \mathbb{N}\) be measurable, and let \(s\) be a real number with \(|s| \le 1\). Then the function \(\omega \mapsto s^{X(\omega)}\) is integrable with respect to \(\mu\).

theorem integrable_pow_of_abs_le_one {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → ℕ}
    (hX : Measurable X) {s : ℝ} (hs : |s| ≤ 1) :
    Integrable (fun ω => s ^ X ω) μ

Used by 7

Used byComparison principle for Galton–Watson extinction · Least fixed point equals one iff mean offspring is at most one · Limit of generating-function iterates is the least fixed point · Iterates of the offspring generating function stay in (0, 1) · Iterates of the generating function at zero are nondecreasing · Generating function of the n-th generation size · Generating function of a sum of independent variables

TheoremThe generating function at \(s = 1\)#✓fully proved

For every probability measure \(\mu\) on \(\Omega\) and every function \(X : \Omega \to \mathbb{N}\), the probability generating function \(G_X(s) = \int_\Omega s^{X(\omega)} \, d\mu(\omega)\) of \(X\) under \(\mu\) satisfies \(G_X(1) = 1\).

@[simp]
theorem pgf_one (X : Ω → ℕ) (μ : Measure Ω) [IsProbabilityMeasure μ] : pgf X μ 1 = 1

Uses 1

Statement usesProbability generating function

TheoremThe generating function at \(s = 0\)#✓fully proved

Let \(\mu\) be a measure on \(\Omega\) and let \(X : \Omega \to \mathbb{N}\) be measurable. Then the probability generating function \(G_X(s) = \int_\Omega s^{X(\omega)} \, d\mu(\omega)\) of \(X\) under \(\mu\) satisfies \(G_X(0) = \mu(\lbrace \omega : X(\omega) = 0 \rbrace)\), where the measure of the event is read as a real number, an infinite value being read as \(0\).

When \(\mu\) is a probability measure this is the probability that \(X = 0\), and when \(\mu\) is finite it is the mass of that event.

theorem pgf_zero (X : Ω → ℕ) (μ : Measure Ω) (hX : Measurable X) :
    pgf X μ 0 = μ.real {ω | X ω = 0}

Uses 1 · Used by 1

Statement usesProbability generating function

Used byProbability of extinction by generation n

TheoremSeries form of the probability generating function#✓fully proved

Let \(\mu\) be a finite measure on \(\Omega\), let \(X : \Omega \to \mathbb{N}\) be measurable, and let \(s\) be a real number with \(|s| \le 1\). Then the probability generating function \(G_X(s) = \int_\Omega s^{X(\omega)} \, d\mu(\omega)\) of \(X\) under \(\mu\) satisfies

\[G_X(s) = \sum_{k=0}^{\infty} s^k \, \mu(\{\omega \in \Omega : X(\omega) = k\}).\]

theorem pgf_eq_tsum (X : Ω → ℕ) (μ : Measure Ω) [IsFiniteMeasure μ] (hX : Measurable X)
    {s : ℝ} (hs : |s| ≤ 1) :
    pgf X μ s = ∑' k, s ^ k * μ.real {ω | X ω = k}

Uses 1

Statement usesProbability generating function

TheoremGenerating function of a sum of independent variables#✓fully proved

Let \(\mu\) be a finite measure on \(\Omega\), and for \(Z : \Omega \to \mathbb{N}\) write \(G_Z(s) = \int_\Omega s^{Z(\omega)} \, d\mu(\omega)\) for the probability generating function of \(Z\) under \(\mu\). If \(X, Y : \Omega \to \mathbb{N}\) are measurable and independent under \(\mu\), then \(G_{X+Y}(s) = G_X(s) \, G_Y(s)\) for every real \(s\) with \(|s| \le 1\).

theorem pgf_add_of_indepFun {μ : Measure Ω} [IsFiniteMeasure μ] {X Y : Ω → ℕ}
    (hX : Measurable X) (hY : Measurable Y) (hXY : IndepFun X Y μ) {s : ℝ} (hs : |s| ≤ 1) :
    pgf (fun ω => X ω + Y ω) μ s = pgf X μ s * pgf Y μ s

Uses 2

Statement usesProbability generating function

Proof usesIntegrability of \(s^X\) for \(|s| \le 1\)

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.