Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Basic Properties of the Legendre-Fenchel Conjugate: the Fenchel-Young Inequality, Convexity, Full Domain under Superlinear Growth, and the Quadratic
lemmalem:legendre-fenchel-conjugate-basic-rn-2026aAnalysisThe conjugate satisfies the Fenchel-Young inequality, has a convex domain on which it is convex whatever f is, is defined everywhere when f grows faster than every linear function, and maps half the squared norm to itself.The Legendre-Fenchel Conjugate of a Real Function on a Subset of Euclidean Space
definitiondef:legendre-fenchel-conjugate-rn-2026aAnalysisFor a real function f on a nonempty subset C of Euclidean space, the conjugate is defined at every p for which p.x - f(x) is bounded above on C, and there equals its supremum.Sequential Banach-Alaoglu Theorem: Bounded Sequences in the Dual of a Separable Real Normed Space Have Weak-Star Convergent Subsequences
theoremthm:banach-alaoglu-sequential-2026aAnalysisIn the dual of a separable real normed space, every sequence bounded in the dual norm by M has a subsequence converging weak-star to a functional of dual norm at most M.The Dual of a Real Normed Space is a Real Banach Space, and the Dual Norm is the Least Bound
lemmalem:dual-space-basic-2026aAnalysisThe bounded linear functionals on a real normed space form a real vector space under pointwise operations; the dual norm is the least nonnegative bound of a functional, is a norm, and makes the dual a Banach space. Weak-star limits are unique, and norm convergence implies weak-st…Weak-Star Convergence in the Dual of a Real Normed Space
definitiondef:weak-star-convergence-dual-2026aAnalysisA sequence of bounded linear functionals on a real normed space converges weak-star to a bounded linear functional when it converges to it at every vector.The Dual Space of a Real Normed Space and the Dual Norm
definitiondef:dual-space-real-normed-2026aAnalysisThe dual of a real normed space is the set of bounded linear functionals on it, with pointwise addition and scalar multiplication, and the dual norm of a functional is the greatest lower bound of its nonnegative bounds.Mean-Field Limit of the N-Particle Dyson Game: the Value per Particle Converges to the Solution of the Dyson Hamilton-Jacobi Equation on the Wasserstein Space
theoremthm:dyson-n-particle-mean-field-limit-2026aAnalysisProbabilityPDEFor N particles on the line with logarithmic repulsion beta/(2(N-1)), a confining potential, idiosyncratic noise sigma^2/(N-1) below the collision threshold sigma^2 < beta and mean-field running cost, the solution of the N-particle Hamilton-Jacobi equation divided by N converges,…The Half-Relaxed Limits of the Regularised N-Particle Dyson Solutions are Viscosity Sub- and Supersolutions of the Limit Dyson Equation up to a Cost Defect
propositionprop:dyson-half-relaxed-limits-viscosity-2026aAnalysisProbabilityPDEThe upper half-relaxed limit of the sup-convolved N-particle Dyson solutions divided by N is a viscosity subsolution, and the lower half-relaxed limit of the inf-convolved ones a viscosity supersolution, of the Dyson Hamilton-Jacobi equation on the Wasserstein space without commo…Gibbs Maximisers for the Regularised N-Particle Dyson Solutions Tested at a Local Extremum: Energy Bound, Concentration and the Score Identity
lemmalem:dyson-localised-gibbs-concentration-2026aAnalysisProbabilityPDEAt a point where the half-relaxed limit minus the penalty is locally dominated by a linear function plus a small multiple of the distance, the Gibbs maximisers of the regularised N-particle solution minus N times the quadratic block test function minus the penalty have bounded en…Half-Relaxed Limits of the Sup- and Inf-Convolved N-Particle Dyson Solutions: Bounds, Continuity and Limits along Configurations of Bounded Energy
lemmalem:dyson-regularised-half-relaxed-limits-2026aAnalysisProbabilityPDERegularise the N-particle Dyson solution v_N by a sup-convolution and an inf-convolution with wall weight 1/N and fixed parameter tau. The upper and lower half-relaxed limits of the regularised solutions divided by N are bounded, satisfy an explicit W2 modulus on the finite-energ…Upper and Lower Half-Relaxed Limits along Empirical Measures of Functions on the Weyl Chambers
definitiondef:empirical-half-relaxed-limits-2026aAnalysisProbabilityFor functions f_N on the Weyl chambers of linear growth in N, the upper half-relaxed limit at a measure of finite confined logarithmic energy is the infimum, over radii and starting indices, of the supremum of f_N(x)/N over all later N and all configurations x whose empirical mea…The Mean-Field Limit of the Relative Score of Laws of Dyson Particles Concentrating at a Measure
lemmalem:dyson-particle-score-limit-2026aAnalysisProbabilityIf laws of N Dyson particles have relative scores with bounded Fisher term per particle and their empirical measures concentrate in W2 at a measure of finite confined logarithmic energy, then that measure has a score in the confined logarithmic-energy pair, the particle scores pa…The Discrete Dyson Energy per Particle: Bounds, Compactness with a Lower Limit, and Recovery Configurations with Separated Particles
lemmalem:dyson-discrete-energy-limits-2026aAnalysisProbabilityThe N-particle Dyson potential divided by N controls the second moment of the empirical measure; configurations of bounded energy per particle have empirical measures converging in W2 along a subsequence to a measure of finite confined logarithmic energy, which is at most the low…Quantile Blocks of an Atomless Measure on the Line: Block Maps, Distances to Ordered Empirical Measures, and the Block Test Function
lemmalem:quantile-blocks-line-2026aAnalysisProbabilityAn atomless measure on the line is cut into N ordered blocks of mass 1/N. The block map of an ordered configuration pushes the measure to its empirical measure and is optimal against every monotone transport of the measure, which gives the Wasserstein distance of ordered empirica…The N-Particle Dyson Game and its Mean-Field Limit: Standing Data and Equations
settingset:dyson-n-particle-2026aAnalysisProbabilityPDEStanding data for the mean-field limit of the N-particle Dyson game: interaction beta, noise sigma with sigma^2 < beta, a confining potential V, a discount lambda and a bounded uniformly continuous cost g; the N-particle Hamilton-Jacobi equation on the Weyl chamber with its solut…The N-Particle Dyson Hamilton-Jacobi Equation with a Mean-Field Running Cost
equationeq:dyson-n-particle-hamilton-jacobi-2026aAnalysisProbabilityPDEThe Hamilton-Jacobi equation of N controlled particles on the Weyl chamber with logarithmic repulsion of strength beta/(2(N-1)), confinement V, idiosyncratic noise of intensity sigma^2/(N-1), quadratic control cost and running cost N times a function of the empirical measure.Gradient Maps of a Function on an Open Subset of Euclidean Space
definitiondef:gradient-map-euclidean-2026bAnalysisA gradient map of a real function on an open subset of Euclidean space is a Borel vector field on the whole space that agrees with the gradient of the function at every point of the open set outside a Lebesgue-null set, the function being differentiable there.Gibbs Maximisers of the Relative Free Energy: the Variational Principle and the Relative Score
lemmalem:gibbs-maximiser-relative-free-energy-euclidean-2026bAnalysisProbabilityFor a convex open D, a penalty U on D with monotone gradient and Gibbs-integrable tails, a temperature a>0, and a semiconvex f bounded above with |Df|^2 <= A + B(U - min U), the Gibbs measure pi_f with density proportional to exp((f-U)/a) on D lies in the domain of the relative f…The N-Particle Dyson Potential on the Weyl Chamber: Penalty, Monotone Gradient, Dissipation with Constants Uniform in N, and Gibbs Integrability
lemmalem:dyson-n-particle-data-weyl-chamber-2026aAnalysisPDEFor a confining potential V on the line and sigma^2 < beta, the N-particle Dyson potential P_N = H_{b_N} + sum V(x_k) with b_N = beta/(2(N-1)) is a penalty on the Weyl chamber with monotone gradient, satisfies the dissipation inequality with noise kappa_N = sigma^2/(N-1), epsilon…Integrating a Semiconvex Viscosity Subsolution of the Penalty-Drift Equation against a Measure of Finite Relative Fisher Information
lemmalem:semiconvex-subsolution-weak-form-euclidean-2026aAnalysisProbabilityPDEFor bounded w on an open convex D with |Dw|^2 <= A + B(U - p0), the a.e. gradient of a continuous w is Borel and square-integrable against measures of finite relative free energy. A semiconvex viscosity subsolution of the penalty-drift operator satisfies, for every mu of finite r…