Strong zero-cost no-arbitrage in the base market
Definitionfd02_NoArbitragearbitrageformal-verificationoption-pricing
Strong absence of arbitrage excludes a zero-cost trading strategy that is nonnegative in both states and strictly positive in either state.
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
/-- Zero initial cost and nonnegative payoffs force zero in both states. -/
def NoArbitrage (m : TwoStateMarket) : Prop :=
∀ t : Trade,
initialCost m t = 0 →
0 ≤ terminalPayoff m t true →
0 ≤ terminalPayoff m t false →
terminalPayoff m t true = 0 ∧ terminalPayoff m t false = 0
end FinancialDerivatives.FD02Source
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 , the predicate “no arbitrage” holds exactly if, for every pair of real signed holdings , the three conditions , , and imply simultaneously and . In particular, the condition concerns zero-initial-cost trades and includes both states, including zero payoffs.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.