Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Defines the real exponential function as the map sending u to the sum of the absolutely convergent series of u^k/k! over k from 0, and the number e as exp(1).
- For σ-finite measure spaces, the integral of a nonnegative product-measurable function against the product measure equals both iterated integrals (Tonelli); for an integrable function the sections are integrable outside a null set, and the iterated integral, set to zero on that n…
- Two σ-finite measures have exactly one product measure on the product σ-algebra, determined by its values μ(A)ν(B) on measurable rectangles; it is σ-finite, and the measure of every product-measurable set is the integral of the measures of its sections, in either order.
- A set of subsets of X is a σ-algebra exactly when it is both a π-system and a λ-system, and a λ-system containing a π-system contains the σ-algebra it generates, which is the smallest λ-system containing it.
Measurable Rectangles and the Product σ-Algebra
definitiondef:product-sigma-algebra-2026bAnalysisProbabilityThe measurable rectangles of two measurable spaces are the sets A×B with A and B measurable, and the product σ-algebra on X×Y is the σ-algebra they generate.Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion
theoremthm:linearity-monotonicity-integral-2026cAnalysisProbabilityThe integral of nonnegative measurable maps is additive, also over series; a measurable real map is integrable exactly when the integral of its absolute value is finite, and the integral on integrable maps is linear, monotone and bounded in absolute value by the integral of the a…- If measurable real maps converge pointwise and are dominated by one integrable map, then the limit and all terms are integrable, the integrals of the distances to the limit tend to zero, and the integrals converge to the integral of the limit.
- For a sequence of nonnegative measurable maps, the pointwise limit inferior is measurable and its integral is at most the limit inferior of the integrals.
- The pointwise supremum of a nondecreasing sequence of nonnegative measurable maps is measurable, and its integral is the supremum of their integrals.
Integrable Functions and Their Lebesgue Integral
definitiondef:lebesgue-integral-integrable-2026cAnalysisProbabilityA real-valued measurable function is integrable when the integrals of its positive and negative parts are finite; L¹(μ) is the set of integrable functions, and the integral of such a function is the difference of those two integrals.Nonnegative Measurable Maps and Their Lebesgue Integral
definitiondef:lebesgue-integral-nonnegative-2026dAnalysisProbabilityM+ is the set of measurable maps into [0,∞]; the integral of such a map is the supremum of the simple integrals of the nonnegative simple functions below it.Simple Functions, Nonnegative Simple Functions, and the Simple Integral
definitiondef:simple-function-integral-2026bAnalysisProbabilityA simple function is a measurable real-valued map with finite image; the simple integral of a nonnegative one is the finite sum over its values c of c times the measure of the level set.Measurable Map, and the Set of Measurable Maps
definitiondef:measurable-function-2026dAnalysisProbabilityDefines measurable maps between measurable spaces and the set of them, and fixes the Borel σ-algebras with respect to which maps into ℝ, ℝⁿ, real p×q matrices and [0,∞] are called measurable.Lebesgue Measure on the Real Line: Existence, Lengths of Intervals and Uniqueness
theoremthm:lebesgue-measure-real-line-2026bAnalysisProbabilityAssuming dependent choice, Lebesgue outer measure is an outer measure, every Borel set is Carathéodory measurable, and Lebesgue measure is a sigma-finite measure on the Borel sets giving each interval its length; it is the only measure on the Borel sets giving each half-open inte…Lebesgue Outer Measure on the Real Line
definitiondef:lebesgue-outer-measure-real-line-2026bAnalysisProbabilityFor a subset A of the real line, the Lebesgue outer measure is the infimum, in [0,∞], of the total lengths of the sequences of open intervals covering A; it defines a map from the power set of the real line to [0,∞].Carathéodory's Theorem: the Measurable Sets of an Outer Measure Form a σ-Algebra on Which It Is a Measure
theoremthm:caratheodory-extension-2026bAnalysisProbabilityFor an outer measure on X, a subset is Carathéodory measurable as soon as the splitting inequality holds for test sets of finite outer measure; the measurable sets form a σ-algebra containing every null set, and the outer measure restricted to them is a measure.- An outer measure on a set X is a map from the power set of X to [0,∞] that vanishes on the empty set, is monotone, and is countably subadditive.
Measure, Measure Space, and Probability Measure
definitiondef:measure-measure-space-2026cAnalysisProbabilityDefines a measure on a measurable space as a countably additive map from the measurable sets to [0,∞] vanishing on the empty set, a measure space, and finite, σ-finite and probability measures.Borel Sigma-Algebra on the Real Line
definitiondef:borel-sigma-algebra-real-line-2026aAnalysisProbabilityIdentify the real line with the Euclidean space . The Borel -algebra on , denoted , is the -algebra generated by the family of all open subsets of . Its members are called Borel sets. In…The σ-Algebra Generated by a Set of Subsets
definitiondef:generated-sigma-algebra-2026cAnalysisProbabilityDefines the σ-algebra σ(C) generated by a set C of subsets of X as the intersection of all σ-algebras on X containing C, and records which sets belong to it.