Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Existence of Independent Sequences with Prescribed Distributions
theoremthm:existence-independent-sequence-2026aProbabilityLet be a sequence of probability measures on , where is the set of real numbers, is the Borel -algebra, and is the set of natural numbers. Then there exist…Joint Distribution, Expectations, and Block Independence for Independent Random Variables
theoremthm:independent-block-functions-2026aProbabilityThroughout, is a natural number with , is Euclidean space, denotes the real numbers, and the Borel -algebra. Define the -fold product Borel -algebra on iteratively…Smooth Test Function Criterion for Convergence in Distribution
theoremthm:smooth-test-convergence-distribution-2026aAnalysisProbabilityLet and be random variables, not necessarily on a common probability space, and let denote the real numbers. Call a function an admissible test function if is bounded, is a map on…- Let be a random variable on a probability space with distribution , let denote the real numbers, and let be measurable with respect to the Borel -algebra on both sides. Then …
- 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 Weight Defines a Probability Distribution
theoremthm:gaussian-integral-2026aAnalysisProbabilityLet with the exponential function, let be Lebesgue measure, and for a Borel set let the integral of Lebesgue Integral of a Nonnegative Measurable Function of the measurable function…- Define by , with the exponential function; is continuous (a composition of continuous maps, by Composition of Continuous Euclidean Maps and claim 3 of Basic Properties of the Exponential Function), hence measurable with respect…
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…- Let be a sequence of independent and identically distributed random variables on a probability space such that and have finite expectation, and write . For let…
Expectation of a Product of Independent Random Variables
lemmalem:expectation-product-independent-2026aProbabilityLet and be independent random variables on a probability space , each with finite expectation. Then the product (a random variable, since and sums, differences, and squares of random variables are r…- Let and be random variables on a common probability space, with the modes of convergence of Almost Sure Convergence, Convergence in Probability, and Convergence in Distribution. Then: 1. if almost surely, then in probability; 2.…
Almost Sure Convergence, Convergence in Probability, and Convergence in Distribution
definitiondef:convergence-modes-2026aProbabilityLet and be random variables on a common probability space (for convergence in distribution, a common space is not required). 1. converges to almost surely if…- Let be a probability space and let be a sequence of events. Define an event by the closure properties of Sigma-Algebra and Measurable Space; it consists of exactl…
- Let be a random variable on a probability space and let . Markov's inequality. If pointwise, then with the expectation in (the inequality being trivial when the right side is i…
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…Independence of Events and of Random Variables
definitiondef:independence-events-rvs-2026aProbabilityLet be a probability space. Events are independent if for every nonempty subset , with the finite product notation. A sequence (or arbitra…- Let be a random variable on a probability space . If pointwise, the expectation of is , the integral of Lebesgue Integral of a Nonnegative Measurable Function. If is integrable with respec…
Distribution and Cumulative Distribution Function of a Random Variable
definitiondef:distribution-cdf-random-variable-2026aProbabilityLet be a random variable on a probability space . The distribution (or law) of is the function on the Borel -algebra. It is a probability measure on…Probability Space, Event, and Random Variable
definitiondef:probability-space-random-variable-2026aProbabilityA probability space is a measure space whose measure is a probability measure in the sense of that definition, that is, . Members of are called events, and is the probability of the event . A random variable on…- Let and be -finite measure spaces and let be the product measure on the product -algebra. Sections. For measurable with respect to (in the sense…