Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Borel -Algebras of Euclidean Space and of the Euclidean Metric Coincide
lemmalem:borel-metric-euclidean-agree-2026aAnalysisTopologyLet be a natural number and let be the Euclidean distance on Euclidean space , which is a metric. Then the Borel -algebra of the metric space and the Borel -algebra…Scaling Lebesgue Measure on ℝⁿ by a Diagonal Matrix
lemmalem:lebesgue-scaling-euclidean-2026bAnalysisAssuming dependent choice, the image of a Borel set of ℝⁿ under an invertible diagonal matrix is Borel, with Lebesgue measure multiplied by the absolute value of the product of the diagonal entries; in particular scaling by c multiplies Lebesgue measure by |c|ⁿ.- Let be a set and let be a function into the real numbers. We say that is bounded if there is a real number with such that for every , the absolute value being that of Absolute Value in an Ordered Field for the ordered…
- Let be a metric space with Borel -algebra . A Borel measure on is a measure on the measurable space .
A Continuous Compactly Supported Function on is Bounded and Integrable
lemmalem:integral-continuous-compact-support-2026aAnalysisLet be a natural number, let denote the Euclidean distance, a metric on each Euclidean space, let be the Euclidean norm on , and let be Lebesgue measure on the Borel -algebra . Topolo…The Integral of an Indicator Function is the Measure of the Set
lemmalem:indicator-integral-measure-2026aAnalysisProbabilityLet be a measure space, with the conventions for given there, and let . Then the indicator function is a nonnegative simple function on , and the integral b…Balls Have Positive Lebesgue Measure and Bounded Sets Have Finite Lebesgue Measure
lemmalem:lebesgue-measure-ball-box-bounds-2026aAnalysisLet be a natural number, let be Lebesgue measure on the Borel -algebra of Euclidean space , and let be the Euclidean distance, a metric on whose open sets form a topology by…Compact Support on Means Vanishing Outside a Bounded Set
lemmalem:compact-support-euclidean-criterion-2026aAnalysisTopologyLet be a natural number, let be the Euclidean norm on Euclidean space , and let be the Euclidean distance, a metric on . By The Open Subsets of a Metric Space Form a Topology the subsets open in fo…Compactly Supported Real-Valued Function
definitiondef:compactly-supported-function-2026aAnalysisTopologyLet be a topological space and let . We say that is compactly supported if its support is a compact subset of .Support of a Real-Valued Function on a Topological Space
definitiondef:support-real-function-topological-2026aAnalysisTopologyLet be a topological space, let be the real numbers, and let . The support of , written , is the closure in of the setConvergence in Distribution to a Constant and Convergence in Probability
lemmalem:convergence-distribution-constant-2026bProbabilityIf random elements of a metric space, possibly on different probability spaces, converge in distribution to a constant c, then for every positive epsilon the probability of being at distance at least epsilon from c tends to zero; on one probability space and a separable metric sp…Lipschitz Test Functions Determine a Finite Borel Measure, and Uniqueness of Weak Limits
lemmalem:weak-limit-unique-2026bAnalysisProbabilityTwo finite Borel measures on a metric space that give the same integral to every Lipschitz function with values in [0,1] are equal; in particular a sequence of finite Borel measures has at most one weak limit.- For Borel probability measures on a metric space, weak convergence is equivalent to convergence of the integrals of bounded Lipschitz functions, to the upper bound for closed sets, to the lower bound for open sets, and to convergence on every set whose boundary is null for the li…
Bounded Lower Semicontinuous Functions are Increasing Limits of Lipschitz Functions
lemmalem:lipschitz-approximation-lsc-2026aAnalysisTopologyLet be a metric space with nonempty, let be a real number with , and let be lower semicontinuous on with for every . For let , where is the canonical map from…Convergence in Distribution of Random Elements of a Metric Space
definitiondef:convergence-in-distribution-metric-2026cProbabilityA sequence of random elements of a metric space, possibly on different probability spaces, converges in distribution when their laws converge weakly to the law of the limit.Weak Convergence of Finite Borel Measures on a Metric Space
definitiondef:weak-convergence-measures-metric-2026cAnalysisProbabilityA sequence of finite Borel measures on a metric space converges weakly to a finite Borel measure when the integrals of every bounded continuous function converge.- The law of a random element of a metric space is the image of the probability measure under it, a probability measure on the Borel sets; two random elements, possibly on different probability spaces, are identically distributed when their laws coincide.
Borel Measurability and Bounded Integration on a Metric Space
lemmalem:borel-metric-toolkit-2026aAnalysisTopologyProbabilityLet be a metric space, let be its topology of open subsets, and let be its Borel -algebra. Measurability of maps between measurable spaces is that of Measurable Map, and the Set of Measurable Maps, and den…A Lipschitz Map is Uniformly Continuous and Continuous
lemmalem:lipschitz-continuous-metric-2026bAnalysisTopologyA Lipschitz map between metric spaces is uniformly continuous, and hence continuous.- A measure is finitely additive, monotone, subtractive on sets of finite measure, countably subadditive, and continuous from below along increasing sequences and from above along decreasing sequences starting at finite measure.