Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Boundedness, Lower Semicontinuity and Attainment of the Mean-Field Cost
theoremthm:mean-field-cost-lsc-attainment-2026bAnalysisProbabilityAdopt the setting and notation of the mean-field cost of a control from an initial state: the affine-controlled transition-rate family on states with control set , the horizon , the population cost data ,…The Mean-Field Cost of a Control from an Initial State
definitiondef:mean-field-control-cost-2026bAnalysisProbabilityLet be an affine-controlled transition-rate family on states with control set , let be the probability simplex, let be a real number, and let be population cost data on states with cont…Sequential Characterization of Lower Semicontinuity on a Subset of a Metric Space
lemmalem:lsc-sequential-characterization-2026aAnalysisTopologyLet be a metric space, let , and let be the restriction of to , a metric on by claim 1 of The Restriction of a Metric to a Subset Induces the Subspace Topology. Let be the set of real numbers with the addition and the order…Stability of the Mean-Field Flow under Perturbation of the Initial State and Weak Convergence of Controls
lemmalem:mean-field-flow-stability-2026cAnalysisProbabilityLet be an affine-controlled transition-rate family on states with control set and Lipschitz constant , let be its transition-rate family, and adopt from that lemma the real numbers , , and…Integrals of Functions Vanishing or Agreeing off a Null Set on a Compact Interval
lemmalem:integral-null-set-interval-2026aAnalysisLet be real numbers with and adopt the notation and of the restricted Lebesgue measure space on a compact interval, so that is a measure space by claim 1 there. Measurability of a re…- Let be a metric space, and let be the collection of subsets of that are open in , which is a topology on by The Open Subsets of a Metric Space Form a Topology. We say that is separable if there is a countable subset t…
Borel Sets and Measurable Maps in a Separable Metric Space
lemmalem:separable-metric-borel-toolkit-2026aAnalysisTopologyProbabilityLet be the set of rational numbers and let be the set of those with . Let be a measurable space. Call a pair a separable metric datum when is a metric space and is a non…- Let be a metric space and let be the collection of subsets of that are open in , a topology on by The Open Subsets of a Metric Space Form a Topology. Then the following hold. 1. (Separability.) If is totally bounded in , then th…
Coordinatewise Convergence, Sequential Compactness and Density in a Product Metric Space
lemmalem:product-metric-sequential-2026aAnalysisTopologyLet and be metric spaces, let be the Cartesian product of the underlying sets, and let be the product metric, which is a metric by claim 1 of The Product Metric is a Metric. Let denote the natural numbers. Write…Euclidean Points as Tuples of Real Numbers
lemmalem:euclidean-points-are-tuples-2026aSet TheoryMultivariable CalculusLet be a natural number, let be the initial segment determined by , and let be the set of real numbers. Euclidean space is introduced there as the set of all ordered -tuples with each , the term…Convergence, Limits and the Cauchy Condition for Real Sequences Agree with Those in the Real Line as a Metric Space, which is Complete
lemmalem:real-sequence-frameworks-agree-2026bAnalysisTopologyFor a sequence of real numbers, convergence, the limit and the Cauchy condition mean the same in the real numbers and in the real line with the metric |s - t|; and the real line is a complete metric space.Weak Sequential Compactness of Borel Measures of Total Mass One on a Compact Metric Space
theoremthm:weak-sequential-compactness-measures-compact-metric-2026aAnalysisTopologyProbabilityLet be a metric space, let be the collection of subsets of that are open in , which is a topology on by The Open Subsets of a Metric Space Form a Topology, and assume that is compact in . Let denote the…Riesz-Markov Representation Theorem on a Compact Metric Space
theoremthm:riesz-markov-compact-metric-2026aAnalysisTopologyLet be a metric space with nonempty, let be the collection of subsets of that are open in , which is a topology on by The Open Subsets of a Metric Space Form a Topology, and assume that is compact in . Let…A Countable Uniformly Dense Family of Lipschitz Functions on a Compact Metric Space
lemmalem:continuous-uniform-dense-compact-2026aAnalysisTopologyLet be a metric space with nonempty, and let be the collection of subsets of that are open in , which is a topology on by The Open Subsets of a Metric Space Form a Topology. Assume that is compact in . Let…The Convolution of a Continuous Function with a Continuous Kernel is Continuous
lemmalem:convolution-continuous-2026aAnalysisLet , , , , , the set and the convolution be as in Convolution of a Continuous Function with a Compactly Supported Continuous Kernel, and let denote the Euclidean distance. Then is…Continuous Partition of Unity Subordinate to a Finite Open Cover of a Compact Set in a Metric Space
lemmalem:partition-of-unity-compact-metric-2026aAnalysisTopologyLet be a metric space, and let be the collection of subsets of that are open in , which is a topology on by The Open Subsets of a Metric Space Form a Topology. Let denote the real numbers, with the addition, multiplication, iden…Convolution of a Continuous Function with a Compactly Supported Continuous Kernel
definitiondef:convolution-2026aAnalysisLet be a natural number, let be the Euclidean norm on Euclidean space , let denote the Euclidean distance, a metric on each Euclidean space, and let be Lebesgue measure on the Borel -algebra of .…The Convolution Integrand is Continuous, Compactly Supported and Integrable
lemmalem:convolution-integrand-2026aAnalysisLet be a natural number, let be the Euclidean norm on Euclidean space , let denote the Euclidean distance, a metric on each Euclidean space, and let be Lebesgue measure on the Borel -algebra…- Let be a natural number, let be the Euclidean norm on Euclidean space and let be the Euclidean distance, a metric on ; write for the closed ball of centre and radius in . Let…
A Continuous Compactly Supported Function on is Uniformly Continuous
lemmalem:continuous-compact-support-uniformly-continuous-2026aAnalysisTopologyLet be a natural number, let be the Euclidean norm on , and let denote the Euclidean distance, a metric on each Euclidean space. Let be continuous on , as a map from …