Geometric Formalization of First-Order Stochastic Dominance in $N$ Dimensions: A Tractable Path to Multi-Dimensional Economic Decision Analysis
Jingyuan Li
cs.LO
May 19, 2025 · v1
TL;DR
Formally verifies a geometric characterization of N-dimensional first-order stochastic dominance using the Lean 4 theorem prover.
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.
Problem
Multi-dimensional first-order stochastic dominance (FSD) relies on complex measure theory and multivariate calculus, creating barriers to formal verification. Economic applications in portfolio selection and risk management need rigorous guarantees that traditional analytical approaches make hard to machine-check.
Approach
The authors introduce a geometric characterization of N-dimensional FSD through direct comparison of survival probabilities in upper-right orthants, bypassing integration theory. Key definitions and the equivalence between traditional FSD and the geometric characterization are formalized and proved in Lean 4.
Results
The geometric framework provides a tractable path to formal verification of multi-dimensional stochastic dominance. The formalization demonstrates applicability to portfolio selection, risk management, and welfare analysis while maintaining mathematical rigor.
