Signed stock and bank holdings
Definitionfd02_Tradearbitrageformal-verificationoption-pricing
A buy-and-hold strategy consists of unrestricted real stock holdings and real units of the bank account. Negative values represent short-selling or borrowing.
Definition code
import Mathlib.Data.Real.Basic namespace FinancialDerivatives.FD02 /-- Signed holdings in the stock and the unit-price bank account. -/ structure Trade where shares : ℝ cash : ℝ end FinancialDerivatives.FD02
Source
Original derived definition based on Wilmott, Howison and Dewynne (1995), §§2.4,3.2, printed pp. 30–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
A trade is an ordered pair of arbitrary real numbers, interpreted as the number of shares and the cash holding . Either component may be positive, zero, or negative; no budget or sign constraint is imposed.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.