# Pricing in discrete financial models

 Title: Pricing in discrete financial models Author: Mnacho Echenim Submission date: 2018-07-16 Abstract: We have formalized the computation of fair prices for derivative products in discrete financial models. As an application, we derive a way to compute fair prices of derivative products in the Cox-Ross-Rubinstein model of a financial market, thus completing the work that was presented in this paper. Change history: [2019-05-12]: Renamed discr_mkt predicate to stk_strict_subs and got rid of predicate A for a more natural definition of the type discrete_market; renamed basic quantity processes for coherent notation; renamed value_process into val_process and closing_value_process to cls_val_process; relaxed hypothesis of lemma CRR_market_fair_price. Added functions to price some basic options. (revision 0b813a1a833f) BibTeX: @article{DiscretePricing-AFP, author = {Mnacho Echenim}, title = {Pricing in discrete financial models}, journal = {Archive of Formal Proofs}, month = jul, year = 2018, note = {\url{http://isa-afp.org/entries/DiscretePricing.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.