Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Mean Value Theorem on a Closed Real Interval and on Any Interval
theoremthm:mean-value-closed-interval-2026bA function continuous on [a,b] and differentiable on (a,b) satisfies f(b)-f(a)=f'(xi)(b-a) for some xi in (a,b); the same holds between any two points of an interval for a function continuous on it and differentiable at the points strictly inside it.- A function continuous on a closed interval [a,b] with a<b, differentiable on (a,b) and taking equal values at a and b has derivative zero at some point of (a,b).
- Let be real numbers with in the order of the ordered field , let be the closed interval determined by and , and let be the set of natural numbers, each being identified with its image in under the…
- A real function continuous on a closed interval [a,b] is bounded and attains a least and a greatest value there.
Restriction Stability of Continuity and of the Derivative
lemmalem:restriction-continuity-derivative-2026bRestricting a function on an interval to a subinterval with at least two points preserves continuity and the derivative at a point, and at a point strictly inside the subinterval differentiability of the restriction gives differentiability of the function with the same derivative…Almost Sure Equality Preserves Square-Integrability and the Mean-Square Norm
lemmalem:almost-sure-equality-square-integrable-2026aLet be a probability space, and let and be random variables on it that are almost surely equal, in the sense that there is an event with such that for every . If …The Twice Continuously Differentiable Extension Determined by Affine-Controlled Rate Data
lemmalem:affine-c2-extension-2026bProbabilityLet be twice continuously differentiable affine-controlled rate data on states with control set and derivative bound , and let be the probability simplex. For each ordered pair with…Twice Continuously Differentiable Affine-Controlled Rate Data
definitiondef:c2-affine-rate-data-2026bProbabilityLet and be natural numbers with and , let be the probability simplex, let be a nonempty subset of Euclidean space that is convex and compact for the topology determined by the Euclidean distance, ca…Conditional-Variance Lower Bound for the Completed-Square Control Energy
lemmalem:fluctuation-conditional-variance-2026aProbabilityAdopt the setting, hypotheses (H1)--(H2), and notation of the completion-of-squares theorem for the fluctuation cost: in particular the fluctuation processes and of a solution of the controlled -agent dynamics about a…Sharp Drift Linearization Error under a Control-Affine Extension
lemmalem:affine-drift-linearization-sharp-2026bProbabilityAdopt the setting of the fluctuation processes of the controlled -agent dynamics: a transition-rate family on states with control set , a nonempty subset of Euclidean space , and rate bound , an observation-rate family ,…- The absolute value of the dot product of two points of R^n is at most the product of their Euclidean norms.
Uniform Convergence in Probability of the N-Agent Empirical State Measure to the Unique Optimal Mean-Field Trajectory
corollarycor:n-agent-trajectory-uniform-convergence-2026cAnalysisProbabilityAdopt the setting, hypotheses and notation of the convergence theorem for the optimal -agent value. In particular: is an affine-controlled transition-rate family on states with control set , with…Convergence of the Optimal N-Agent Value to the Optimal Mean-Field Value and Concentration of Asymptotically Optimal Controls
theoremthm:n-agent-optimal-value-mean-field-limit-2026cAnalysisProbabilityAdopt the setting, hypotheses and notation of the asymptotic lower bound theorem for the -agent cost. In particular: is an affine-controlled transition-rate family on states with control set and…Asymptotic Lower Bound for the N-Agent Cost and Concentration of the Limit Laws on the Optimal Mean-Field Controls
theoremthm:n-agent-cost-liminf-limit-laws-2026cAnalysisProbabilityAdopt the setting, hypotheses and notation of the comparison lemma for the -agent system and the mean-field flow. In particular: is an affine-controlled transition-rate family on states with control set and…Comparison of the N-Agent System with the Mean-Field Flow and Cost along the Realized Control
lemmalem:n-agent-mean-field-comparison-2026cAnalysisProbabilityLet and be natural numbers with and , let be an affine-controlled transition-rate family on states with control set and let be its transition-rate family, with rate bound , aggregat…The Realized Control of the Controlled N-Agent Dynamics as a Random Element of the Control Set
lemmalem:realized-control-random-element-2026cAnalysisProbabilityAdopt the setting of the controlled -agent dynamics: natural numbers , , and ; a nonempty convex subset of Euclidean space , called the control set, which is compact for the topology determined by the…The Simplex, the Control Set and Their Product are Compact Separable Metric Spaces
lemmalem:simplex-control-product-compact-2026aAnalysisTopologyProbabilityLet and be natural numbers with and , and let be a real number. Let be the probability simplex, write for the Euclidean norm, let be the Euclidean distance, a metric by…Control Policy with Values in a Prescribed Subset of Euclidean Space
definitiondef:a-valued-control-policy-2026aProbabilityLet and be natural numbers with and , let be a real number, and let be a nonempty subset of Euclidean space . Let be an observation-driven control policy with horizon , control dimen…Structure of the Optimal Control Set and Separation of Near-Optimal Controls
lemmalem:mean-field-optimal-set-structure-2026bAnalysisProbabilityAdopt the setting, hypotheses and notation of the optimal value, controls and trajectories of the mean-field problem: the initial state , the optimal value , the set of optimal controls, the mean-field flow…The Optimal Value, the Optimal Controls and the Optimal Trajectories of the Mean-Field Problem
definitiondef:mean-field-optimal-solution-set-2026bAnalysisProbabilityAdopt the setting, hypotheses and notation of the boundedness, lower semicontinuity and attainment theorem for the mean-field cost: the affine-controlled transition-rate family on states with control set , the horizo…