ConditionalMeanAtoms

Abstract

The atom in each equal-probability quantile bin is the conditional mean of that bin. Compact support keeps every atom inside the same closed interval. The construction is increasing, preserves the original mean, and identifies finite prefix sums with lower integrated quantiles.

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

$$\forall (\mu :\mathrm{ProbDist}\mathbb{R})(n:\mathbb{N})(\mathrm{hn}:0<n)(k:\mathrm{Fin}n),\mathrm{condMeanAtom}\mu n\mathrm{hn}k=n\cdot \int (u:\mathbb{R})\mathrm{in}\mathrm{Set}.\mathrm{Ioc}(k/n)((k+1)/n),\mu .\mathrm{toMeasure}.\mathrm{quantile}u$$

Formalization. D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtom (✓ std3).

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

Commentary.

Each atom is n times the integral of the generalized inverse over its equal-probability quantile bin, with right-closed left-open endpoints.

Definition 1.2 (condMeanAtomize).

$$\forall (\mu :\mathrm{ProbDist}\mathbb{R})(n:\mathbb{N})(\mathrm{hn}:0<n),\mathrm{condMeanAtomize}\mu n\mathrm{hn}=\mathrm{DiscreteLaw}.\mathrm{uniform}n\mathrm{hn}(\mathrm{fun}(k:\mathrm{Fin}n)\mapsto \mathrm{condMeanAtom}\mu n\mathrm{hn}k)$$

Formalization. D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtomize (✓ 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 atoms form an equal-weight finite law.

Lemma 1.3 (integrableOn_quantile_bin).

$$\forall \{ab:\mathbb{R}\}\{\mu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \forall \{n:\mathbb{N}\},0<n\to \forall (k:\mathrm{Fin}n),\mathrm{MeasureTheory}.\mathrm{IntegrableOn}(\mathrm{coe}\mu ).\mathrm{quantile}(\mathrm{Set}.\mathrm{Ioc}(\mathrm{coe}\mathrm{coe}k/\mathrm{coe}n)((\mathrm{coe}\mathrm{coe}k+1)/\mathrm{coe}n))\mathrm{MeasureTheory}.\mathrm{volume}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/ConditionalMeanAtoms.integrableOn_quantile_bin (✓ 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 concentration makes the generalized inverse integrable over every positive-cardinality quantile bin.

Lemma 1.4 (condMeanAtom_mem_Icc).

$$\forall \{ab:\mathbb{R}\}\{\mu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \forall (n:\mathbb{N})(\mathrm{hn}:0<n)(k:\mathrm{Fin}n),\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{condMeanAtom}\mu n\mathrm{hn}k\in \mathrm{Set}.\mathrm{Icc}ab$$

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

Every conditional-mean atom remains in the original closed support interval, including a singleton interval.

Lemma 1.5 (condMeanAtom_monotone).

$$\forall \{ab:\mathbb{R}\}\{\mu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \forall \{n:\mathbb{N}\}(\mathrm{hn}:0<n),\mathrm{Monotone}\mathrm{fun}k\mapsto \mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{condMeanAtom}\mu n\mathrm{hn}k$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtom_monotone (✓ 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 means of consecutive quantile bins form an increasing finite vector.

Lemma 1.6 (condMeanAtomize_mean_eq).

$$\forall \{\mu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mathrm{MeasureTheory}.\mathrm{Integrable}(\mathrm{fun}x\mapsto x)\mathrm{coe}\mu \to \forall (n:\mathbb{N})(\mathrm{hn}:0<n),(\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{condMeanAtomize}\mu n\mathrm{hn}).\mathrm{mean}=\mu .\mathrm{expect}\mathrm{id}$$

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

Conditional-mean atomization preserves the original mean whenever the original coordinate is integrable.

Lemma 1.7 (condMeanAtomize_partial_sum_eq).

$$\forall \{ab:\mathbb{R}\}\{\mu :\mathrm{Econlib}.\mathrm{Probability}.\mathrm{ProbDist}\mathbb{R}\},\mu .\mathrm{supportsOn}(\mathrm{Set}.\mathrm{Icc}ab)\to \forall \{n:\mathbb{N}\}(\mathrm{hn}:0<n)(K:\mathrm{Fin}n),\sum i\mathrm{with}\mathrm{coe}i\le \mathrm{coe}K,\mathrm{Econlib}.\mathrm{Probability}.\mathrm{DiscreteLaw}.\mathrm{condMeanAtom}\mu n\mathrm{hn}i=\mathrm{coe}n\cdot \int (u:\mathbb{R})\mathrm{in}\mathrm{Set}.\mathrm{Ioc}0((\mathrm{coe}\mathrm{coe}K+1)/\mathrm{coe}n),(\mathrm{coe}\mu ).\mathrm{quantile}u$$

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

Every lower prefix sum of conditional-mean atoms is n times the integrated quantile up to the end of that prefix.

References

• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtom
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtom_mem_Icc
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtom_monotone
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtomize
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtomize_mean_eq
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanAtoms.condMeanAtomize_partial_sum_eq
• Truth anchor: D5/S3/Analytic/Probability/ConditionalMeanAtoms.integrableOn_quantile_bin
• Dependency: D5/S3/Analytic/Probability/CompactConvexOrder
• Dependency: D5/S3/Analytic/Probability/CompactQuantile
• Dependency: D5/S3/Analytic/Probability/FiniteMartingaleCoupling