Probability

Markov's Inequality

A non-negative random variable rarely exceeds a multiple of its expectation

lean4-proofprobabilityvisualization

Chebyshev's Inequality

A random variable rarely deviates from its mean by more than a few standard deviations

lean4-proofprobabilityvisualization

Bayes' Theorem

Reversing conditional probability to update beliefs from evidence

lean4-proofprobabilityvisualization

Jensen's Inequality

For a convex function phi, phi(E[X]) <= E[phi(X)] — the image of the mean is at most the mean of images

lean4-proofprobabilityvisualization

Holder's Inequality

For conjugate exponents p and q, the L^p and L^q norms bound the integral of a product

lean4-proofprobabilityvisualization

Minkowski's Inequality

The L^p norm satisfies the triangle inequality: ||f+g||_p <= ||f||_p + ||g||_p for p >= 1

lean4-proofprobabilityvisualization

Borel-Cantelli Lemma

If the sum of event probabilities is finite, almost surely only finitely many events occur

lean4-proofprobabilityvisualization

Law of Total Expectation

The expectation of X equals the expectation of its conditional expectation: E[X] = E[E[X|Y]]

lean4-proofprobabilityvisualization

Law of Total Variance

Var(X) decomposes as the sum of the expected conditional variance and the variance of the conditional mean

lean4-proofprobabilityvisualization

Linearity of Conditional Expectation

Conditional expectation is linear: E[aX+bY|G] = aE[X|G] + bE[Y|G] almost surely

lean4-proofprobabilityvisualization

Martingale Definition

A stochastic process is a martingale if future conditional expectations equal the current value

lean4-proofprobabilityvisualization

Strong Law of Large Numbers

The sample mean of i.i.d. integrable random variables converges almost surely to the population mean

lean4-proofprobabilityvisualization

Central Limit Theorem

Standardized sums of i.i.d. finite-variance random variables converge in distribution to the standard normal

lean4-proofprobabilityvisualization

Kolmogorov 0-1 Law

Every tail event of an independent sequence of random variables has probability exactly 0 or 1

lean4-proofprobabilityvisualization

Doob's Martingale Convergence

An L1-bounded submartingale converges almost surely to an integrable limit

lean4-proofprobabilityvisualization

Optional Stopping Theorem

The expected value of a stopped martingale equals its initial value under integrability conditions

lean4-proofprobabilityvisualization

Characteristic Function

The characteristic function φ_X(t) = E[exp(itX)] uniquely determines the distribution of a random variable

lean4-proofprobabilityvisualization

Chernoff Bound

The tail probability P(X ≥ ε) is bounded exponentially by the moment generating function

lean4-proofprobabilityvisualization

Weak Convergence (Distribution)

A sequence of probability measures converges weakly if integrals of bounded continuous functions converge

lean4-proofprobabilityvisualization