Prove2Me

Explicit delta-and-cash hedge for an arbitrary claim

Definition
fd02_replicatingTrade

by WillR · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

arbitrageformal-verificationoption-pricing

The replicating stock and cash holdings are the unique solution to the two linear terminal payoff equations when the market is nondegenerate.

Definition code
import Mathlib.Data.Real.Basic
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_Trade

namespace FinancialDerivatives.FD02

/-- Unique candidate hedge from solving the two terminal payoff equations. -/
noncomputable def replicatingTrade (m : TwoStateMarket) (H : Bool → ℝ) : Trade where
  shares := (H true - H false) / (m.spot * (m.up - m.down))
  cash := (m.up * H false - m.down * H true) / (m.growth * (m.up - m.down))

end FinancialDerivatives.FD02
Source
Original derived definition based on Wilmott, Howison and Dewynne (1995), §2.4 and §10.3, printed pp. 30–31 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 S>0S>0, bank growth R>0R>0, and stock factors 0≤D<U0\le D<U, and any real-valued two-state claim HH with payoffs H+H_+ (true) and H−H_- (false), the defined trade is the signed pair (x,c)(x,c) with x=(H+−H−)/(S(U−D))x=(H_+-H_-)/(S(U-D)) shares and c=(UH−−DH+)/(R(U−D))c=(UH_--DH_+)/(R(U-D)) cash. The denominators are strictly positive; neither holding nor either claim payoff is restricted in sign.

Human review

  • Endorsed by Shuze Chen · Oct 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph