CompactConvexOrder

Abstract

Compact interval convex order includes both mass-one support conditions, equality of means, and all tests that are convex and continuous on the interval. No strict endpoint, absolute continuity, or finite-support condition is imposed. Stop-loss comparison gives the lower integrated-quantile inequalities used by conditional-mean discretization.

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 (ProbDist).

$$\forall (\alpha :\mathrm{Type}u)[\mathrm{MeasurableSpace}\alpha ],\mathrm{ProbDist}\alpha =\mathrm{MeasureTheory}.\mathrm{ProbabilityMeasure}\alpha$$

Formalization. D5/S3/Analytic/Probability/CompactConvexOrder.ProbDist (✓ 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 probability-law carrier is the native ProbabilityMeasure, with its original measurable structure.

Definition 1.2 (expect).

$$\forall \{\alpha :\mathrm{Type}u\}[\mathrm{MeasurableSpace}\alpha ](d:\mathrm{ProbDist}\alpha )(f:\alpha \to \mathbb{R}),d.\mathrm{expect}f=\int (x:\alpha ),fx\mathrm{dmu}d.\mathrm{toMeasure}$$

Formalization. D5/S3/Analytic/Probability/CompactConvexOrder.expect (✓ std3).

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

Commentary.

Expectation is the real integral against the measure underlying the probability law.

Definition 1.3 (map).

$$\forall \{\alpha :\mathrm{Type}u\}\{\beta :\mathrm{Type}v\}[\mathrm{MeasurableSpace}\alpha ][\mathrm{MeasurableSpace}\beta ](d:\mathrm{ProbDist}\alpha )(f:\alpha \to \beta )(\mathrm{hf}:\mathrm{Measurable}f),d.\mathrm{map}f\mathrm{hf}=\mathrm{MeasureTheory}.\mathrm{ProbabilityMeasure}.\mathrm{map}df$$

Formalization. D5/S3/Analytic/Probability/CompactConvexOrder.map (✓ 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 measurable map transports the native probability law by pushforward.

Lemma 1.4 (map_toMeasure).

$$\forall \{\alpha :\mathrm{Type}u1\}\{\beta :\mathrm{Type}u2\}[\mathrm{MeasurableSpace}\alpha ][\mathrm{MeasurableSpace}\beta ](d:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\alpha )(f:\alpha \to \beta )(\mathrm{hf}:\mathrm{Measurable}f),\mathrm{coe}(d.\mathrm{map}f\mathrm{hf})=\mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{map}f\mathrm{coe}d$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactConvexOrder.map_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 of a transported probability law is the ordinary measure pushforward.

Lemma 1.5 (expect_map).

$$\forall \{\alpha :\mathrm{Type}u1\}\{\beta :\mathrm{Type}u2\}[\mathrm{MeasurableSpace}\alpha ][\mathrm{MeasurableSpace}\beta ](d:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\alpha )(f:\alpha \to \beta )(\mathrm{hf}:\mathrm{Measurable}f)(g:\beta \to \mathbb{R}),\mathrm{MeasureTheory}.\mathrm{AEStronglyMeasurable}g\mathrm{coe}(d.\mathrm{map}f\mathrm{hf})\to (d.\mathrm{map}f\mathrm{hf}).\mathrm{expect}g=d.\mathrm{expect}\mathrm{fun}x\mapsto g(fx)$$

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

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

Commentary.

Expectation after measurable pushforward equals expectation of the composed test, under the stated almost-everywhere strong measurability condition.

Definition 1.6 (supportsOn).

$$\forall \{\alpha :\mathrm{Type}u\}[\mathrm{MeasurableSpace}\alpha ](d:\mathrm{ProbDist}\alpha )(s:\mathrm{Set}\alpha ),d.\mathrm{supportsOn}s⟺d.\mathrm{toMeasure}s=1$$

Formalization. D5/S3/Analytic/Probability/CompactConvexOrder.supportsOn (✓ std3).

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

Commentary.

Support on a set means that the set has probability one; it does not mean that every point lies in a topological support.

Lemma 1.7 (ae_mem_of_supportsOn).

$$\forall \{d:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{s:\mathrm{Set}\mathbb{R}\},\mathrm{MeasurableSet}s\to d.\mathrm{supportsOn}s\to \forall \mathrm{ae}(x:\mathbb{R})\mathrm{dmu}\mathrm{coe}d,x\in s$$

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

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

Commentary.

Mass one on a measurable set implies membership in that set almost everywhere under the same law.

Lemma 1.8 (integrable_of_supportsOn_Icc).

$$\forall \{d:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{ab:\mathbb{R}\}\{f:\mathbb{R}\to \mathbb{R}\},d.\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \mathrm{ContinuousOn}f(\mathrm{Set}.\mathrm{Icc}ab)\to \mathrm{MeasureTheory}.\mathrm{Integrable}f\mathrm{coe}d$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactConvexOrder.integrable_of_supportsOn_Icc (✓ 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 test continuous on a closed compact interval is integrable under any probability law assigning that interval mass one.

Lemma 1.9 (integrable_id_of_supportsOn_Icc).

$$\forall \{d:\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\}\{ab:\mathbb{R}\},d.\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \mathrm{MeasureTheory}.\mathrm{Integrable}\mathrm{id}\mathrm{coe}d$$

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

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

Commentary.

Compact interval concentration makes the real coordinate integrable.

Definition 1.10 (ConvexOrderOnIcc).

$$\forall (ab:\mathbb{R})(\mu \nu :\mathrm{ProbDist}\mathbb{R}),\mathrm{ConvexOrderOnIcc}ab\mu \nu ⟺(\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\wedge \nu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\wedge \mu .\mathrm{expect}\mathrm{id}=\nu .\mathrm{expect}\mathrm{id}\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 \mu .\mathrm{expect}\phi \le \nu .\mathrm{expect}\phi )$$

Formalization. D5/S3/Analytic/Probability/CompactConvexOrder.ConvexOrderOnIcc (✓ std3).

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

Commentary.

Interval convex order records both mass-one conditions, equality of means, and comparison of every real test convex and continuous on that interval.

Theorem 1.11 (lowerIntegratedQuantile_ge_of_convexOrderOnIcc).

$$\forall \{ab:\mathbb{R}\}\{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mathrm{ConvexOrderOnIcc}ab\mu \nu \to \forall \{t:\mathbb{R}\},t\in \mathrm{Set}.\mathrm{Ioc}01\to \int (u:\mathbb{R})\mathrm{in}\mathrm{Set}.\mathrm{Ioc}0t,(\mathrm{coe}\nu ).\mathrm{quantile}u\le \int (u:\mathbb{R})\mathrm{in}\mathrm{Set}.\mathrm{Ioc}0t,(\mathrm{coe}\mu ).\mathrm{quantile}u$$

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

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

Commentary.

Interval convex order reverses the inequality between lower integrated quantiles at every positive level at most one.

References

• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.ConvexOrderOnIcc
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.ProbDist
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.ae_mem_of_supportsOn
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.expect
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.expect_map
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.integrable_id_of_supportsOn_Icc
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.integrable_of_supportsOn_Icc
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.lowerIntegratedQuantile_ge_of_convexOrderOnIcc
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.map
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.map_toMeasure
• Truth anchor: D5/S3/Analytic/Probability/CompactConvexOrder.supportsOn
• Dependency: D5/S3/Analytic/Convexity/FiniteMajorization
• Dependency: D5/S3/Analytic/Probability/CompactQuantile