Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Geometric Formalization of First-Order Stochastic Dominance in $N$ Dimensions: A Tractable Path to Multi-Dimensional Economic Decision Analysis

Jingyuan Li

TL;DR

This work addresses the challenge of formalizing multi-dimensional first-order stochastic dominance by introducing a geometric framework that uses survival probabilities in the upper-right orthant. Implemented in Lean 4 with Mathlib, it replaces measure-theoretic complexity with combinatorial, inclusion–exclusion constructions on hyperrectangles, yielding tractable equivalence results between geometric FSD and traditional utility-based FSD. The key contributions include the ND definitions (RVector, Icc_n, Ioo_n, indicatorUpperRightOrthant), the ND survival probability, and formal proofs translating orthant-indicator dominance into FSD, along with an extension pathway to general non-decreasing utilities. The framework enables verifiable analysis for multi-attribute economic problems—portfolio selection, risk management, and welfare analysis—and opens avenues for certified libraries, privacy guarantees, and AI systems that require rigorous, multi-dimensional decision guarantees.

Abstract

This paper introduces and formally verifies a novel geometric framework for first-order stochastic dominance (FSD) in $N$ dimensions using the Lean 4 theorem prover. Traditional analytical approaches to multi-dimensional stochastic dominance rely heavily on complex measure theory and multivariate calculus, creating significant barriers to formalization in proof assistants. Our geometric approach characterizes $N$-dimensional FSD through direct comparison of survival probabilities in upper-right orthants, bypassing the need for complex integration theory. We formalize key definitions and prove the equivalence between traditional FSD requirements and our geometric characterization. This approach achieves a more tractable and intuitive path to formal verification while maintaining mathematical rigor. We demonstrate how this framework directly enables formal analysis of multi-dimensional economic problems in portfolio selection, risk management, and welfare analysis. The work establishes a foundation for further development of verified decision-making tools in economics and finance, particularly for high-stakes domains requiring rigorous guarantees.

Geometric Formalization of First-Order Stochastic Dominance in $N$ Dimensions: A Tractable Path to Multi-Dimensional Economic Decision Analysis

TL;DR

This work addresses the challenge of formalizing multi-dimensional first-order stochastic dominance by introducing a geometric framework that uses survival probabilities in the upper-right orthant. Implemented in Lean 4 with Mathlib, it replaces measure-theoretic complexity with combinatorial, inclusion–exclusion constructions on hyperrectangles, yielding tractable equivalence results between geometric FSD and traditional utility-based FSD. The key contributions include the ND definitions (RVector, Icc_n, Ioo_n, indicatorUpperRightOrthant), the ND survival probability, and formal proofs translating orthant-indicator dominance into FSD, along with an extension pathway to general non-decreasing utilities. The framework enables verifiable analysis for multi-attribute economic problems—portfolio selection, risk management, and welfare analysis—and opens avenues for certified libraries, privacy guarantees, and AI systems that require rigorous, multi-dimensional decision guarantees.

Abstract

This paper introduces and formally verifies a novel geometric framework for first-order stochastic dominance (FSD) in dimensions using the Lean 4 theorem prover. Traditional analytical approaches to multi-dimensional stochastic dominance rely heavily on complex measure theory and multivariate calculus, creating significant barriers to formalization in proof assistants. Our geometric approach characterizes -dimensional FSD through direct comparison of survival probabilities in upper-right orthants, bypassing the need for complex integration theory. We formalize key definitions and prove the equivalence between traditional FSD requirements and our geometric characterization. This approach achieves a more tractable and intuitive path to formal verification while maintaining mathematical rigor. We demonstrate how this framework directly enables formal analysis of multi-dimensional economic problems in portfolio selection, risk management, and welfare analysis. The work establishes a foundation for further development of verified decision-making tools in economics and finance, particularly for high-stakes domains requiring rigorous guarantees.
Paper Structure (32 sections, 8 theorems, 16 equations, 1 figure)

This paper contains 32 sections, 8 theorems, 16 equations, 1 figure.

Table of Contents

  1. Introduction
  2. The Role of the Lean 4 Prover and Mathlib
  3. Geometric Formalization of First-Order Stochastic Dominance in One Dimension
  4. Specialized Riemann-Stieltjes Integral for Indicator Functions
  5. Geometric Framework for $N$-Dimensional Stochastic Dominance
  6. Key Theorems for $N$-Dimensional Geometric FSD
  7. Main Results
  8. Extension to General Non-Decreasing Utility Functions
  9. Economic Applications: A Geometric Perspective
  10. Portfolio Selection
  11. Risk Management
  12. Welfare Analysis and Policy Evaluation
  13. New Application Area: Formal Guarantees in Data Privacy
  14. New Application Area: Certified Libraries and Embedded Systems
  15. Comparison with Analytical and Other Formal Approaches
  16. ...and 17 more sections

Key Result

Lemma 3.2

Suppose $a < b$. If $u_1(x) = \mathbf{1}_{(x_1, \infty)}(x)$ and $u_2(x) = \mathbf{1}_{(x_2, \infty)}(x)$ agree for all $x \in [a, b]$, where $x_1, x_2 \in (a, b)$, then $x_1 = x_2$.

Figures (1)

  • Figure 1: Geometric interpretation of the upper-right orthant in 2D stochastic dominance. The survival probability measures the probability mass in the shaded region where all components exceed their threshold values.

Theorems & Definitions (43)

  • Definition 3.1: Specialized Riemann-Stieltjes Integral for Indicator Functions
  • Remark 3.1: Formalization Note
  • Example 3.1: Calculating the Specialized Integral
  • Lemma 3.2: Uniqueness of Indicator Point (1D)
  • proof
  • Remark 3.2: Verification Perspective
  • Lemma 3.3: Integral Calculation for Indicator Functions (1D)
  • proof
  • Remark 3.3: Purpose
  • Theorem 3.4: FSD Equivalence for Indicator Functions (1D)
  • ...and 33 more