CompactStrassen

Abstract

For arbitrary real endpoints and Borel probability measures of mass one on their closed interval, equal means and every interval-convex interval-continuous test inequality are equivalent to a single joint probability measure with both exact pushforward marginals and native joint-almost-everywhere conditional expectation of the second coordinate given the first equal to the first. Atomic, singular, and singleton laws are included. Empty-interval support premises are impossible. Coordinate integrability follows from compact marginal support. The construction takes a compact weak limit of finite martingale couplings, preserves both marginals, extends continuous tests to every bounded Borel test, then applies native conditional-expectation uniqueness. The native conditional-expectation identity uses the tested martingale law and integrability on the same joint measure.

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.

Lemma 1.1 (tested_martingale_of_weak_limit).

$$\forall \{ab:\mathbb{R}\}\{\mathrm{piSeq}:\mathbb{N}\to \mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\}\{\mathrm{piInf}:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},(\forall (n:\mathbb{N}),\mathrm{coe}(\mathrm{piSeq}n)(\mathrm{Set}.\mathrm{Icc}ab\times \mathrm{set}\mathrm{Set}.\mathrm{Icc}ab)=1)\to \mathrm{coe}\mathrm{piInf}(\mathrm{Set}.\mathrm{Icc}ab\times \mathrm{set}\mathrm{Set}.\mathrm{Icc}ab)=1\to (\forall (n:\mathbb{N})(\phi :\mathbb{R}\to \mathbb{R}),\mathrm{Measurable}\phi \to (\exists M,\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}\mathrm{coe}(\mathrm{piSeq}n)=0)\to \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}n\mapsto \mathrm{piSeq}n)\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\mathrm{piInf})\to \forall (\phi :\mathbb{R}\to \mathbb{R}),\mathrm{Continuous}\phi \to (\exists M,\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}\mathrm{coe}\mathrm{piInf}=0$$

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

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

Commentary.

On one compact square, weak convergence of tested martingale laws preserves the displacement identity for every bounded continuous test of the first coordinate.

Lemma 1.2 (tested_martingale_measurable_of_continuous).

$$\forall \{ab:\mathbb{R}\}\{\pi :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mathrm{coe}\pi (\mathrm{Set}.\mathrm{Icc}ab\times \mathrm{set}\mathrm{Set}.\mathrm{Icc}ab)=1\to \mathrm{MeasureTheory}.\mathrm{Integrable}(\mathrm{fun}p\mapsto p.1)\mathrm{coe}\pi \to \mathrm{MeasureTheory}.\mathrm{Integrable}(\mathrm{fun}p\mapsto p.2)\mathrm{coe}\pi \to (\forall (\phi :\mathbb{R}\to \mathbb{R}),\mathrm{Continuous}\phi \to (\exists M,\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}\mathrm{coe}\pi =0)\to \forall (\phi :\mathbb{R}\to \mathbb{R}),\mathrm{Measurable}\phi \to (\exists M,\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}\mathrm{coe}\pi =0$$

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

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

Commentary.

For a joint law supported on a compact square and with integrable coordinates, vanishing displacement against every bounded continuous first-coordinate test extends to every bounded measurable first-coordinate test.

Theorem 1.3 (martingaleCoupling_of_weak_limit).

$$\forall \{ab:\mathbb{R}\}\{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\mathrm{muSeq}\mathrm{nuSeq}:\mathbb{N}\to \mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{\mathrm{piSeq}:\mathbb{N}\to \mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\}\{\mathrm{piInf}:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}(\mathbb{R}\times \mathbb{R})\},\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \nu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to (\forall (n:\mathbb{N}),\mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}(\mathrm{muSeq}n)(\mathrm{nuSeq}n)(\mathrm{piSeq}n))\to (\forall (n:\mathbb{N}),\mathrm{coe}(\mathrm{piSeq}n)(\mathrm{Set}.\mathrm{Icc}ab\times \mathrm{set}\mathrm{Set}.\mathrm{Icc}ab)=1)\to \mathrm{coe}\mathrm{piInf}(\mathrm{Set}.\mathrm{Icc}ab\times \mathrm{set}\mathrm{Set}.\mathrm{Icc}ab)=1\to \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}n\mapsto \mathrm{piSeq}n)\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\mathrm{piInf})\to \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}n\mapsto \mathrm{muSeq}n)\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\mu )\to \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}n\mapsto \mathrm{nuSeq}n)\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\nu )\to \mathrm{Econlib}.\mathrm{Probability}.\mathrm{IsMartingaleCoupling}\mu \nu \mathrm{piInf}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactStrassen.martingaleCoupling_of_weak_limit (✓ 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 weak limit on the common compact square of genuine tested martingale couplings is again a tested martingale coupling of the two limiting marginals.

Theorem 1.4 (compact_convex_order_iff_martingale).

$$\forall (ab:\mathbb{R})(\mu \nu :\mathrm{MeasureTheory}.\mathrm{ProbabilityMeasure}\mathbb{R}),\mathrm{coe}\mu (\mathrm{Set}.\mathrm{Icc}ab)=1\to \mathrm{coe}\nu (\mathrm{Set}.\mathrm{Icc}ab)=1\to ((\int (x:\mathbb{R}),x\mathrm{dmu}\mathrm{coe}\mu =\int (x:\mathbb{R}),x\mathrm{dmu}\mathrm{coe}\nu \wedge \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 \int (x:\mathbb{R}),\phi x\mathrm{dmu}\mathrm{coe}\mu \le \int (x:\mathbb{R}),\phi x\mathrm{dmu}\mathrm{coe}\nu )⟺\exists (\pi :\mathrm{MeasureTheory}.\mathrm{ProbabilityMeasure}(\mathbb{R}\times \mathbb{R})),\mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{map}\mathrm{Prod}.\mathrm{fst}\mathrm{coe}\pi =\mathrm{coe}\mu \wedge \mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{map}\mathrm{Prod}.\mathrm{snd}\mathrm{coe}\pi =\mathrm{coe}\nu \wedge (\mathrm{coe}\pi )[\mathrm{Prod}.\mathrm{snd}|\mathrm{MeasurableSpace}.\mathrm{comap}\mathrm{Prod}.\mathrm{fst}(\mathrm{borel}\mathbb{R})]=\mathrm{ae}[\mathrm{coe}\pi ]\mathrm{Prod}.\mathrm{fst})$$

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

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

Commentary.

For every pair of compactly concentrated Borel real laws, equal means and all interval-local convex continuous test inequalities are equivalent to existence of one native joint probability law with both exact pushforward marginals and the joint-a.e. conditional-expectation identity. No strict endpoint or regularity assumption on the laws is required.

References

• Truth anchor: D5/S3/Analytic/Probability/CompactStrassen.compact_convex_order_iff_martingale
• Truth anchor: D5/S3/Analytic/Probability/CompactStrassen.martingaleCoupling_of_weak_limit
• Truth anchor: D5/S3/Analytic/Probability/CompactStrassen.tested_martingale_measurable_of_continuous
• Truth anchor: D5/S3/Analytic/Probability/CompactStrassen.tested_martingale_of_weak_limit
• Dependency: D5/S3/Analytic/Probability/ConditionalMeanApproximation
• Dependency: D5/S3/Analytic/Probability/FiniteMartingaleCoupling