Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- 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.Locally Lipschitz Function on an Open Subset of a Metric Space
definitiondef:locally-lipschitz-metric-2026bAnalysisDefines a real-valued function on an open subset of a metric space to be locally Lipschitz when each point has an open ball in the subset on which the function satisfies a Lipschitz bound.- A metric space has interpolation points if any two points x, y have, for each t in [0,1], a point at distance at most t d(x,y) from x and at most (1-t) d(x,y) from y.
The Noncommutative Wasserstein Distance Satisfies the Triangle Inequality and is a Metric on Noncommutative Laws
theoremthm:nc-wasserstein-triangle-2026aAnalysisProbabilityThe noncommutative quadratic Wasserstein distance satisfies the triangle inequality, so it is a metric on noncommutative laws and on each set of laws with a common norm bound.Gluing Two Noncommutative Couplings along a Common Marginal
lemmalem:nc-gluing-couplings-2026aAnalysisProbabilityTwo couplings sharing a middle marginal glue to a law of 3d variables with norm bound R whose first two and last two blocks have the given couplings, so its outer blocks couple the outer marginals.The Law of a Tuple of Bounded Self-Adjoint Operators in a Tracial Vector State
lemmalem:nc-law-operator-tuple-2026aAnalysisProbabilityA unit vector and a tuple of self-adjoint operators of norm at most R give a state on noncommutative polynomials with moment bounds R^k; if the vector state is tracial on products of words, this state is a noncommutative law with norm bound R.Evaluation of Noncommutative Polynomials at Bounded Operators: a Unital Homomorphism Compatible with Adjoints, Substitution, Representations and the GNS Multiplication Operators
lemmalem:nc-polynomial-evaluation-operators-2026aAnalysisAlgebraEvaluation at a tuple of bounded operators is a unital algebra homomorphism that respects adjoints for self-adjoint tuples, commutes with substitution and with unital multiplicative linear maps, turns GNS left multiplications into L_p, and obeys the bound R^k on words of length k…Evaluation of Noncommutative Polynomials at a Tuple of Bounded Operators
definitiondef:nc-polynomial-evaluation-operators-2026aAnalysisAlgebraDefines the value p(T) of a noncommutative polynomial at a tuple T of bounded operators on a complex Hilbert space, sending each monomial to the product of the operators along its word.Linear Maps from Noncommutative Polynomials into Bounded Operators: Existence and Uniqueness from Values on Monomials
lemmalem:nc-operator-linear-extension-2026aAnalysisAlgebraAny assignment of bounded operators to words extends uniquely to a linear map from noncommutative polynomials into bounded operators, given by summing over the support of a polynomial in any order.The Amalgamated Free Product of Two Noncommutative Laws over a Common Marginal: Representations, Amalgamation, Freeness and the Tracial Vacuum State
theoremthm:nc-amalgamated-free-product-2026aAnalysisAlgebraThe two tracial algebras act on the amalgamated free product space by unital *-representations that agree on the marginal algebra, alternating products of centred elements applied to the vacuum give the tuple vectors, the vacuum state restricts to the given traces, and it is inva…Cyclic Symmetry of Nested Conditional Expectations over a Common Marginal
lemmalem:nc-nested-expectation-cyclic-2026aAnalysisAlgebraA nested conditional expectation folded from the inside out and the same expression folded from the outside in have the same trace against given elements of the marginal algebra.The Amalgamated Free Product Space: Multilinearity of the Tuple Vectors and the Bounded Left Actions of the Two Tracial Algebras
lemmalem:nc-free-product-actions-2026aAnalysisAlgebraIn the amalgamated free product space the tuple vectors are multilinear and balanced over the marginal algebra, the formal actions are linear, unital and multiplicative up to null vectors and agree on the marginal algebra, and each extends to a bounded operator of norm at most th…The Amalgamated Free Product Space of Two Noncommutative Laws over a Common Marginal, Its Vacuum Vector and Vacuum State
definitiondef:nc-free-product-space-2026aAnalysisAlgebraDefines the amalgamated free product space of two noncommutative laws over a common marginal as the Hilbert completion of the formal space, with its tuple vectors, vacuum vector and vacuum state.The Formal Amalgamated Free Product: the Free Vector Space, Positivity of the Nested-Expectation Form, and Linearity and Formal Adjoints of the Actions
lemmalem:nc-free-product-formal-2026aAnalysisAlgebraThe formal free product space is a complex vector space, the nested-expectation form is Hermitian and positive semidefinite (via positive Gram operators and their square roots), and the formal actions are linear with formal adjoints.