Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Removal Form of the Shared-Clock Insertion Response: Discrepancy on the Enlarged Clock Family, the Base-Clock Insertion Count, and the Linearisation Defect Along Either Path
lemmalem:insertion-response-removal-form-2026aAnalysisProbabilityAdopt the setting, notation and data of Shared-Clock Point Insertion into the Open-Loop Aggregate Solution: Exact Response Identity, Crude Bound, and Linearisation Defect, with the sole exception of its discrepancy hypothesis (D), which is not assumed here: the natural numbers…Weighted Cauchy-Schwarz Inequality on a Measure Space and the Symmetrised Score Functional: Bounds and Averaging
lemmalem:symmetrised-score-averaging-2026aAnalysisProbabilityLet be a natural number and let be a point of the Euclidean space , with , where is the absolute value and sums over are the finite sums of the real numbers. Points of…Sum of a Nonnegative Function over an Arbitrary Set
definitiondef:sum-nonnegative-function-over-set-2026aAnalysisSet TheoryLet be a set and let be a function with values in the nonnegative real numbers. For a nonempty finite subset , denotes the sum over the finite index set of the restriction of to , and …Gaussian Smoothing of a Finitely Supported Probability Mass Function: Density Bounds and Control of the Directional Score Integral by the Move Information
lemmalem:discrete-smoothing-score-bound-2026aAnalysisProbabilityStatisticsLet be a natural number, let be a real number with , and let , , , and (for ) be as in…The Gaussian Smoothing Weight: Normalization, Derivatives, Exponential Tilting, Moments, and First-Order Remainder
lemmalem:gaussian-smoothing-weight-2026aAnalysisProbabilityLet be a natural number, let be Euclidean space with the Euclidean norm , the dot product , and the Euclidean distance , and let be Lebesgue measure on the Borel -algebra . Let…Asymptotic Lower Bound for the Recentred N-Agent Cost by the Fluctuation LQG Value, under Law-Transported Injection Certificates
theoremthm:n-agent-cost-lqg-lower-bound-2026cAnalysisProbabilityAdopt the common data, the family of solutions, the standing hypotheses, hypotheses (I), (I) and (CB), the notion of an admissible parameter vector, and the real number of the asymptotic lower bound theorem: in particular the stationary mean-field triple , the…Adjoint Energy Identity for the Kalman Covariance Riccati Equation
lemmalem:riccati-adjoint-energy-2026aAnalysisLinear AlgebraAdopt the setting and notation of the Kalman covariance Riccati existence theorem: real numbers , a natural number , assignments , and of real matrices with rows and columns to each , all entries continuous in , with every and e…Asymptotic Lower Bound for the Recentred N-Agent Cost without Uniform Control-Moment Hypotheses
theoremthm:n-agent-cost-lower-bound-2026aAnalysisProbabilityCommon data. Fix an affine-controlled transition-rate family on states with compact convex control set and control bound , its transition-rate family with rate bound , an observation-rate family…Ledger Decomposition of the Recentred N-Agent Cost over the Block Cascade and Its Near-Field Filtering Lower Bound
lemmalem:n-agent-cascade-ledger-2026aAnalysisProbabilityAdopt the setting, notation, parameters and standing hypotheses of the tracked energy bound lemma, formed for one and the same data as there. In particular: the affine-controlled transition-rate family on states with compact convex control set…Localized Joint Coercivity of the Recentred N-Agent Cost Integrand under a Positive-Definite Fluctuation Hessian
lemmalem:fluctuation-local-joint-coercivity-2026aAnalysisAdopt the setting and notation of the first-order expansion lemma for the recentred -agent cost: the transition-rate family on states with control set and rate bound ; the observation-rate family ; the horizon…Quadratic Expansion Bounds for the Mean-Field To-Go Value along a Stationary Mean-Field Triple
lemmalem:mean-field-togo-comparison-2026aAnalysisAdopt the setting, hypotheses and notation of the time-shift lemma for the mean-field control problem: the affine-controlled transition-rate family on states — whose control set is nonempty, compact and convex as pa…Time Shift of the Mean-Field Control Problem: Restriction of a Stationary Triple, Cost Splitting, and the Dynamic Programming Principle
lemmalem:mean-field-togo-shift-2026aAnalysisAdopt the setting, hypotheses and notation of the definition of the optimal value, controls and trajectories of the mean-field problem — in particular: the affine-controlled transition-rate family on states with control set…Pointwise-in-Time Tracking of the Mean-Field Flow and Cost along the Realized Control of the Controlled N-Agent Dynamics
lemmalem:n-agent-pathwise-tracking-2026aAnalysisProbabilityAdopt the setting, hypotheses, and notation of the comparison lemma for the -agent system and the mean-field flow: the affine-controlled transition-rate family on states with control set and its transition-rate family…First-Order Expansion of the Mean-Field Cost about a Stationary Mean-Field Triple and Its Quadratic Lower Bound
lemmalem:mean-field-cost-first-order-identity-2026aAnalysisMultivariable CalculusLet , , , with rate bound , with derivative bound , , , with second-derivative bound (the open set of the cost extension, written in that definition, is written here),…Quadratic Growth of the Mean-Field Hamiltonian in the Control along a Stationary Mean-Field Triple
lemmalem:hamiltonian-quadratic-growth-2026aAnalysisMultivariable CalculusLet , , , with rate bound , with derivative bound , , , with second-derivative bound , , and be as in the definition of a stationary mean-field triple (the open set of t…Limits of Penalised Maxima on a Compact Subset of a Metric Space
lemmalem:doubling-limit-compact-metric-2026aAnalysisTopologyFor an upper semicontinuous and a nonnegative lower semicontinuous penalty on a compact set, the penalised maxima decrease to , the penalty vanishes along maximisers, and every cluster point maximises over the z…- Given upper semicontinuous summands on open sets and a test function whose difference with their sum has a local maximum, produces for each symmetric matrices that are admissible second-order test data from above for the summands, with block diagon…
Quadruple Approximable by Test-Function Data
definitiondef:approximable-by-test-data-2026aAnalysisPDEA quadruple of a point, value, vector and symmetric matrix is approximable by test data when it is the limit of data of test functions touching the function from above (or from below) at nearby points.Viscosity Inequalities Pass to Limits of Test-Function Data
lemmalem:viscosity-inequality-limit-test-data-2026bAnalysisPDEIf a second-order equation operator is continuous at a quadruple that is approximable by test data from above for a viscosity subsolution, the subsolution inequality holds at that quadruple; symmetrically from below for a supersolution.The Set of Symmetric Real Matrices is a Metric Space
lemmalem:symmetric-matrix-distance-is-metric-2026aAnalysisTopologyLinear AlgebraLet be a natural number, let be the set of symmetric real matrices, and let be the distance between symmetric real matrices. Then is a metric on , so that…