LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The coupling infimum is finite for finite-first-moment probabilities

Statement

If $μ, ν$ are Borel probability measures on $R^{d}$ with finite first moments, then $Π (μ, ν)$ is nonempty and $W_{1} (μ, ν) < \infty$ for the definition in The coupling definition of the 1-Wasserstein distance.

Facts & Assumptions

Given: Borel probability measures $μ, ν$ on $R^{d}$ and $\int ∣ x ∣ d μ, \int ∣ y ∣ d ν < \infty$ .

[F1]

$W_{1}$ is the infimum of the coupling costs over Borel probability couplings with the stated marginals (The coupling definition of the 1-Wasserstein distance).

[F2]

The product of two sigma-finite measures exists and has the prescribed marginal measures (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique); for Euclidean Borel measures this product is a Borel measure on the Euclidean product (The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}).

[F3]

Tonelli's theorem permits iterated integration of nonnegative measurable functions on the product (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F4]

The Euclidean norm satisfies $∣ x - y ∣ \leq ∣ x ∣ + ∣ y ∣$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

Proof

1.1givenF1F2construct

Both probability measures are finite, hence sigma-finite. Their product $μ \otimes ν$ is a Borel probability measure with marginals $μ$ and $ν$ by [F2], so it belongs to $Π (μ, ν)$ by [F1].

2.1F1F3F4step 1.1algebra∎

The Euclidean inequality [F4] and Tonelli [F3], together with the marginals from step 1.1, give $\int ∣ x - y ∣ d (μ \otimes ν) \leq \int ∣ x ∣ d μ + \int ∣ y ∣ d ν < \infty .$ The infimum in [F1] is nonnegative and no larger than this finite coupling cost.

Depends on

Used by

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

François Golse, Mean-Field Limits in Statistical Dynamics, Lecture 1 (standard reference, not scraped)