Archive ouverte HAL - Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL

Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL

Abstract : 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.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01954948
Contributeur : Mnacho Echenim <>
Soumis le : vendredi 14 décembre 2018 - 09:39:33
Dernière modification le : mardi 2 avril 2019 - 01:47:33

Lien texte intégral

Identifiants

  • HAL Id : hal-01954948, version 1
  • ARXIV : 1807.09873

Citation

Mnacho Echenim, Herve Guiol, Nicolas Peltier. Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. 2018. ⟨hal-01954948⟩

Partager

Métriques

Consultations de la notice

159