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

Bench / transport

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

What information does a coupling contain?

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

Why this difficulty?

Identify the two marginal constraints and distinguish a feasible coupling from an optimal one.

Editorial review and exact formal-coverage boundary

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

  • The complete explanatory QA has no aligned Lean view. The rectangle-language interpretation, general discussion of dependence and distinction between feasibility and cost optimality are prose-reviewed here; no optimal-plan or metric certification is claimed.

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

Assumptions and conventions

  • \(μ,ν\) are Borel probability measures on \(\mathbb{R}^{d}\). A candidate joint measure \(γ\) is defined on \(\mathbb{R}^{d}\times \mathbb{R}^{d}\). No transport cost function or independence assumption is imposed on a general coupling.

Natural-language question

State the two marginal identities that make \(γ\) a coupling of \(μ\) and \(ν\). Is independence part of the definition? Identify a canonical feasible coupling and explain why feasibility alone does not mean optimality.

Reference mathematical proof

  1. For every Borel A,B, the marginal constraints are \[\begin{gathered}\gamma(A\times\mathbb R^d)=\mu(A),\\\gamma(\mathbb R^d\times B)=\nu(B).\end{gathered}\] Equivalently the coordinate pushforwards are \(μ\) and \(ν\).

  2. A coupling specifies a joint law with these marginals; it need not be independent. Correlation is allowed as long as the marginal constraints remain satisfied.

  3. The independent product is a canonical feasible coupling: \[(\mu\otimes\nu)(A\times B)=\mu(A)\nu(B).\] Its marginals use the total masses equal to one.

  4. Optimality requires a specified cost and a comparison of its integral over feasible plans. No optimality follows from the marginal identities alone.

Formal support and missing Lean alignment

The local coupling definition and product-coupling theorem support the stated concepts. No equivalent Lean task for the entire explanation is admitted.

Assessment rubric · 4 points
  1. States both marginal identities with the correct coordinate order. (1 point)
  2. Does not assume independence for every coupling. (1 point)
  3. Identifies the product measure as a feasible probability coupling. (1 point)
  4. Distinguishes feasibility from cost optimality. (1 point)

Lean view: not yet aligned

The local coupling definition and product-coupling theorem support the stated concepts. No equivalent Lean task for the entire explanation is admitted.

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

What this does—and does not—verify

No existence of an optimal plan, uniqueness, or Wasserstein metric theorem is asserted.

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 coupling-definition exercise over the local transport foundation.

Exact local source and full context · Locate the existing Lean declaration

AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isCoupling_prod

ASTIS formal support (not an equivalent QA)

    Mathlib facts / definitions

      Binding SHA-256: d61f3a0414d8d767ef90fd31733e4fb71d9b47d0f6a62b5844c939a7ee915c7f