Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Comparison and Uniqueness for Free-Energy-Penalised Viscosity Solutions of the Discounted HJB Equation with Free Langevin Noise in a Wall
theoremthm:nc-penalised-comparison-2026aAnalysisProbabilityUnder the structure condition on the Hamiltonian, a bounded weak-star upper semicontinuous penalised subsolution lies below a bounded weak-star lower semicontinuous penalised supersolution on the domain of the wall-confined free energy; solutions are unique there.Maximisers of the Doubled Difference Penalised by the Wall-Confined Free Energy on Bounded Noncommutative Laws
lemmalem:nc-penalised-doubling-maximiser-2026aAnalysisProbabilityFor bounded semicontinuous u and v the doubled difference penalised by the squared distance and the wall-confined free energy attains its maximum, the maximum decreases in the doubling strength with the usual gain, and it tends to the unpenalised supremum as the penalty weight va…Free-Energy-Penalised Viscosity Subsolutions, Supersolutions and Solutions of the Discounted HJB Equation with Free Langevin Noise in a Wall
definitiondef:nc-penalised-viscosity-solution-2026aAnalysisProbabilityA subsolution: at every strict maximum of u minus a test function minus a small multiple of the wall-confined free energy, the law has a score and the equation holds with inequality for every bounded plan superjet, up to an error proportional to the penalty weight; supersolutions…The Discounted Hamilton-Jacobi-Bellman Equation with Free Langevin Noise in a Wall on Noncommutative Laws
equationeq:nc-free-langevin-hjb-2026aAnalysisProbabilityThe discounted HJB equation with free Langevin noise confined by a wall, in score form: the discount term plus the Hamiltonian at the plan plus half the squared noise intensity times the pairing of the score with the momentum.The Discounted Hamilton-Jacobi-Bellman Equation with Free Langevin Noise in a Wall on Noncommutative Laws: Standing Notation
settingset:nc-free-langevin-hjb-2026aAnalysisProbabilityStanding notation for the discounted HJB equation with free Langevin noise in a wall: plan jets on square-integrable laws, the pairings, the discount rate, noise intensity and wall radius, the wall-confined free energy of a free entropy penalty, and the Hamiltonian.Plan Jets of Squared Wasserstein Distances at an Optimal Coupling of Bounded Noncommutative Laws
lemmalem:nc-squared-distance-plan-jets-2026aAnalysisProbabilityAt an optimal coupling of two bounded laws, the law of the position with the doubling momentum is a plan superjet of the squared distance to the second law and, with shared momentum, a plan subjet of minus the squared distance from the first; the score pairings reduce to pairings…Weak-Star Semicontinuity on Bounded Laws of Functions on Square-Integrable Noncommutative Laws
definitiondef:nc-weak-star-semicontinuous-2026aAnalysisProbabilityA function on square-integrable noncommutative laws is weak-star upper (lower) semicontinuous on bounded laws if its values at the images of bounded laws are upper (lower) semicontinuous along weak-star convergent sequences with a common norm bound.The Wall-Confined Free Energy: Norm Bound, Lower Bound, Weak-Star Compact Sublevel Sets and Displacement Monotonicity of the Score
lemmalem:nc-wall-confined-free-energy-2026aAnalysisProbabilityThe wall-confined free energy lives on laws with norm bound R, is bounded below, has weak-star compact sublevel sets on which it is lower semicontinuous, and has a score that is displacement monotone along optimal couplings.The Wall-Confined Free Energy and Its Score
definitiondef:nc-wall-confined-free-energy-2026aAnalysisProbabilityThe wall-confined free energy is a free entropy penalty plus the wall energy of radius R; its score, defined where the conjugate variables and the wall force exist, is the wall force minus the conjugate variables.The Conjugate Variables of a Free Entropy Penalty are Displacement Monotone along Optimal Couplings
lemmalem:nc-free-entropy-penalty-monotone-2026aAnalysisProbabilityAdding the tangent inequalities of a free entropy penalty at the two ends of an optimal coupling shows that the conjugate variables are displacement monotone (decreasing) along it.Free Entropy Penalties: Displacement Convexity with Minus the Conjugate Variables as Gradient
definitiondef:nc-free-entropy-penalty-2026aAnalysisProbabilityA free entropy penalty is a real function on a set of noncommutative laws, bounded below on norm balls, with weak-star closed sublevel sets, satisfying the tangent inequality along optimal couplings with gradient minus the conjugate variables.The Wall Energy: Finiteness Forces the Norm Bound, Closed Sublevel Sets, and Monotonicity of the Wall Force along Couplings
lemmalem:nc-wall-energy-2026aAnalysisProbabilityLaws of finite wall energy have norm bound R and nonnegative energy; sublevel sets of the wall energy are weak-star closed; and the wall force is monotone along every coupling.The Wall Energy of a Given Radius and the Wall Force of a Noncommutative Law
definitiondef:nc-wall-energy-2026aAnalysisProbabilityDefines the wall energy of radius R of a noncommutative law as the series of its even moments scaled by powers of R, its finiteness domain, and the wall force as the limit in the GNS space of the differentiated partial sums.Monotonicity of Odd Powers under a Tracial State
lemmalem:nc-odd-power-trace-monotone-2026aAnalysisProbabilityFor self-adjoint noncommutative polynomials a and b and an odd power n, a tracial state takes a real nonnegative value on the product of a^n - b^n with a - b.Marginal Isometries, Bounded Plans and Displacement Pairings for Noncommutative Laws
definitiondef:nc-marginal-pairings-2026aAnalysisProbabilityFixes the isometries from the GNS spaces of the two marginals into that of a joint law, bounded plans with their momentum norm, and the pairings of GNS vectors with the momentum of a plan and with the displacement of a coupling.The Free Difference Quotient and the Conjugate Variables of a Noncommutative Law
definitiondef:nc-conjugate-variables-2026aAnalysisProbabilityDefines the free difference quotient of a noncommutative law as a linear functional on polynomials, and the conjugate variables as the vectors of the GNS space that represent these functionals.Uniqueness of a Continuous Viscosity Solution of the Mean-Field Control Equation on the Torus
corollarycor:torus-control-uniqueness-2026aProbabilityPDEFor the control Hamiltonian of a control datum, a continuous viscosity subsolution lies below a continuous viscosity supersolution, so the mean-field control equation has at most one continuous viscosity solution.The Discounted Hamilton-Jacobi-Bellman Equation of Mean-Field Control with Idiosyncratic Noise on the Torus
equationeq:torus-control-hjb-2026aProbabilityPDEThe discounted Hamilton-Jacobi-Bellman equation on the torus Wasserstein space with the control Hamiltonian of a control datum.The Control Hamiltonian is Continuous Along Couplings and Satisfies the Score-Perturbation Bound and the Structure Condition
lemmalem:torus-control-hamiltonian-conditions-2026aProbabilityPDEThe control Hamiltonian of a control datum satisfies all three conditions of the torus comparison theory, with explicit constants in the score-perturbation bound.Control Data and the Control Hamiltonian on the Torus Wasserstein Space
definitiondef:torus-control-hamiltonian-2026aProbabilityPDEA control datum is a bounded drift and a bounded running cost on the torus that are Lipschitz in the position and the measure. Its control Hamiltonian integrates half the squared momentum minus the drift times the momentum minus the running cost.