LemmaStatement: AI-adaptedProof: AI-adapted

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.

The moment generating function of a finite sum of independent variables is the product of their moment generating functions

Statement

Let $(X_{i})_{i \in I}$ be a finite mutually independent family of real random variables on a common probability space, with independence in the sense of Independent random elements. For any real random variable $X$ on that space, use the extended nonnegative notation $M_{X} (t) : = \int_{Ω} \exp (t X) d P = E [\exp (t X)] \in [0, + \infty], t \in R .$ Then, for every real $t$ , $M_{\sum_{i \in I} X_{i}} (t) = \prod_{i \in I} M_{X_{i}} (t) .$ The extended product uses the nonnegative expectation-product convention: a zero factor makes the product zero even if another is infinite. The identity requires no exponential-moment finiteness assumption. Whenever all individual $M_{X_{i}} (t)$ are finite, the left side is finite as well. In the original finite-probability-space convention of The moment generating function $M_{X} (t) = E [e^{t X}]$ on a finite probability space, the integrals are finite sums, so this is exactly the original everywhere-finite MGF identity. Finite-valued atom independence suffices in that case. For $I = \emptyset$ , both sides equal $1$ .

Facts & Assumptions

Given: A finite mutually independent family $(X_{i})_{i \in I}$ of real random variables on one probability space, and $t \in R$ .

[L1]

The expectation of a nonnegative measurable variable is its extended nonnegative integral; the original finite-space MGF is $M_{X} (t) = E [\exp (t X)]$ . (Expectation of a nonnegative or integrable random variable, The moment generating function $M_{X} (t) = E [e^{t X}]$ on a finite probability space)

[L2]

Expectation factors over finite products of mutually independent nonnegative real random variables in $[0, + \infty]$ , with the stated zero-factor convention; finite-valued atom independence on the original finite space is sufficient. (Expectation factors over a finite product of mutually independent random variables)

[L3]

$\exp (x + y) = \exp (x) \exp (y)$ for all reals $x, y$ , and $\exp$ is positive. (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ )

[L4]

Independence is independence of the coordinate inverse-image sigma-algebras. (Independent random elements)

[L5]

The exponential is smooth, hence continuous, and the Borel sigma-algebra is generated by open sets. (The exponential function is smooth and $(\exp)^{'} = \exp$ , The Borel sigma-algebra of a topological space)

Proof

technique · direct

1.1L2L3L4L5

In the original finite-valued atom-independence convention, summing joint atom probabilities over finite attained-value sets proves independence for Borel inverse-image events, as in the finite-valued bridge of [L2]. The map $f_{t} (x) = \exp (t x)$ is continuous by [L5]. The family ${B \subseteq R : f_{t}^{- 1} (B) \in B (R)}$ is a sigma-algebra, since inverse images preserve complements and countable unions, and it contains the open sets by continuity. Therefore it contains every Borel set by [L5], so $f_{t}$ is Borel measurable. Hence $Y_{i} = f_{t} (X_{i})$ is a measurable nonnegative real variable by [L3]. For any Borel set $B$ , ${Y_{i} \in B} = {X_{i} \in f_{t}^{- 1} (B)} \in σ (X_{i}) .$ Thus $σ (Y_{i}) \subseteq σ (X_{i})$ , and the independence in [L4] passes to the family $(Y_{i})_{i \in I}$ . This inverse-image argument uses no choice principle.

2.1step 1.1L1L2L3

Iterating [L3] gives $\exp (t \sum_{i} X_{i}) = \prod_{i} Y_{i}$ pointwise. Apply the nonnegative branch of [L2] to the independent variables from step 1.1 and use [L1] in each factor to obtain the displayed equality in $[0, + \infty]$ . If every individual MGF is finite at $t$ , the finite product on the right is finite. On an original finite probability space, all exponential variables are bounded, so [L1] identifies these integrals with the finite MGFs, and [L2] also covers its finite-valued atom-independence convention.

3.1step 2.1L1L3∎

For $I = \emptyset$ , the sum is zero and the random product is $1$ . Thus $M_{0} (t) = E [\exp (0)] = 1$ on a probability space, and the product on the right is the empty product $1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

Y. Zhao, MIT 18.218 Probabilistic Method in Combinatorics, Section 4.1 (standard reference, not scraped)