Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Bench / transport

sogb-004 · public-dev · editorial and formal status separate

Wasserstein symmetry without an optimal plan

Statistical Optimal Transport · natural-language: L3 (author-assigned; calibration pending)

Why this difficulty?

Transport both marginals, preserve cost, and pass from near-optimal plans to an infimum without assuming attainment.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

  • This batch admits no aligned Lean view. The finite-dimensional finite-second-moment specialization, product-coupling cost bound, real-valued interpretation and explanatory boundary statements are reviewed here as mathematics, not as a checked translation of the full QA.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

  • Let E be a finite-dimensional real Euclidean space with its Borel sigma-algebra. Let \(μ,ν\) be probability measures with finite second moments.
  • A coupling \(γ\) has marginals \(μ,ν\). Define \(W_{2}(μ,ν)\) as the infimum of the square root of \(\int \|x-y\|^{2}\) \(dγ\) over such couplings. Do not assume an infimizing coupling is attained.

Natural-language question

Prove symmetry of \(W_{2}\) by swapping coordinates of near-optimal couplings. Which measurability and marginal identities are used, and where does the finite-cost hypothesis prevent an invalid subtraction of infinities?

Reference mathematical proof

  1. The coordinate swap S(x,y)=(y,x) is continuous and hence Borel measurable. For \(γ′=S\#γ\), the identities \(π_{1}\circ S=π_{2}\) and \(π_{2}\circ S=π_{1}\) give marginals \(ν,μ\) by composition of pushforwards.

  2. Nonnegative change of variables and symmetry of the norm give \[\int\|x-y\|^2\,d(S_\#\gamma)=\int\|y-x\|^2\,d\gamma=\int\|x-y\|^2\,d\gamma.\] No signed Fubini theorem is required.

  3. The product coupling has finite quadratic cost since \(\|x-y\|^{2}\le 2\|x\|^{2}+2\|y\|^{2}\). Thus the infimum is finite and, for each \(ε>0\), an admissible coupling can be selected with square-root cost less than \(W_{2}(μ,ν)+ε\). This is near-optimal selection, not an optimal-plan existence theorem.

  4. Swapping this plan gives \(W_{2}(ν,μ)\le W_{2}(μ,ν)+ε\). Let \(ε\) decrease to zero, then interchange \(μ\) and \(ν\) to obtain equality. Finiteness justifies the real-valued \(ε\) argument; there was no operation \(\infty -\infty \). The library also treats an extended-valued generalization, which is not silently identified with this question.

Formal support and missing Lean alignment

Formal support exists for swapping marginals, preserving cost and comparing near-optimal values. No single aligned Lean task for the entire finite-second-moment explanation is admitted in this batch.

Assessment rubric · 4 points
  1. Checks swap measurability and both pushforward marginal identities. (1 point)
  2. Proves nonnegative quadratic-cost preservation. (1 point)
  3. Supplies finite product-coupling cost and near-optimal selection rather than assuming attainment. (1 point)
  4. Passes \(ε\) to zero in both directions without subtracting infinities. (1 point)

Lean view: not yet aligned

Formal support exists for swapping marginals, preserving cost and comparing near-optimal values. No single aligned Lean task for the entire finite-second-moment explanation is admitted in this batch.

This support theorem does not certify the complete QA or its explanatory counterexamples.

What this does—and does not—verify

A supporting formal symmetry theorem is not a verified Lean translation of every sentence of this QA. This question neither proves an optimal coupling exists nor derives the triangle inequality.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original exercise over the existing project-owned coupling-swap route; not copied textbook text.

Exact local source and full context · Locate the owning module (declaration not yet indexed in this graph)

AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSymmetry.wassersteinDistance_comm

ASTIS formal support (not an equivalent QA)

  • AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSymmetry.isCoupling_map_swapPair
  • AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSymmetry.lintegral_quadraticCost_map_swapPair

Mathlib facts / definitions

  • Measure.map_map
  • lintegral_map

Binding SHA-256: 2274ba27f6d700779d832ff90a2b26d881f2bf5f23c3dfc78689f556020559cf