Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-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 Euclidean quadratic Wasserstein space

Definition

For an integer d≥1, let Rd have its Euclidean norm and Borel sigma-algebra. Define P2(Rd) to be the Borel probability measures μ with ∫∣x∣2 dμ(x)<∞. A coupling of μ,ν∈P2(Rd) is a Borel probability measure π on Rd×Rd whose first and second coordinate marginals are μ and ν; write Γ(μ,ν) for the set of couplings. Define W2(μ,ν)=(inf⁡π∈Γ(μ,ν)∫Rd×Rd∣x−y∣2 dπ(x,y))1/2.

Facts & Assumptions

Given: An integer d≥1 and μ,ν∈P2(Rd).

[F2]

For a nonnegative function on a product probability space, Tonelli identifies its integral with either iterated integral; ∣x−y∣2≤2∣x∣2+2∣y∣2. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product Expectation of a nonnegative or integrable random variable

Proof

1.1givenF1

The product law μ⊗ν is a Borel probability on Rd×Rd with marginals μ,ν by [F1], so it belongs to Γ(μ,ν). Thus the coupling set in the definition is nonempty.

2.1givenF1F2step 1.1∎

By the inequality in [F2] and the finite second moments of μ,ν, Tonelli gives ∫∣x−y∣2d(μ⊗ν)≤2∫∣x∣2dμ+2∫∣y∣2dν<∞. All coupling costs are nonnegative, so their infimum is finite and nonnegative; its square root in the displayed definition is therefore a finite real number.

Depends on

Used by

Dependency tree · two levels

34 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