CompactQuantile

Abstract

The generalized inverse of a real CDF pushes Lebesgue measure on the open unit interval to the original probability measure. Atoms and singular laws are included. The midpoint approximation uses bounded continuous real tests; integration against the quantile is stated for arbitrary normed real vector targets with the declared measurability assumption.

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

$$\forall (\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R})(t:\mathbb{R}),\mu .\mathrm{quantile}t=\mathrm{sInf}\{x:\mathbb{R}|t\le (\mu (\mathrm{Set}.\mathrm{Iic}x)).\mathrm{toReal}\}$$

Formalization. D5/S3/Analytic/Probability/CompactQuantile.quantile (✓ 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 lower generalized inverse of the cumulative distribution function; the infimum convention defines it for every real probability level, while order and transport results use the open unit interval.

Lemma 1.2 (set_nonempty).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ]\{t:\mathbb{R}\},t<1\to \{x|t\le (\mu (\mathrm{Set}.\mathrm{Iic}x)).\mathrm{toReal}\}.\mathrm{Nonempty}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.set_nonempty (✓ 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 probability level below one, some finite right endpoint has cumulative mass at least that level.

Lemma 1.3 (quantile_le_iff).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ]\{t:\mathbb{R}\},t\in \mathrm{Set}.\mathrm{Ioo}01\to \forall \{x:\mathbb{R}\},\mu .\mathrm{quantile}t\le x⟺t\le (\mu (\mathrm{Set}.\mathrm{Iic}x)).\mathrm{toReal}$$

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

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

Commentary.

Inside the open unit interval, the generalized inverse lies below x exactly when the cumulative mass at x reaches the requested probability level.

Lemma 1.4 (monotoneOn_quantile).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ],\mathrm{MonotoneOn}\mu .\mathrm{quantile}(\mathrm{Set}.\mathrm{Ioo}01)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.monotoneOn_quantile (✓ 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 generalized inverse is increasing on the open unit interval.

Lemma 1.5 (aemeasurable_quantile_restrict_Ioo).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ],\mathrm{AEMeasurable}\mu .\mathrm{quantile}(\mathrm{MeasureTheory}.\mathrm{volume}.\mathrm{restrict}(\mathrm{Set}.\mathrm{Ioo}01))$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.aemeasurable_quantile_restrict_Ioo (✓ 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 generalized inverse is almost-everywhere measurable for Lebesgue measure restricted to the open unit interval.

Theorem 1.6 (map_quantile_volume_Ioo).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ],\mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{map}\mu .\mathrm{quantile}(\mathrm{MeasureTheory}.\mathrm{volume}.\mathrm{restrict}(\mathrm{Set}.\mathrm{Ioo}01))=\mu$$

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

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

Commentary.

Pushing Lebesgue probability on the open unit interval through the generalized inverse recovers the entire original law, including its atoms.

