Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A -Displacement Convex Penalty Pair Has a -Monotone Score Along Optimal Couplings
lemmalem:displacement-convex-pair-monotone-2026eAnalysisProbabilityFor a lambda-displacement convex penalty pair and two measures of the score domain, the displacement pairings of the two scores along an optimal coupling and its swap sum to at most minus lambda times the squared Wasserstein distance; at pairs uniquely mapped in both directions t…-Displacement Convexity of a Penalty Pair on the Wasserstein Space
definitiondef:displacement-convex-penalty-pair-2026eAnalysisProbabilityA penalty pair is lambda-displacement convex if, along every optimal coupling from a measure of the score domain to a measure of the penalty domain, the penalty lies above its first-order expansion given by the displacement pairing of the score, plus lambda/2 times the transport…Penalty Pairs on the Wasserstein Space: the Penalty, Its Score, and Their Domains
definitiondef:penalty-pair-wasserstein-2026cAnalysisProbabilityA penalty pair on the Wasserstein space is a penalty domain, a score domain inside it, a real-valued penalty on the former and a score in the tangent space at each point of the latter, such that the score domain is nonempty and dense, the penalty is bounded below by a multiple of…Translations on a Space of Square-Integrable Random Vectors: Constant Classes, Law Invariance, the Translation Derivative and the Translation Hessian
lemmalem:translation-lift-2026aAnalysisProbabilityThe constant classes form a linear isometry of Euclidean space into the space of square-integrable random vectors, so translation by a constant is an isometry of the parameter into that space. For a law-invariant function the translated function depends only on the law; if the fu…The First Marginal of a Probability Measure on a Product: Finite Second Moment, the Wasserstein Contraction, and the Gradient Plan
lemmalem:marginal-wasserstein-2026aAnalysisProbabilityThe first marginal of a probability measure with finite second moment on a product of Euclidean spaces again has finite second moment, at most that of the measure; passing to first marginals does not increase the Wasserstein distance; and pairing the first projection with the fir…Plans and Their Velocity Fields: the Marginal, the Composition Isometry, the Pairing, the Velocity Shift and the Lift
lemmalem:plan-integration-wasserstein-2026aAnalysisProbabilityA plan is a probability measure with finite second moment on a product of two copies of Euclidean space, read as a position with a velocity attached. Its first marginal has finite second moment; composition with the first projection is a linear isometry from the vector fields aga…The Coordinate Fields of a Coupling, and the Second Moment as a Lipschitz Function of the Wasserstein Distance
lemmalem:second-moment-wasserstein-2026aAnalysisProbabilityFor a coupling of two probability measures with finite second moment, the two coordinate projections are square-integrable vector fields against the coupling whose squared norms are the two second moments and whose squared distance is the quadratic cost; consequently the square r…Wasserstein Spaces, Random Vectors, Vector Fields and Symmetric Matrices in Every Dimension: Standing Notation
settingset:wasserstein-viscosity-2026cAnalysisProbabilityStanding notation for second-order equations on the Wasserstein space: probability measures, Wasserstein spaces and spaces of square-integrable random vectors in every dimension, square-integrable vector fields against a measure on one Euclidean space with values in another, and…The Standard Normal Distribution Has Finite Fisher Information, Score Minus the Identity, and Fisher Information One
lemmalem:standard-normal-score-2026aAnalysisProbabilityThe standard normal distribution on the real line is the measure with density exp(-x^2/2)/c with respect to Lebesgue measure, a positive continuously differentiable density whose derivative is -x times the density; it has second moment one, finite Fisher information, score equal…The Lifted Free Score: Norm, Weak Identity and the Second-Moment Identity
lemmalem:free-score-lift-2026aAnalysisProbabilityFor a square-integrable random variable whose law has finite free Fisher information, the lifted free score has squared norm equal to the free Fisher information and pairs with the lifted derivative of a test function to the integral of the difference quotient against the product…Finite Free Fisher Information, the Free Score and the Free Fisher Information of a Probability Measure on the Real Line
definitiondef:free-score-fisher-information-2026aAnalysisProbabilityA probability measure on the real line with finite second moment has finite free Fisher information when the integral, against the product of the measure with itself, of the difference quotient of the derivative of every test function is bounded by a constant times the L^2(mu)-no…One-Dimensional Test Functions: Scalars, Derivatives, and the Difference Quotient of the Derivative
lemmalem:test-function-one-dimensional-2026aAnalysisProbabilityIn dimension one, with the real line identified with R^1, the dot product is the product and the norm the absolute value, the gradient map of a test function is its derivative and its Laplacian its second derivative, both continuous and bounded; the difference quotient of the der…Composition of a Square-Integrable Vector Field with a Random Vector, and the Lifted Score: Isometry, Norm, Weak Identity and Second-Moment Identity
lemmalem:score-lift-2026aAnalysisProbabilityComposing a square-integrable vector field with a random vector of law mu gives a well-defined square-integrable random vector, and this composition is a linear isometry from L^2(mu;R^d) into L^2(Omega;R^d). For a law with finite Fisher information the lifted score has squared no…The Score of a Measure with a Positive Continuously Differentiable Density
lemmalem:score-density-2026aAnalysisProbabilityIf mu has a positive C^1 density m with respect to Lebesgue measure and the vector field grad(m)/m is square-integrable against mu, then integration by parts shows that this field represents minus the integral of the Laplacian on gradients of test functions, so mu has finite Fish…Finite Fisher Information, the Score and the Fisher Information of a Probability Measure
definitiondef:score-fisher-information-2026aAnalysisProbabilityA probability measure with finite second moment has finite Fisher information when the integral of the Laplacian of every test function is bounded by a constant times the L^2(mu)-norm of its gradient (the dual form of the classical condition); its score is then the unique element…Basic Properties of the Tangent Space: Closed Subspace, the Identity Map Belongs to It, Second-Moment Limits, and Representation of Bounded Functionals on Gradients
lemmalem:tangent-space-wasserstein-basic-2026aAnalysisProbabilityThe tangent space at mu is a closed linear subspace of L^2(mu;R^d) in which the gradients of test functions are dense; the identity map lies in it, being the L^2(mu)-limit of the gradients of the second-moment test functions, whose Laplacians integrate to d in the limit; and ever…The Tangent Space of the Wasserstein Space at a Probability Measure
definitiondef:tangent-space-wasserstein-2026aAnalysisProbabilityThe tangent space at a probability measure mu with finite second moment is the closure, in L^2(mu;R^d), of the gradients of test functions.Square-Integrable Vector Fields Against a Probability Measure on Euclidean Space, and Test Functions: Standing Notation
settingset:wasserstein-tangent-2026aAnalysisProbabilityStanding notation for the space L^2(mu;R^d) of square-integrable vector fields on R^d with respect to a Borel probability measure mu, read as the space of square-integrable random vectors on the probability space (R^d, B(R^d), mu), with its inner product, norm, distance, closures…The Gradient of a Test Function is Bounded and Square-Integrable, and Its Laplacian Bounded and Integrable, Against Every Probability Measure
lemmalem:test-function-gradient-integrable-2026aAnalysisProbabilityFor a test function, each partial derivative and the Laplacian are continuous, compactly supported and bounded, so the gradient is a bounded Borel vector field whose squared norm is integrable against every Borel probability measure, and the Laplacian is integrable against every…The Lift of the Second Moment: a Quadratic Function of Class with Gradient 2X and Translation Laplacian 2d
lemmalem:second-moment-lift-2026aAnalysisProbabilityThe lift of the second moment is the squared L^2 norm: a C^2 function on the space of square-integrable random vectors with gradient 2X, Hessian twice the identity form, and translation Laplacian 2d. This is the quadratic function in the explicit solution of the Dyson equation.