FiniteMartingaleCoupling

Abstract

Finite laws have arbitrary nonnegative weights summing to one, including repeated atoms and zero weights. A transition matrix produces one genuine joint probability measure with both exact marginals and every bounded measurable martingale test. Uniform finite laws in convex order admit such a matrix and coupling. The coupling predicate reuses CostTransport.IsCoupling from the frozen optimal-transport library.

The construction of Daniel Lyng in Econlib revision d7bd9477476cade1c6695c8891746048ceddc52f is adapted under Apache-2.0. Apache-2.0 license: docs/reports/licenses/econlib-strassen/LICENSE.txt. Strassen (1965) provides the historical martingale-transport context. In formulas, coe denotes the canonical coercion, dmu the integration measure, iUnion indexed union, smul scalar multiplication, and ae almost everywhere. Namespace-qualified Lean names and interval constructors retain their mathematical meaning; separated identifier words denote the corresponding underscored Lean constant.

Definition 1.1 (IsCoupling).

$$\forall \{\alpha :\mathrm{Type}u\}\{\beta :\mathrm{Type}v\}[\mathrm{MeasurableSpace}\alpha ][\mathrm{MeasurableSpace}\beta ](\mu :\mathrm{ProbDist}\alpha )(\nu :\mathrm{ProbDist}\beta )(\pi :\mathrm{ProbDist}(\alpha \times \beta )),\mathrm{IsCoupling}\mu \nu \pi ⟺\mathrm{CostTransport}.\mathrm{IsCoupling}\pi .\mathrm{toMeasure}\mu .\mathrm{toMeasure}\nu .\mathrm{toMeasure}$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.IsCoupling (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

An actual joint law is a coupling exactly when its two pushforward measures are the specified marginals. This predicate is the existing general measure coupling predicate specialized to probability laws.

Lemma 1.2 (fst_probability_marginal).

$$\forall \{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsCoupling}\mu \nu \pi \to \pi .\mathrm{map}\mathrm{Prod}.\mathrm{fst}\mathrm{measurablefst}=\mu$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.fst_probability_marginal (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The first probability-law pushforward agrees with the first specified marginal.

Lemma 1.3 (snd_probability_marginal).

$$\forall \{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsCoupling}\mu \nu \pi \to \pi .\mathrm{map}\mathrm{Prod}.\mathrm{snd}\mathrm{measurablesnd}=\nu$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.snd_probability_marginal (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The second probability-law pushforward agrees with the second specified marginal.

Lemma 1.4 (supportsOn_Icc_prod).

$$\forall \{ab:\mathbb{R}\}\{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsCoupling}\mu \nu \pi \to \mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \nu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \mathrm{coe}\pi (\mathrm{Set}.\mathrm{Icc}ab\times \mathrm{set}\mathrm{Set}.\mathrm{Icc}ab)=1$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.supportsOn_Icc_prod (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

A genuine coupling of two laws concentrated on the same closed interval is concentrated on its Cartesian square.

Definition 1.5 (IsMartingaleCoupling).

$$\forall (\mu \nu :\mathrm{ProbDist}\mathbb{R})(\pi :\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})),\mathrm{IsMartingaleCoupling}\mu \nu \pi ⟺(\pi .\mathrm{map}\mathrm{Prod}.\mathrm{fst}\mathrm{measurablefst}=\mu \wedge \pi .\mathrm{map}\mathrm{Prod}.\mathrm{snd}\mathrm{measurablesnd}=\nu \wedge \mathrm{MeasureTheory}.\mathrm{Integrable}\mathrm{Prod}.\mathrm{fst}\pi .\mathrm{toMeasure}\wedge \mathrm{MeasureTheory}.\mathrm{Integrable}\mathrm{Prod}.\mathrm{snd}\pi .\mathrm{toMeasure}\wedge \forall (\phi :\mathbb{R}\to \mathbb{R}),\mathrm{Measurable}\phi \to (\exists (M:\mathbb{R}),\forall (x:\mathbb{R}),|\phi x|\le M)\to \int (p:\mathbb{R}\times \mathbb{R}),(p.2-p.1)\cdot \phi p.1\mathrm{dmu}\pi .\mathrm{toMeasure}=0)$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.IsMartingaleCoupling (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

A tested martingale coupling has both exact marginals, integrable real coordinates, and vanishing displacement integral against every globally bounded measurable function of its first coordinate.

Lemma 1.6 (fst_measure).

$$\forall \{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}\mu \nu \pi \to (\mathrm{coe}\pi ).\mathrm{fst}=\mathrm{coe}\mu$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.fst_measure (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The first measure marginal of a tested martingale coupling is the first specified law.

Lemma 1.7 (snd_measure).

$$\forall \{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}\mu \nu \pi \to (\mathrm{coe}\pi ).\mathrm{snd}=\mathrm{coe}\nu$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.snd_measure (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The second measure marginal of a tested martingale coupling is the second specified law.

Lemma 1.8 (marginal_mean_eq).

$$\forall \{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}\mu \nu \pi \to \mu .\mathrm{expect}\mathrm{id}=\nu .\mathrm{expect}\mathrm{id}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.marginal_mean_eq (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The two marginal means of a tested martingale coupling are equal.

Lemma 1.9 (convex_expect_le).

$$\forall \{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}\mu \nu \pi \to \forall \{ab:\mathbb{R}\},\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \nu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \forall (\phi :\mathbb{R}\to \mathbb{R}),\mathrm{ConvexOn}\mathbb{R}(\mathrm{Set}.\mathrm{Icc}ab)\phi \to \mathrm{ContinuousOn}\phi (\mathrm{Set}.\mathrm{Icc}ab)\to \mu .\mathrm{expect}\phi \le \nu .\mathrm{expect}\phi$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.convex_expect_le (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

Conditional Jensen gives the convex-test inequality using only convexity and continuity on the common compact interval.

Definition 1.10 (DiscreteLaw).

$$\mathrm{DiscreteLaw}=\{(n:\mathbb{N}),(\mathrm{atom}:\mathrm{Fin}n\to \mathbb{R}),(\mathrm{weight}:\mathrm{Fin}n\to \mathbb{R})|(\forall (i:\mathrm{Fin}n),0\le \mathrm{weight}i)\wedge \sum (i:\mathrm{Fin}n),\mathrm{weight}i=1\}$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.DiscreteLaw (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

A finite real law consists of a natural cardinality, real atoms, and nonnegative real weights of total one. Zero weights and repeated atoms are allowed.

Definition 1.11 (toProbDist).

$$\forall (p:\mathrm{DiscreteLaw}),p.\mathrm{toProbDist}.\mathrm{toMeasure}=\sum (i:\mathrm{Fin}p.n),\mathrm{ENNReal}.\mathrm{ofReal}(p.\mathrm{weight}i)\mathrm{smul}\mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{dirac}(p.\mathrm{atom}i)$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toProbDist (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

Finite weighted Dirac sums define genuine native probability laws; for a transition matrix the joint atom weights are the first-law weights multiplied by the transition entries.

Lemma 1.12 (toProbDist_toMeasure).

$$\forall (p:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}),\mathrm{coe}p.\mathrm{toProbDist}=\sum i,\mathrm{ENNReal}.\mathrm{ofReal}(p.\mathrm{weight}i)\mathrm{smul}\mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{dirac}(p.\mathrm{atom}i)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toProbDist_toMeasure (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The underlying measure is the finite sum of weighted Dirac measures, with real nonnegative weights converted to ENNReal.

Lemma 1.13 (toProbDist_supportsOn_of_atoms_mem).

$$\forall (p:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw})\{s:\mathrm{Set}\mathbb{R}\},\mathrm{MeasurableSet}s\to (\forall (i:\mathrm{Fin}p.n),p.\mathrm{atom}i\in s)\to p.\mathrm{toProbDist}.\mathrm{supportsOn}s$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toProbDist_supportsOn_of_atoms_mem (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

If every listed atom belongs to a measurable set, the finite probability law assigns that set mass one.

Definition 1.14 (mean).

$$\forall (p:\mathrm{DiscreteLaw}),p.\mathrm{mean}=\sum (i:\mathrm{Fin}p.n),p.\mathrm{weight}i\cdot p.\mathrm{atom}i$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.mean (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The mean of a finite law is its weighted sum of atoms.

Definition 1.15 (ConvexOrder).

$$\forall (pq:\mathrm{DiscreteLaw}),p.\mathrm{ConvexOrder}q⟺\forall (\phi :\mathbb{R}\to \mathbb{R}),\mathrm{ConvexOn}\mathbb{R}\mathrm{Set}.\mathrm{univ}\phi \to \sum (i:\mathrm{Fin}p.n),p.\mathrm{weight}i\cdot \phi (p.\mathrm{atom}i)\le \sum (j:\mathrm{Fin}q.n),q.\mathrm{weight}j\cdot \phi (q.\mathrm{atom}j)$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.ConvexOrder (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

Finite-law convex order compares weighted sums of every globally convex real test.

Definition 1.16 (uniform).

$$\forall (n:\mathbb{N})(\mathrm{hn}:0<n)(x:\mathrm{Fin}n\to \mathbb{R}),(\mathrm{uniform}n\mathrm{hn}x).n=n\wedge (\mathrm{uniform}n\mathrm{hn}x).\mathrm{atom}=x\wedge (\mathrm{uniform}n\mathrm{hn}x).\mathrm{weight}=(\mathrm{fun}(i:\mathrm{Fin}n)\mapsto 1/n)$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.uniform (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

A positive finite cardinality and a real vector define the law with equal weights reciprocal to that cardinality.

Lemma 1.17 (uniform_mean).

$$\forall \{n:\mathbb{N}\}(\mathrm{hn}:0<n)(x:\mathrm{Fin}n\to \mathbb{R}),(\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{uniform}n\mathrm{hn}x).\mathrm{mean}=(\sum i,xi)/\mathrm{coe}n$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.uniform_mean (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The mean of an equal-weight finite law is the arithmetic average of its atom vector.

Definition 1.18 (BistochasticMartingaleMatrix).

$$\forall (pq:\mathrm{DiscreteLaw}),\mathrm{BistochasticMartingaleMatrix}pq=\{(T:\mathrm{Fin}p.n\to \mathrm{Fin}q.n\to \mathbb{R})|(\forall (i:\mathrm{Fin}p.n)(j:\mathrm{Fin}q.n),0\le Tij)\wedge (\forall (i:\mathrm{Fin}p.n),p.\mathrm{weight}i\ne 0\to \sum (j:\mathrm{Fin}q.n),Tij=1)\wedge (\forall (i:\mathrm{Fin}p.n),p.\mathrm{weight}i\ne 0\to \sum (j:\mathrm{Fin}q.n),Tij\cdot q.\mathrm{atom}j=p.\mathrm{atom}i)\wedge (\forall (j:\mathrm{Fin}q.n),\sum (i:\mathrm{Fin}p.n),p.\mathrm{weight}i\cdot Tij=q.\mathrm{weight}j)\}$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.BistochasticMartingaleMatrix (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

A transition matrix is nonnegative, has row sum one and the prescribed conditional mean on every positive-weight row, and has the exact weighted column marginal. Zero-weight rows impose no artificial row or mean restriction.

Definition 1.19 (toJointProbDist).

$$\forall \{pq:\mathrm{DiscreteLaw}\}(M:\mathrm{BistochasticMartingaleMatrix}pq),M.\mathrm{toJointProbDist}.\mathrm{toMeasure}=\sum (i:\mathrm{Fin}p.n),\sum (j:\mathrm{Fin}q.n),\mathrm{ENNReal}.\mathrm{ofReal}(p.\mathrm{weight}i\cdot M.Tij)\mathrm{smul}\mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{dirac}(p.\mathrm{atom}i,q.\mathrm{atom}j)$$

Formalization. D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toJointProbDist (✓ std3).

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

Finite weighted Dirac sums define genuine native probability laws; for a transition matrix the joint atom weights are the first-law weights multiplied by the transition entries.

Lemma 1.20 (isMartingaleCoupling).

$$\forall \{pq:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}\}(M:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{BistochasticMartingaleMatrix}pq),\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}p.\mathrm{toProbDist}q.\mathrm{toProbDist}M.\mathrm{toJointProbDist}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.isMartingaleCoupling (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The weighted Dirac joint law built from such a matrix satisfies both actual marginals, coordinate integrability, and every bounded measurable martingale test.

Theorem 1.21 (exists_martingaleCoupling_uniform).

$$\forall (pq:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}),0<p.n\to p.n=q.n\to (\forall (i:\mathrm{Fin}p.n),p.\mathrm{weight}i=1/\mathrm{coe}p.n)\to (\forall (j:\mathrm{Fin}q.n),q.\mathrm{weight}j=1/\mathrm{coe}q.n)\to p.\mathrm{ConvexOrder}q\to \exists (\pi :\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})),\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}p.\mathrm{toProbDist}q.\mathrm{toProbDist}\pi$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/FiniteMartingaleCoupling.exists_martingaleCoupling_uniform (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

Two positive equal-cardinality equal-weight finite laws in convex order have a genuine martingale coupling.

References

• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.BistochasticMartingaleMatrix
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.ConvexOrder
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.DiscreteLaw
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.IsCoupling
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.IsMartingaleCoupling
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.convex_expect_le
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.exists_martingaleCoupling_uniform
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.fst_measure
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.fst_probability_marginal
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.isMartingaleCoupling
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.marginal_mean_eq
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.mean
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.snd_measure
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.snd_probability_marginal
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.supportsOn_Icc_prod
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toJointProbDist
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toProbDist
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toProbDist_supportsOn_of_atoms_mem
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.toProbDist_toMeasure
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.uniform
• Truth anchor: D5/S3/Analytic/Probability/FiniteMartingaleCoupling.uniform_mean
• Dependency: D5/S3/Analytic/Convexity/FiniteMajorization
• Dependency: D5/S3/Analytic/Probability/CompactConvexOrder
• Dependency: D5/S3/Geometry/ProbabilityTransport/CostCoupling