Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Smooth Test Functions Characterize Convergence in Distribution of Real Random Variables
theoremthm:smooth-test-convergence-distribution-2026bProbabilityReal random variables converge in distribution exactly when the expectations of f(X_n) converge to that of f(X) for every three times continuously differentiable f that is bounded together with its first three derivatives.Taylor Expansion with Third-Order Remainder Bound
lemmalem:taylor-third-order-remainder-2026aAnalysisLet denote the real numbers and let be a map on , and suppose its third derivative is bounded: there is with for all , where , , denote the iterat…- The expectation of a function of a random element is the integral of that function against the law of the random element: for nonnegative functions, for real functions (with integrability transferred both ways), and for vector-valued functions.
- Let be a sequence of independent and identically distributed random variables on a probability space such that and have finite expectation, and suppose ; write…
The Gaussian Integral Is Finite and Positive, and the First Two Gaussian Moments
theoremthm:gaussian-integral-2026cAnalysisProbabilityThe function exp(-x^2/2) is Lebesgue integrable on the real line with positive integral c_G, and x exp(-x^2/2) and x^2 exp(-x^2/2) are integrable with integrals 0 and c_G.- The standard normal density is exp(-x^2/2) divided by the Gaussian constant, and the standard normal distribution is the measure on the real line with this density; a random variable is standard normal if its law is this distribution.
Strong Law of Large Numbers under a Fourth Moment Bound
theoremthm:strong-law-large-numbers-fourth-moment-2026aProbabilityLet be a sequence of independent and identically distributed random variables on a probability space such that has finite expectation (hence so do , , and , since for…- For pairwise uncorrelated square-integrable random variables with common mean m and variances at most σ², the probability that the sample mean S_n/n deviates from m by at least ε is at most σ²/(nε²), and hence tends to 0. Independent identically distributed random variables with…
Expectations and Variances of Independent Random Variables
lemmalem:expectation-product-independent-2026bProbabilityThe expectation of a product of independent random variables is the product of the expectations, for nonnegative and for integrable ones; hence independent square-integrable random variables are uncorrelated, variances add over pairwise uncorrelated summands, and covariance matri…- Let and be random variables on a common probability space, with the modes of convergence of Convergence in Probability. Then: 1. if almost surely, then in probability; 2. if in probability, then in distribu…
- A sequence of random elements of a separable metric space converges in probability to a random element when, for every positive epsilon, the probability that their distance exceeds epsilon tends to zero.
- If the probabilities of a sequence of events have a finite sum, almost surely only finitely many of the events occur; if the events are independent and the sum is infinite, almost surely infinitely many occur.
- The probability that a nonnegative random variable reaches a level a is at most its expectation divided by a, and the probability that a square-integrable random variable deviates from its mean by at least a is at most its variance divided by a².
Existence of Independent and Identically Distributed Sequences
theoremthm:existence-iid-sequence-2026aProbabilityLet be a probability measure on , with the Borel -algebra. Then there exist a probability space and a sequence of random variables on it that is…- Events are independent if the singleton classes they form are; random elements are independent if the σ-algebras they generate are; an iid sequence is an independent sequence of identically distributed random elements.
- The expectation of a random variable is its integral against the probability measure: in [0,∞] for nonnegative measurable functions, in the reals for integrable random variables, and entrywise for integrable random vectors and matrix-valued functions.
- The distribution function of a probability measure on the Borel sets of the real line gives the measure of each closed left ray, and the distribution function of a random variable is that of its law.
Probability Spaces, Events and Random Elements
definitiondef:probability-space-random-variable-2026cProbabilityA probability space is a measure space of total mass one, its events are the measurable sets, and a random element of a metric space is a measurable function into it with its Borel sigma-algebra; random variables and random vectors are the random elements of the real line and of…- The natural logarithm log on the positive reals is the inverse of the exponential function, read as a bijection from the real line onto the positive reals; so exp(log t) = t and log(exp u) = u.
- The real exponential function satisfies exp(0)=1 and exp(u+v)=exp(u)exp(v), is positive with exp(-u)=1/exp(u) and exp(u)>=1+u, has a quadratic remainder bound near 0, is its own derivative on every interval, is continuous and strictly increasing, tends to 0 at minus infinity, and…