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

Jingyuan Li

Papers from arXiv.org

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.

Date: 2025-05
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://arxiv.org/pdf/2505.12840 Latest version (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:arx:papers:2505.12840

Access Statistics for this paper

More papers in Papers from arXiv.org
Bibliographic data for series maintained by arXiv administrators ().