Risk-neutral path weight factors over concatenated histories
ProvedFinancialDerivatives.FD05.historyWeight_appendbarrier-optionsfd05financial-derivatives
The risk-neutral probability of a concatenated move history is the product of the corresponding history weights.
Preamble
import Mathlib.Data.Real.Basic import Definitions.Def_fd05_historyWeight
Formal statement
namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03
theorem historyWeight_append (m : BinomialMarket) (xs ys : List Bool) :
historyWeight m (xs ++ ys) =
historyWeight m xs * historyWeight m ys := by sorry
end FinancialDerivatives.FD05Source
Wilmott, Howison and Dewynne (1995), The Mathematics of Financial Derivatives, Chapter 12, pp. 206–212. Rigorous finite-binomial first-hit analogue.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.