Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Scaling a Plan-Jet Viscosity Subsolution of an Equation with a Quadratic Hamiltonian Gives a Strict Subsolution
lemmalem:nc-quadratic-hamiltonian-scaling-2026aAnalysisPDEIf u is a plan-jet subsolution for a quadratic Hamiltonian with convex Lipschitz remainder, then theta u with theta<1 satisfies the subsolution inequality with a gain proportional to the squared momentum, up to a small constant.Quadratic Hamiltonians with a Convex Remainder Lipschitz in the Momentum on Phase-Space Noncommutative Laws
definitiondef:nc-quadratic-hamiltonian-2026aAnalysisPDEA Hamiltonian is quadratic with a convex Lipschitz remainder if it is one half the squared momentum plus a remainder that is convex and Lipschitz with linear growth in the momentum and bounded above at zero momentum.Lifts of Functions on Square-Integrable Noncommutative Laws to Square-Integrable Tuples
definitiondef:nc-law-function-lift-2026aAnalysisPDEThe lift of a function on square-integrable noncommutative laws to a tracial W*-probability space: evaluate the function at the law of the tuple.Comparison and Uniqueness for the Linear-Quadratic Hamilton-Jacobi Equation on Square-Integrable Noncommutative Laws
corollarycor:nc-lq-comparison-2026aAnalysisPDEComparison for bounded semicontinuous plan-jet sub- and supersolutions of the linear-quadratic equation, and uniqueness of bounded continuous plan-jet viscosity solutions.The Linear-Quadratic Hamiltonian: Its Lift, the Structure Condition and Its Quadratic Structure
lemmalem:nc-lq-hamiltonian-conditions-2026aAnalysisPDEWith bounded Lipschitz drift coefficients and a bounded uniformly continuous running cost, the linear-quadratic Hamiltonian lifts to the expected formula, satisfies the structure condition, and is quadratic with a convex Lipschitz remainder.The Linear-Quadratic Hamilton-Jacobi Equation with Law-Dependent Affine Drift on Square-Integrable Noncommutative Laws
equationeq:nc-lq-hamilton-jacobi-2026aAnalysisPDEThe linear-quadratic Hamiltonian, one half the squared momentum minus the pairing with a law-dependent affine drift minus a running cost, and its discounted Hamilton-Jacobi equation on noncommutative laws.Comparison Principle for Plan-Jet Viscosity Solutions of the Discounted Hamilton-Jacobi Equation on Square-Integrable Noncommutative Laws
theoremthm:nc-plan-comparison-2026aAnalysisPDEFor a Hamiltonian satisfying the Crandall-Ishii-Lions structure condition that is either Lipschitz in the momentum with linear growth or quadratic with a convex Lipschitz remainder, every bounded usc plan-jet subsolution lies below every bounded lsc plan-jet supersolution.Plan Jets at an Ekeland Point of the Doubled Difference with Logarithmic Confinement on Square-Integrable Noncommutative Laws
lemmalem:nc-plan-doubling-jets-2026aAnalysisPDEAt an Ekeland point of the doubled difference over joint laws, with a logarithmic confinement, the shared doubling momentum gives plan superjets of the first function and plan subjets of the second; the confinement momenta are small, and the doubling distance is controlled by the…Test Functions and Plan Jets: Touching Transfers Plan Jets, and the Jet Form of Plan-Jet Viscosity Solutions
lemmalem:nc-plan-viscosity-jets-2026aAnalysisPDETouching transfers plan jets from the test function to the function, so plan-jet viscosity solutions can be tested equivalently on the plan jets of the function itself.Plan-Jet Viscosity Subsolutions, Supersolutions and Solutions of the Discounted Hamilton-Jacobi Equation on Square-Integrable Noncommutative Laws
definitiondef:nc-plan-viscosity-solution-2026aAnalysisPDEPlan-jet viscosity sub- and supersolutions: whenever a test function touches from above (below) and has a plan super- (sub-)differential with slack, the equation holds as an inequality up to a momentum perturbation of the size of the slack.The Discounted Stationary Hamilton-Jacobi Equation on Square-Integrable Noncommutative Laws
equationeq:nc-discounted-hamilton-jacobi-2026aAnalysisPDEThe discounted stationary Hamilton-Jacobi equation on square-integrable noncommutative laws, with the Hamiltonian evaluated on the joint law of position and gradient.Hamiltonians on Phase-Space Noncommutative Laws that are Lipschitz in the Momentum with Linear Growth
definitiondef:nc-hamiltonian-momentum-lipschitz-2026aAnalysisPDEA Hamiltonian on phase-space laws is Lipschitz in the momentum with linear growth if changing the momentum by Q changes it by at most a constant times one plus the position norm times the norm of Q.The Structure Condition for a Hamiltonian on Phase-Space Noncommutative Laws
definitiondef:nc-hamiltonian-structure-condition-2026aAnalysisPDEThe structure condition of Crandall-Ishii-Lions on phase-space laws, local in the positions: at the doubling momentum alpha(X-Y), moving the base point from X to Y raises the Hamiltonian by little when alpha|X-Y|^2+|X-Y| is small.Plan Superdifferentials, Plan Subdifferentials and Plan Jets with Slack on Square-Integrable Noncommutative Laws
definitiondef:nc-plan-jets-2026aAnalysisPDEA plan is a plan superdifferential (subdifferential) of a function on laws, with slack, if the first-order upper (lower) expansion along the momentum holds uniformly over every tuple jointly realised with the plan; the plan jets are the sets of these.- A plan at a law is a joint law of position and momentum whose first marginal is that law.
Plan Jets and Hamiltonians on Square-Integrable Noncommutative Laws: Standing Notation
settingset:nc-plan-jets-2026aAnalysisPDEStanding notation for plan jets and Hamiltonians on square-integrable noncommutative laws: tuple sums and pairing, lifts of functions on laws to tuples, and the metrics used.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…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…