Two-state portfolio terminal payoff

Definition

fd02_terminalPayoff

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

arbitrageformal-verificationoption-pricing

The same shares and cash holdings are held until the terminal date, with stock factors up/down and common bank growth.

Definition code

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

namespace FinancialDerivatives.FD02

/-- Terminal value after the up or down stock move. -/
def terminalPayoff (m : TwoStateMarket) (t : Trade) (ω : Bool) : ℝ :=
  match ω with
  | true => t.shares * m.spot * m.up + t.cash * m.growth
  | false => t.shares * m.spot * m.down + t.cash * m.growth

end FinancialDerivatives.FD02

Source

Original derived definition based on Wilmott, Howison and Dewynne (1995), §2.4 and §10.1, printed pp. 30–31 and 180–182; 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>0$ , bank growth $R>0$ , and stock factors $0\le D<U$ , any signed trade $(x,c)\in\mathbb R^2$ , and either Boolean state $\omega$ , the defined terminal payoff is $P_{\mathrm{true}}(x,c)=xSU+cR$ when $\omega=\mathrm{true}$ and $P_{\mathrm{false}}(x,c)=xSD+cR$ when $\omega=\mathrm{false}$ . These are the only two states and there are no sign constraints on holdings or payoffs.

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