Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL

被引：0
|
作者：
Echenim, Mnacho [1 ]
Guiol, Hervé [2 ]
Peltier, Nicolas [1 ]
机构：
[1] LIG, Univ. Grenoble Alpes, CNRS, Grenoble,38000, France
[2] TIMC, Univ. Grenoble Alpes, CNRS, Grenoble,38000, France
来源：
Journal of Automated Reasoning | 2019年 / 64卷 / 04期
关键词：
We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets; portfolios; derivative products; arbitrages or fair prices; and we show that; under the usual no-arbitrage condition; the existence of a replicating portfolio for a derivative implies that the latter admits a unique fair price. Then; we provide a formalization of the Cox-Rubinstein model and we show that the market is complete in this model; i.e; that every derivative product admits a replicating portfolio. This entails that in this model; every derivative product admits a unique fair price. In addition; we provide Isabelle functions to compute the fair price of some derivative products. © Springer Nature B.V. 2019;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
引用
收藏
页码：737 / 765
相关论文
共 10 条
1