Theorem 1.7 (integral_eq_integral_quantile).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ]\{E:\mathrm{Type}u1\}[\mathrm{NormedAddCommGroup}E][\mathrm{NormedSpace}\mathbb{R}E](\phi :\mathbb{R}\to E),\mathrm{MeasureTheory}.\mathrm{AEStronglyMeasurable}\phi \mu \to \int (x:\mathbb{R}),\phi x\mathrm{dmu}\mu =\int (t:\mathbb{R})\mathrm{in}\mathrm{Set}.\mathrm{Ioo}01,\phi (\mu .\mathrm{quantile}t)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.integral_eq_integral_quantile (✓ 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 almost-everywhere strongly measurable function has the same Bochner integral under the original law as its composition with the quantile under unit-interval Lebesgue measure. The target is an arbitrary real normed vector space; no extra integrability premise is inserted.

Definition 1.8 (binMidpoint).

$$\forall (n:\mathbb{N})(t:\mathbb{R}),\mathrm{binMidpoint}nt=(\mathrm{Nat}.\mathrm{floor}(n\cdot t)+1/2)/n$$

Formalization. D5/S3/Analytic/Probability/CompactQuantile.binMidpoint (✓ 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 midpoint of the uniform bin containing t, using the natural-number floor and real division. The definition is total even at n equal to zero.

Lemma 1.9 (bins_pairwise_disjoint).

$$\forall (n:\mathbb{N}),\mathrm{Pairwise}(\mathrm{Function}.\mathrm{onFun}\mathrm{Disjoint}\mathrm{fun}(k:\mathrm{Fin}n)\mapsto \mathrm{Set}.\mathrm{Ico}(\mathrm{coe}\mathrm{coe}k/\mathrm{coe}n)((\mathrm{coe}\mathrm{coe}k+1)/\mathrm{coe}n))$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.bins_pairwise_disjoint (✓ 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 n half-open equal bins indexed by Fin n are pairwise disjoint, including the empty family at n equal to zero.

Lemma 1.10 (iUnion_bins_eq_Ico).

$$\forall (n:\mathbb{N}),1\le n\to \mathrm{iUnion}(k:\mathrm{Fin}n),\mathrm{Set}.\mathrm{Ico}(\mathrm{coe}\mathrm{coe}k/\mathrm{coe}n)((\mathrm{coe}\mathrm{coe}k+1)/\mathrm{coe}n)=\mathrm{Set}.\mathrm{Ico}01$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.iUnion_bins_eq_Ico (✓ 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 positive bin count, the union of the half-open equal bins is precisely the half-open unit interval.

Definition 1.11 (stepFun).

$$\forall (\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R})(\phi :\mathbb{R}\to \mathbb{R})(n:\mathbb{N})(t:\mathbb{R}),\mathrm{stepFun}\mu \phi nt=\phi (\mu .\mathrm{quantile}(\mathrm{binMidpoint}nt))$$

Formalization. D5/S3/Analytic/Probability/CompactQuantile.stepFun (✓ std3).

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

Commentary.

Evaluate the test function at the quantile of the midpoint of the bin containing t.

Lemma 1.12 (countable_not_continuousWithinAt_quantile).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ],\{t|t\in \mathrm{Set}.\mathrm{Ioo}01\wedge \neg \mathrm{ContinuousWithinAt}\mu .\mathrm{quantile}(\mathrm{Set}.\mathrm{Ioo}01)t\}.\mathrm{Countable}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.countable_not_continuousWithinAt_quantile (✓ 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 discontinuity set of the increasing generalized inverse within the open unit interval is countable.

Theorem 1.13 (tendsto_integral_of_quantile_midpoint).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}\mu ](\phi :\mathbb{R}\to \mathbb{R}),\mathrm{Continuous}\phi \to \forall \{M:\mathbb{R}\},(\forall (x:\mathbb{R}),|\phi x|\le M)\to \mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}(n:\mathbb{N})\mapsto 1/\mathrm{coe}(n+1)\cdot \sum (k:\mathrm{Fin}(n+1)),\phi (\mu .\mathrm{quantile}((\mathrm{coe}\mathrm{coe}k+1/2)/(\mathrm{coe}n+1))))\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}(\int (x:\mathbb{R}),\phi x\mathrm{dmu}\mu ))$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.tendsto_integral_of_quantile_midpoint (✓ 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 bounded continuous real test, equal-weight midpoint quantile sums converge to its expectation under the original law.

Definition 1.14 (stopLoss).

$$\forall (\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R})(z:\mathbb{R}),\mu .\mathrm{stopLoss}z=\int (x:\mathbb{R}),\max (x-z)0\mathrm{dmu}\mu$$

Formalization. D5/S3/Analytic/Probability/CompactQuantile.stopLoss (✓ 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 expected positive part of the excess over a threshold, defined by the real Bochner integral.

Lemma 1.15 (stopLoss_nonneg).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}(z:\mathbb{R}),0\le \mu .\mathrm{stopLoss}z$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.stopLoss_nonneg (✓ 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 stop-loss value is nonnegative; the assertion uses the total integral convention and needs no finiteness assumption.

Lemma 1.16 (stopLoss_integrable).

$$\forall \{\mu :\mathrm{MeasureTheory}.\mathrm{Measure}\mathbb{R}\}[\mathrm{MeasureTheory}.\mathrm{IsFiniteMeasure}\mu ],\mathrm{MeasureTheory}.\mathrm{Integrable}(\mathrm{fun}x\mapsto x)\mu \to \forall (z:\mathbb{R}),\mathrm{MeasureTheory}.\mathrm{Integrable}(\mathrm{fun}x\mapsto \max (x-z)0)\mu$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/CompactQuantile.stopLoss_integrable (✓ 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 integrable real coordinate under a finite measure makes every positive-part excess integrable.

References

• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.aemeasurable_quantile_restrict_Ioo
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.binMidpoint
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.bins_pairwise_disjoint
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.countable_not_continuousWithinAt_quantile
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.iUnion_bins_eq_Ico
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.integral_eq_integral_quantile
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.map_quantile_volume_Ioo
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.monotoneOn_quantile
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.quantile
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.quantile_le_iff
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.set_nonempty
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.stepFun
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.stopLoss
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.stopLoss_integrable
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.stopLoss_nonneg
• Truth anchor: D5/S3/Analytic/Probability/CompactQuantile.tendsto_integral_of_quantile_midpoint