Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Standard Normal Vectors: Density, Moments, Orthogonal Invariance and Concatenation
lemmalem:standard-normal-vector-2026aProbabilityA random vector is a standard normal vector exactly when its law has the density c_G^{-k} exp(-|x|^2/2) on R^k; such a vector has mean zero and identity covariance, stays standard normal under matrices with orthonormal rows, and two independent ones concatenate to a standard norm…- If real random variables X_n converge in distribution to X and Y_n converge in probability to a constant c, then X_n + Y_n converges in distribution to X + c and Y_n X_n to cX.
Convergence in Distribution of Real Random Variables through Distribution Functions
theoremthm:distribution-function-convergence-2026aProbabilityReal random variables converge in distribution exactly when their distribution functions converge at every point where the limiting distribution function is continuous.Implications between Modes of Convergence of Random Elements
theoremthm:convergence-modes-implications-2026aProbabilityFor random elements of a separable metric space: almost sure convergence and convergence in Lᵖ imply convergence in probability, which implies convergence in distribution and almost sure convergence along a subsequence; limits in probability are almost surely unique.The Distance of Two Random Elements of a Separable Metric Space Is a Random Variable
lemmalem:distance-random-elements-separable-2026aProbabilityFor random elements X and Y of a separable metric space, the function sending an outcome to the distance between X and Y at that outcome is a random variable.The Real Line and Euclidean Space Are Separable
lemmalem:real-euclidean-separable-2026aAnalysisTopologyThe rationals form a countable dense subset of the real line, and the rational tuples a countable dense subset of Euclidean space, so both are separable metric spaces.A Measurable Real Function Has Null Level Sets at Levels Arbitrarily Close to Any Point, for a Finite Measure
lemmalem:null-level-sets-finite-measure-2026aAnalysisProbabilityFor a finite measure and a measurable real function, every open interval of levels contains a level whose level set has measure zero; in particular there are such levels converging to any given real number from above.Bounded Continuous Functions on a Metric Space: Measurability, Integrals, Operations, Lipschitz Functions and Approximation of Closed Sets
lemmalem:bounded-continuous-functions-metric-2026aAnalysisTopologyBounded continuous functions on a metric space are Borel and integrable against every finite Borel measure, with the integral bounded by the bound times the total mass; they are closed under sums, multiples, products, truncation and composition with continuous functions; bounded…Bounded Continuous Functions on a Metric Space
definitiondef:bounded-continuous-functions-metric-2026aAnalysisTopologyThe set of real functions on a metric space that are continuous and bounded in absolute value by a single constant.Convergence of Probability Measures and Random Elements: Standing Notation
settingset:convergence-notation-2026aProbabilityStanding notation for metric spaces with their Borel sets, finite Borel and Borel probability measures, closure, interior, boundary and distance to a set, the bounded continuous functions, weak convergence of measures, and the modes of convergence of random elements.The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions
helperhlp:integral-predicative-2026aAnalysisThe relation between a measure (or a map from the σ-algebra to [0,∞], or a finite signed measure from a given class), a function and the value of its integral is expressed by a predicative formula, for the simple integral, the integral of a nonnegative measurable function, the in…Helly Selection Theorem for Finite Signed Borel Measures on a Locally Compact Separable Metric Space
theoremthm:helly-selection-radon-2026aAnalysisProbabilityOn a locally compact separable metric space, every sequence of finite signed Borel measures with total variation norms at most M has a subsequence converging vaguely to a finite signed Borel measure of norm at most M, which is nonnegative when the measures of the sequence are.Vague Convergence of Finite Signed Borel Measures
definitiondef:vague-convergence-2026aAnalysisProbabilityA sequence of finite signed Borel measures on a metric space converges vaguely to a finite signed Borel measure if the integrals of every continuous function with compact support converge.Banach–Alaoglu Theorem for a Separable Normed Space: the Closed Balls of the Dual Are Weak-Star Sequentially Compact and Compact for a Metric of Weak-Star Convergence
theoremthm:banach-alaoglu-separable-2026aAnalysisTopologyIn the dual of a separable real normed space, every sequence of functionals of dual norm at most M has a weak-star convergent subsequence with limit of dual norm at most M; on this ball weak-star convergence of sequences is convergence for an explicit metric, for which the ball i…Weak-Star Compactness and Vague Convergence: Standing Notation
settingset:weak-star-compactness-notation-2026aAnalysisStanding notation for weak-star compactness in duals of separable normed spaces and for vague convergence of finite signed Borel measures: it extends the notation for the dual of C_c(X) and names the closed balls of a dual space.The Finite Signed Borel Measures on a Locally Compact Separable Metric Space Form a Banach Space under the Total Variation Norm
corollarycor:signed-radon-measures-banach-2026aAnalysisOn a locally compact separable metric space, the finite signed Borel measures with the total variation norm form a real Banach space, because the Riesz representation identifies them isometrically with the dual of the continuous functions with compact support.The Riesz–Markov Representation Theorem on a Locally Compact Metric Space
theoremthm:riesz-markov-locally-compact-2026aAnalysisProbabilityEvery positive linear functional on C_c(X), X a locally compact metric space, is integration against a unique Radon measure; when the functional is bounded for the uniform norm, the measure is finite and its total mass equals the dual norm.Riesz Representation Theorem: the Dual of the Continuous Functions with Compact Support Is the Space of Finite Signed Borel Measures
theoremthm:riesz-representation-cc-dual-2026aAnalysisOn a locally compact separable metric space, integration against a finite signed Borel measure is a bounded linear functional on the continuous functions with compact support whose dual norm is the total variation norm of the measure; this correspondence is linear, and every boun…Jordan Decomposition of a Bounded Linear Functional on the Continuous Functions with Compact Support
lemmalem:jordan-decomposition-functional-cc-2026aAnalysisEvery bounded linear functional on the space of continuous functions with compact support on a metric space is the difference of two bounded positive linear functionals whose dual norms are at most its own; the positive part is the supremum of the functional over the nonnegative…The Radon Measure of a Positive Linear Functional on : the Outer Measure, Compact Sets, Borel Measurability and Regularity
lemmalem:riesz-measure-construction-2026aAnalysisProbabilityFrom a positive linear functional on C_c(X), X a locally compact metric space, the supremum of its values on functions below 1 supported in an open set defines a set function on open sets; its outer extension is an outer measure that is finite on compact sets, where it is the inf…