Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…Test Functions on Euclidean Space, Their Gradient Maps and Laplacians
definitiondef:test-function-euclidean-2026aAnalysisMultivariable CalculusA test function on R^q is a smooth, compactly supported real-valued function; the set of test functions is written C_c^infty(R^q). The gradient map of a test function sends x to the gradient at x, and its Laplacian is the Laplacian of a C^2 function.Existence of a Smooth Plateau Function on Euclidean Space
lemmalem:smooth-plateau-euclidean-2026aAnalysisMultivariable CalculusFor a centre x0 and radii r < s there is a smooth function on R^q with values in [0,1] that equals 1 on the closed ball of radius r about x0 and vanishes wherever the distance to x0 is at least s. This is the bump-function lemma restated for the current (recursive C^k) notion of…The Difference Quotient of a Function with Bounded Continuous Derivative is Bounded, Symmetric and Continuous on the Plane
lemmalem:difference-quotient-c1-real-2026aAnalysisFor a real function with bounded continuous derivative, the difference quotient extended to the diagonal by the derivative is bounded by the same bound, symmetric, continuous on the plane and hence Borel measurable.Scaled Cutoffs and the Second-Moment Test Functions: Uniform Derivative Bounds and Agreement on a Ball
lemmalem:cutoff-second-moment-test-functions-2026aAnalysisMultivariable CalculusRescaling a smooth bump function by a radius R gives smooth compactly supported cutoffs whose first and second partial derivatives are bounded by constants times 1/R and 1/R^2; multiplying the cutoff by half the squared norm gives smooth compactly supported functions whose gradie…Integration by Parts on Euclidean Space Against a Compactly Supported Function of Class
lemmalem:integration-by-parts-euclidean-2026aAnalysisMultivariable CalculusThe partial derivative of a compactly supported C^1 function on R^q integrates to zero, and consequently the integral of f times a partial derivative of g equals minus the integral of the same partial derivative of f times g whenever f and g are of class C^1 and g is compactly su…