ConditionalMeanApproximation

Abstract

Conditional-mean atomization converges weakly to the original compactly supported law and preserves convex order simultaneously for each pair. The final approximation theorem supplies equal positive cardinalities, uniform weights, interval membership of all atoms, and both weak limits.

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.

Theorem 1.1 (condMeanAtomize_tendsto).

$$\forall \{ab:\mathbb{R}\}\{\mu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}(n:\mathbb{N})\mapsto (\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{condMeanAtomize}\mu (n+1)(\mathrm{Nat}.\mathrm{succpos}n)).\mathrm{toProbDist})\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\mu )$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/ConditionalMeanApproximation.condMeanAtomize_tendsto (✓ 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 conditional-mean finite laws with n plus one bins converge weakly to the original compactly supported probability law.

Theorem 1.2 (condMeanAtomize_convexOrder).

$$\forall \{ab:\mathbb{R}\}\{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mathrm{ConvexOrderOnIcc}ab\mu \nu \to \forall (n:\mathbb{N})(\mathrm{hn}:0<n),(\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{condMeanAtomize}\mu n\mathrm{hn}).\mathrm{ConvexOrder}(\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{condMeanAtomize}\nu n\mathrm{hn})$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/ConditionalMeanApproximation.condMeanAtomize_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.

Applying the same positive bin count to both members of an interval convex-order pair preserves finite-law convex order.

Theorem 1.3 (exists_discrete_approximation).

$$\forall \{ab:\mathbb{R}\}\{\mu \nu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mathrm{ConvexOrderOnIcc}ab\mu \nu \to \exists (pq:\mathbb{N}\to \mathrm{DiscreteLaw}),(\forall (n:\mathbb{N}),(pn).\mathrm{ConvexOrder}(qn))\wedge (\forall (n:\mathbb{N}),0<(pn).n)\wedge (\forall (n:\mathbb{N}),(pn).n=(qn).n)\wedge (\forall (n:\mathbb{N})(i:\mathrm{Fin}(pn).n),(pn).\mathrm{weight}i=1/\mathrm{coe}(pn).n)\wedge (\forall (n:\mathbb{N})(j:\mathrm{Fin}(qn).n),(qn).\mathrm{weight}j=1/\mathrm{coe}(qn).n)\wedge (\forall (n:\mathbb{N})(i:\mathrm{Fin}(pn).n),(pn).\mathrm{atom}i\in \mathrm{Set}.\mathrm{Icc}ab)\wedge (\forall (n:\mathbb{N})(j:\mathrm{Fin}(qn).n),(qn).\mathrm{atom}j\in \mathrm{Set}.\mathrm{Icc}ab)\wedge \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}n\mapsto (pn).\mathrm{toProbDist})\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\mu )\wedge \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}n\mapsto (qn).\mathrm{toProbDist})\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\nu )$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/ConditionalMeanApproximation.exists_discrete_approximation (✓ 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 compact convex-order pair admits paired finite approximations in convex order with positive equal cardinalities, equal weights, all atoms in the interval, and both prescribed weak limits.

References

• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanApproximation.condMeanAtomize_convexOrder
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanApproximation.condMeanAtomize_tendsto
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanApproximation.exists_discrete_approximation
• Dependency: D5/S3/Analytic/Probability/ConditionalMeanAtoms