Initial cost of a stock-and-bank trade
Definitionfd02_initialCostarbitrageformal-verificationoption-pricing
Date-zero cost equals shares held times the current stock price plus the current cash-account holding.
Definition code
import Mathlib.Data.Real.Basic import Definitions.Def_fd02_TwoStateMarket import Definitions.Def_fd02_Trade namespace FinancialDerivatives.FD02 /-- Date-zero portfolio cost in bank-account monetary units. -/ def initialCost (m : TwoStateMarket) (t : Trade) : ℝ := t.shares * m.spot + t.cash end FinancialDerivatives.FD02
Source
Original derived definition based on Wilmott, Howison and Dewynne (1995), §3.2, printed pp. 33–34; https://doi.org/10.1017/CBO9780511812545. The same object is fixed for all FD-02 theorem statements.
Read-back
What the Lean code literally says, in plain math · GPT-6
For any market with real spot , bank growth , and stock factors and any signed trade , the defined initial cost is the real number . Thus a negative holding or cost is allowed, and the bank cash holding enters with coefficient one.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.