N 维一阶随机支配的几何形式化：面向多维经济决策分析的可计算路径
计算机科学中的逻辑
2025-05-20 v1 理论经济学
计算金融
摘要
本文提出并形式化验证了一种用于 N 维一阶随机支配（FSD）的新型几何框架，采用 Lean 4 定理证明器。传统的多维随机支配方法高度依赖复杂的测度论与多变量微积分，导致在证明助理中难以形式化。我们的几何方法通过直接比较上右象限中生存概率来刻画 N 维 FSD，绕过复杂积分理论的需求。我们形式化了关键定义，并证明了传统 FSD 要求与几何刻画之间的等价性。该方法实现了更可计算、直观的形式化路径，同时保持数学严谨性。我们展示了这一框架如何直接支持组合选择、风险管理和福利分析等多维经济问题的形式化分析。该工作为在经济学和金融学中进一步开发经验证明的决策工具奠定了基础，尤其是那些需要严格保证的高风险领域。
引用
@article{arxiv.2505.12840,
title = {Geometric Formalization of First-Order Stochastic Dominance in $N$ Dimensions: A Tractable Path to Multi-Dimensional Economic Decision Analysis},
author = {Jingyuan Li},
journal= {arXiv preprint arXiv:2505.12840},
year = {2025}
}