Strong no-arbitrage after adding a quoted derivative
Definitionfd02_ClaimNoArbitragearbitrageformal-verificationoption-pricing
The enlarged market admits unrestricted signed quantities of the claim at quote p. Any zero-cost portfolio with nonnegative payments in both states must pay zero in both.
Definition code
import Mathlib.Data.Real.Basic
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_Trade
import Definitions.Def_fd02_initialCost
import Definitions.Def_fd02_terminalPayoff
namespace FinancialDerivatives.FD02
/-- No free terminal payoff from an unrestricted signed derivative holding. -/
def ClaimNoArbitrage (m : TwoStateMarket) (H : Bool → ℝ) (p : ℝ) : Prop :=
∀ (t : Trade) (a : ℝ),
initialCost m t + a * p = 0 →
0 ≤ terminalPayoff m t true + a * H true →
0 ≤ terminalPayoff m t false + a * H false →
terminalPayoff m t true + a * H true = 0 ∧
terminalPayoff m t false + a * H false = 0
end FinancialDerivatives.FD02Source
Original derived definition based on Wilmott, Howison and Dewynne (1995), §3.2 and §10.3, printed pp. 33–34 and 187; 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 , any real-valued claim with and , and any quoted real price , the predicate “claim no arbitrage” means: for every signed stock/cash trade and every signed amount of the claim, if , , and , then and . This definition does not separately assume no arbitrage for stock and cash.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.