Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Wasserstein Estimates for Affine Push-Forwards, First and Quadratic Moments, and the Cost of a Joint Law
lemmalem:nc-affine-moments-wasserstein-2026aAnalysisAffine substitutions are Lipschitz for the noncommutative Wasserstein distance, first moments and the root second moment are 1-Lipschitz, quadratic moments are Lipschitz on bounded sets, so all of them preserve Cauchy sequences; the cost of a joint law dominates the squared dista…Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data
lemmalem:nc-affine-substitution-basic-2026aAnalysisAffine substitutions map laws to laws and compose like the affine data; the first and quadratic moments of a law are real, symmetric and positive semidefinite, they transform by explicit formulas, and the coordinate data give the marginals, the diagonal and the cost.Affine Data and Affine Substitutions of Noncommutative Polynomials
definitiondef:nc-affine-substitution-2026aAnalysisAn affine datum is a real coefficient matrix with a real shift; it defines a tuple of self-adjoint polynomials of degree at most one, hence a substitution, together with a norm, composites, identities and the marginal, difference and diagonal data.The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It
theoremthm:metric-completion-2026aAnalysisTopologyThe metric completion is a complete metric space into which the canonical map is an isometry with dense image; a map into a complete metric space that preserves Cauchy sequences extends uniquely, continuously and with the same Lipschitz constant.- The metric completion is the set of classes of Cauchy sequences under vanishing limit distance, with the limit distance, and the canonical map sends a point to the class of its constant sequence.
Cauchy Sequences in a Metric Space: Constant Sequences, Convergence of Termwise Distances, the Null Relation, and Independence of Representatives
lemmalem:cauchy-sequences-metric-2026aAnalysisTopologyFor Cauchy sequences in a metric space the termwise distances converge; the limit distance is a pseudometric, and vanishing limit distance is an equivalence relation compatible with it.Well-Posedness of the Eikonal and Discounted Hopf-Lax Equations on Noncommutative Laws with Distance Data
corollarycor:nc-eikonal-discounted-well-posed-2026aAnalysisPDEOn the space of noncommutative laws with a norm bound and the Wasserstein distance, the distance to a weak-star closed target set is the unique slope-based solution of the eikonal equation vanishing on the target, and a multiple of its square is the unique bounded solution of a d…The Noncommutative Laws with a Norm Bound Form a Complete Bounded Metric Space with Interpolation Points
theoremthm:nc-laws-complete-metric-2026aAnalysisProbabilityThe tracial states with norm bound R, with the noncommutative Wasserstein distance, form a complete and bounded metric space in which displacement interpolants are interpolation points.Moments of Noncommutative Laws are Lipschitz in the Wasserstein Distance
lemmalem:nc-moments-wasserstein-lipschitz-2026aAnalysisProbabilityOn laws with a norm bound, each moment is a Lipschitz function of the noncommutative Wasserstein distance; hence Wasserstein convergence implies weak-star convergence and sequentially weak-star closed sets are Wasserstein closed.Distance Functions Give Explicit Slope-Based Solutions of the Eikonal and Discounted Hopf-Lax Equations
propositionprop:distance-slope-solutions-metric-2026aAnalysisPDEIn a metric space with interpolation points, the distance to a nonempty set K solves the eikonal equation with right-hand side 1 off K, and a suitable multiple of its square solves the discounted Hopf-Lax equation with right-hand side a multiple of the squared distance.Comparison Principle for Slope-Based Solutions of the Discounted Hopf-Lax Equation on a Complete Metric Space with Interpolation Points
theoremthm:comparison-discounted-hopf-lax-metric-2026aAnalysisPDEOn a complete metric space with interpolation points, a bounded s-subsolution lies below a bounded s-supersolution of the discounted equation rho u + |grad u|^2/2 = f when f is uniformly continuous.Comparison Principle for Slope-Based Solutions of the Eikonal Equation on a Complete Metric Space with Interpolation Points
theoremthm:comparison-eikonal-metric-2026aAnalysisPDEOn a complete metric space with interpolation points, a bounded s-subsolution lies below a bounded s-supersolution of the eikonal equation off a set K, when the right-hand side is uniformly continuous and bounded below by a positive constant and the two are ordered uniformly near…The Discounted Stationary Hopf-Lax Equation on an Open Subset of a Metric Space
equationeq:discounted-hopf-lax-metric-2026aAnalysisPDENames the discounted stationary equation rho u + (1/2)|grad u|^2 = f on an open subset of a metric space, as the slope-based equation of the Hamiltonian rho r + p^2/2 - f(x).- Names the metric eikonal equation |grad u| = f on an open subset of a metric space, as the slope-based equation of the Hamiltonian p - f(x).
Slope-Based Viscosity Solutions on a Metric Space: Standing Notation
settingset:metric-slope-viscosity-2026aAnalysisPDEStanding notation for slope-based viscosity solutions on a metric space: balls, distance to a set, semicontinuity, local slopes, test classes, Hamiltonians and s-solutions, with the basic slope lemma and Ekeland's principle in force.Ekeland's Variational Principle for Upper Semicontinuous Functions on a Complete Metric Space
theoremthm:ekeland-variational-principle-metric-2026aAnalysisAn upper semicontinuous function bounded above on a complete metric space has, near any almost-maximiser, a point that strictly maximises the function minus a small multiple of the distance to that point.Elementary Properties of Local Slopes: Order, Negation, Bounds from Difference Quotients, Lipschitz Functions and Squared Distances
lemmalem:local-slopes-basic-metric-2026aAnalysisCollects the elementary facts about local slopes used in slope-based viscosity theory: ordering and negation of the slopes, upper and lower bounds from difference quotients, slopes of Lipschitz functions, and the squared distance to a point as a test function in a space with inte…Slope-Based Viscosity Subsolutions, Supersolutions and Solutions on a Metric Space
definitiondef:slope-viscosity-solution-metric-2026aAnalysisPDEDefines Hamiltonians nondecreasing in the slope variable and the slope-based (Gangbo-Swiech) viscosity sub- and supersolutions of H = 0 on an open subset of a metric space, tested by a function of a test class plus a locally Lipschitz perturbation.Test Classes for Slope-Based Viscosity Solutions on a Metric Space
definitiondef:slope-test-classes-metric-2026aAnalysisDefines the two test classes of slope-based viscosity solutions: locally Lipschitz functions with continuous local slope equal to their sub-slope, respectively to their super-slope.Local Slope, Super-Slope, Sub-Slope and Upper Slope Envelope of a Locally Lipschitz Function on a Metric Space
definitiondef:local-slopes-metric-2026aAnalysisDefines the local slope of a locally Lipschitz function on an open subset of a metric space as the limit superior of its difference quotients, its one-sided variants from the positive and negative parts of the increments, and the upper envelope of the slope.