Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Every probability measure, in particular the measure of a probability space, is a finite measure.
The Borel Sets of ℝⁿ Form a σ-Algebra, and Intervals of ℝ Are Sets
helperhlp:borel-euclidean-interval-set-2026aThe Borel sets of ℝⁿ form a σ-algebra, so ℝⁿ with them is a measurable space; and every interval of ℝ is a set.Order Facts for Natural Numbers: Not Less Than Gives Greater or Equal, and Below n+1 Gives at Most n
helperhlp:natural-order-negation-successor-2026aFor natural numbers m and n, failure of m<n gives n≤m, and m<n+1 gives m≤n.Ordered Pairs in a Map between Classes: Membership as a Value, and the Components Lie in the Domain and the Codomain
helperhlp:class-map-pairs-2026aFor a map F:A→B between arbitrary classes, a pair (a,b) lies in F exactly when F(a)=b, and the components of any pair in F lie in A and B respectively.- Intersecting the empty set with any class, on either side, gives the empty set.
An Element of [0,∞] below a Real Number Is a Real Number
helperhlp:nonnegative-extended-below-real-2026aAnalysisAn element of [0,∞] that is at most some real number is itself a real number.Cancelling an Added Real, and the Product of a Real with a Negative
lemmalem:real-add-cancel-negative-product-2026aAlgebraSet TheoryIn the real numbers, a summand added to both sides of an equation can be cancelled, and the product of a real number with the negative of another is the negative of their product.- Standing notation for conditional expectations: a sub-σ-algebra G of F, G-measurable and Borel functions, and pointwise products of random variables and random vectors.
- Under dependent choice, a random variable measurable with respect to the σ-algebra generated by a random element Z of a metric space S is a Borel function of Z; consequently the conditional expectation of an integrable random variable or vector given Z has a version of the form h…
Conditional Jensen Inequality, Lᵖ Contraction and Convergence Theorems for Conditional Expectations
lemmalem:conditional-expectation-convergence-2026aProbabilityA convex function of a version of a conditional expectation is almost surely at most a version of the conditional expectation of the convex function; versions contract the p-th moment; and versions converge almost surely under monotone convergence and in mean under dominated conv…Integrals with Respect to the Restriction of a Measure to a Sub-σ-Algebra
lemmalem:integral-sub-sigma-algebra-2026aFor a σ-algebra G contained in F, a G-measurable function has the same integral with respect to the restriction of μ to G as with respect to μ, over the whole space and over every set of G, and it is integrable for one measure exactly when it is for the other.Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites
helperhlp:random-element-sigma-families-2026aBeing a metric space, lying in a ball, being open, being a σ-algebra on a set and being a Borel set are predicative conditions with the space and the metric as variables; consequently, for families of random elements indexed by an arbitrary set, the families of their generated σ-…Independent Random Elements: Preimages, Functions and Blocks
lemmalem:independent-random-elements-2026aIndependence of random elements is tested on preimages of Borel sets, is preserved by measurable functions, and passes to disjoint blocks of an independent finite family of random variables.- The σ-algebra generated by a random element, or by a family of random elements, is the σ-algebra generated by the preimages of Borel sets.
The σ-Algebra Generated by Measurable Functions into Metric Spaces
lemmalem:sigma-algebra-random-elements-2026aThe σ-algebra generated by the preimages of Borel sets under measurable functions into metric spaces lies in the given σ-algebra, makes the functions measurable, and is the smallest σ-algebra that does; for a family it is also generated by the σ-algebras of the single functions.- The distribution function of a probability measure on the real line is nondecreasing with values in [0,1], right-continuous, tends to 0 at minus infinity and to 1 at plus infinity, and determines the measure; so two random variables are identically distributed exactly when their…
Rules for Expectations, Variances and Covariances
lemmalem:expectation-variance-rules-2026aProbabilityExpectation is linear and monotone, gives probabilities of events and fixes constants, and commutes with affine functions of random vectors; variance and covariance obey the usual second-moment formulas, and covariance matrices are symmetric positive semidefinite and transform as…- Standing notation for probability: a probability space, events of the form {X in B} and their probabilities, random elements and their laws and distribution functions, expectation, variance and covariance, and almost sure properties.
Lᵖ Inclusions and Constants on a Finite Measure Space
lemmalem:lp-inclusion-finite-measure-2026aAnalysisProbabilityOn a finite measure space every q-integrable function is p-integrable for p at most q, the product of two square-integrable functions is integrable with the Cauchy-Schwarz bound, and constant functions are p-integrable with integral the constant times the total mass.Finite Signed Measures from Finite Measures and from Integrals
lemmalem:signed-measure-examples-2026aFinite measures and differences of finite measures are finite signed measures; measures and finite signed measures restrict to sub-σ-algebras; and the indefinite integral of an integrable function over the sets of a sub-σ-algebra is a finite signed measure, absolutely continuous…