Alphabeta Math

Finite Probability Spaces and Random Variables

About this page
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.

✓ 19 results · all verified · 6 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 13 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
2 · Logical flowchart

3 · Items

Definition

Finite probability spaces, outcome weights, events, and event probabilities

Lemma

Normalization, nonnegativity, monotonicity, complements, and differences in a finite probability space

Theorem

Probability is additive on every finite pairwise-disjoint family of events

Corollary

Two-event inclusion-exclusion: ℙ(A∪ B)=ℙ(A)+ℙ(B)-ℙ(A∩ B)

Theorem

The finite union bound

Definition

Conditional probability ℙ(A∣ B) for ℙ(B)>0

Theorem

The multiplication rule and finite chain rule for conditional probability

Theorem

The law of total probability for a finite partition

Theorem

Bayes' theorem over a finite partition

Definition

Independent events, pairwise independence, and mutual independence of a finite family

Theorem

Two positive-probability events are independent exactly when conditioning on either leaves the other's probability unchanged

Lemma

Mutual independence is inherited by subfamilies and by replacing events with complements

Definition

The uniform probability space on a nonempty finite set

Definition

The finite product of finite probability spaces

Theorem

Product weights normalize, and coordinate events are mutually independent

Definition

Real random variables on finite probability spaces and their finite distributions

Definition

Expectation of a real random variable on a finite probability space

Lemma

Expectation is the sum of each attained value times its probability

Theorem

Expectation is linear for every finite family of random variables, without any independence hypothesis

Theorem

Expectation preserves pointwise order and lies between the minimum and maximum attained values

Definition

The indicator random variable of an event

Lemma

Indicators turn event probabilities, intersections, and finite counts into expectations and products

Definition

Pairwise and mutual independence of finite-valued random variables

Theorem

A finite family of events is mutually independent exactly when its indicators are mutually independent

Definition

Variance, standard deviation, and covariance on a finite probability space

Lemma

Var(X)=E[X²]-E[X]² and Cov(X,Y)=E[XY]-E[X]E[Y]

Definition

Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials

Theorem

Markov's inequality on a finite probability space

Theorem

Chebyshev's inequality on a finite probability space

Lemma

Cauchy-Schwarz for finite random variables: E[XY]² leE[X²]E[Y²]

Theorem

The finite second-moment bound ℙ(X≠0)geE[X]²/E[X²] when E[X²]>0

Corollary

ℙ(X=0)leVar(X)/E[X]² whenever E[X]≠0

Sources