Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- For a σ-algebra on a set, there is a set whose elements are exactly the finite signed measures on the measurable space; it is a subset of the set of functions from the σ-algebra to ℝ.
The Natural Numbers Read in ℝ: a Predicative Condition and a Function from ℕ₀ to ℝ
helperhlp:natural-numbers-reals-function-2026aReading an element n of ℕ₀ as the real number n_ℝ is a predicative condition at any two variable positions, and n ↦ n_ℝ is a function from ℕ₀ to ℝ.The Measures, the Finite Measures and the Probability Measures on a Measurable Space Form Sets
helperhlp:measures-form-set-2026aAnalysisProbabilityFor a σ-algebra on a set, there is a set whose elements are exactly the measures on the measurable space, and likewise for the finite measures and for the probability measures; each is a subset of the set of functions from the σ-algebra to [0,∞].The Integral of a Multiple by a Constant in [0,∞], the Constant ∞ Included
lemmalem:integral-extended-scalar-multiple-2026aAnalysisFor a nonnegative measurable function f and a constant c in [0,∞], including c = ∞, the multiple cf is again nonnegative measurable and its integral is c times the integral of f.The Lebesgue Integral over ℝⁿ of a Product of Functions of One Coordinate Each
lemmalem:coordinate-product-integral-rn-2026aAnalysisFor nonnegative measurable functions h_1, ..., h_n on ℝ, the function x ↦ h_1(x_1)⋯h_n(x_n) on ℝⁿ is measurable and its Lebesgue integral is the product of the integrals of the h_j; likewise with each h_j restricted to a Borel set B_j.The Lebesgue Integral over ℝ of a Nonnegative Continuous Function as the Limit of Its Riemann Integrals over [−n, n]
lemmalem:improper-integral-continuous-nonnegative-2026aAnalysisOn a compact interval, the Lebesgue integral over ℝ of a function times the indicator of the interval is the Riemann integral of its restriction, when that restriction is continuous. For a nonnegative continuous function on ℝ, the Lebesgue integral is the supremum, and for an int…The Borel Sets of ℝⁿ, Lebesgue Measure on ℝⁿ and Integrals against It Are Predicative in the Dimension
helperhlp:lebesgue-measure-rn-predicative-2026aAnalysisThe conditions that a set is the Borel σ-algebra of ℝⁿ, that a set is Lebesgue measure on ℝⁿ, and that a number is the integral of a nonnegative measurable function against Lebesgue measure on ℝⁿ, are expressed by predicative formulas in which the dimension n is a variable; so in…A Random Vector Is Gaussian with Mean m and Covariance Σ Exactly When Its Law Is N(m,Σ)
corollarycor:gaussian-law-characterization-2026aProbabilityA random vector in d-space is Gaussian with mean m and covariance matrix Σ if and only if its law is the Gaussian law N(m,Σ).Convergence in Distribution through Expectations of Bounded Continuous and of Bounded Lipschitz Functions
lemmalem:convergence-distribution-expectations-2026aProbabilityRandom elements of a metric space, possibly on different probability spaces, converge in distribution exactly when the expectations of every bounded continuous function of them converge, and exactly when this holds for every bounded Lipschitz function.- For a real p at least 1, a sequence of random vectors in R^k converges in L^p to a random vector when the expected p-th power of the Euclidean norm of their difference tends to zero.
Almost Sure Convergence of Random Elements of a Metric Space
definitiondef:almost-sure-convergence-2026aProbabilityA sequence of random elements of a metric space converges almost surely to a random element when, outside an event of probability zero, the sequence of values converges to the value of the limit.Standard Normal Vectors and the Standard Normal Distribution on ℝᵏ
definitiondef:standard-normal-vector-2026bProbabilityDefines the standard normal density and distribution on k-dimensional space, and calls a random vector standard normal when its coordinates are independent standard normal random variables.The Boundary of a Subset of a Metric Space Is Closed and Borel
lemmalem:boundary-metric-2026aAnalysisTopologyThe boundary of any subset of a metric space is closed in the metric topology, hence a Borel set.- The boundary of a subset of a metric space is its closure minus its interior.
A Compact Subset of a Metric Space as a Metric Space: Compactness, Local Compactness, Separability, Continuous Functions and Finite Borel Measures
lemmalem:compact-subset-metric-subspace-2026aAnalysisTopologyA compact subset of a metric space, with the restricted metric, is a compact, locally compact and separable metric space on which every continuous function has compact support; finite Borel measures pass between the subset and the whole space by restriction and by extension by ze…The Central Limit Theorem for Independent Identically Distributed Square-Integrable Random Variables
theoremthm:central-limit-lindeberg-2026aProbabilityFor an iid sequence of square-integrable random variables with mean mu and positive variance sigma^2, the normalized partial sums (S_n - n mu)/(sigma sqrt n) converge in distribution to a standard normal random variable.- Standing notation for results on Gaussian random vectors: the Gaussian constant, the standard normal densities and laws on R and R^k, standard normal and Gaussian random vectors, and the Gaussian laws N(m, Sigma).
- N(m, Sigma) is the common law of all Gaussian random vectors with mean m and covariance matrix Sigma.
The Law of a Gaussian Random Vector Is Determined by Its Mean and Covariance Matrix
theoremthm:gaussian-law-mean-covariance-2026aProbabilityA Gaussian random vector X with mean m and nonzero covariance matrix BB^T, B^T B invertible, equals m + BW almost surely for the standard normal vector W = (B^T B)^{-1} B^T (X - m), a function of X; hence two Gaussian vectors with the same mean and covariance have the same law, a…A Nonzero Positive Semidefinite Matrix Factors as BBᵀ with BᵀB Invertible
lemmalem:psd-full-rank-factorization-2026aLinear AlgebraEvery nonzero symmetric positive semidefinite d x d matrix Sigma equals B B^T for some d x r matrix B with r at most d whose Gram matrix B^T B is invertible.