CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04

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.

Expectation agrees with the published finite weighted sum

Statement

Let $(Ω, w)$ be a finite probability space and let $X : Ω \to R$ . After identifying $(Ω, w)$ with the full-power-set probability space of Finite probability spaces are exactly finite full-power-set probability spaces, the expectation defined by Expectation of a nonnegative or integrable random variable agrees with the published finite formulas: $E [X] = \sum_{ω \in Ω} X (ω) w (ω) = \sum_{x \in X (Ω)} x P (X = x) .$

Facts & Assumptions

Given: A finite probability space $(Ω, w)$ and a real-valued function $X : Ω \to R$ .

[L1]

Finite probability spaces are exactly full-power-set probability spaces, and every finite real random variable is measurable there (Finite probability spaces are exactly finite full-power-set probability spaces, Finite random variables are measurable).

[L2]

Change of variables for expectation identifies $E [X]$ with the integral of the identity function against the law of $X$ (Change of variables for expectation).

[L3]

The published finite expectation is $\sum_{ω \in Ω} X (ω) w (ω)$ , and it is also the sum over attained values weighted by their probabilities (Expectation of a real random variable on a finite probability space, Expectation is the sum of each attained value times its probability).

Proof

technique · direct

1.1

By [L1], the general expectation and the law of $X$ are defined on the same full-power-set probability space attached to $(Ω, w)$ .

2.1

Applying [L2] to the identity map on $R$ gives $E [X] = \int_{R} x d P_{X} .$ For a finite random variable, [L3] identifies this quantity with both $\sum_{ω \in Ω} X (ω) w (ω) and \sum_{x \in X (Ω)} x P (X = x) .$

step 1.1L2L3

3.1

Thus the general expectation is exactly the published finite weighted-sum expectation and its finite-distribution reformulation.

step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Rick Durrett, Probability: Theory and Examples, 5th ed., Section 1.6.3 (standard reference, not scraped)