Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Calculus of the Free Fock Space: Orthonormal Monomials, Adjoints, Commutation Relations and the Vacuum
lemmalem:nc-free-fock-space-2026aAnalysisProbabilityMonomials are orthonormal in the free Fock space, annihilation operators are the adjoints of creation operators, left and right operators commute up to the vacuum projection, and the left and right semicircular operators are bounded, self-adjoint and commute; formulas for the vac…The Free Fock Space: Creation, Annihilation and Semicircular Operators
definitiondef:nc-free-fock-space-2026aAnalysisProbabilityThe free Fock space is the completion of the noncommutative polynomials in which the monomials are orthonormal; creation operators multiply by a variable on the left or right, and annihilation operators strip a leading or trailing letter.Comparison and Uniqueness for the Linear-Quadratic HJB Equation with Free Langevin Noise in a Wall on Noncommutative Laws
corollarycor:nc-free-langevin-lq-comparison-2026aAnalysisProbabilityFor bounded Lipschitz drift coefficients and a bounded uniformly continuous running cost, penalised sub- and supersolutions of the linear-quadratic equation compare on the domain of the wall-confined free energy, and solutions are unique there.The Linear-Quadratic Hamilton-Jacobi-Bellman Equation with Free Langevin Noise in a Wall on Noncommutative Laws
equationeq:nc-free-langevin-lq-hjb-2026aAnalysisProbabilityThe discounted HJB equation with free Langevin noise in a wall, with the linear-quadratic Hamiltonian with law-dependent affine drift.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.