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