Prove2Me

Discounted one-period risk-neutral claim valuation

Definition
fd02_riskNeutralValue

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

arbitrageformal-verificationoption-pricing

The one-period proposed price is the up/down payoff average weighted by risk-neutral probabilities and divided by the bank accumulation factor.

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

namespace FinancialDerivatives.FD02

/-- Discounted two-state expectation under the candidate martingale weights. -/
noncomputable def riskNeutralValue (m : TwoStateMarket) (H : Bool → ℝ) : ℝ :=
  (riskNeutralUp m * H true + (1 - riskNeutralUp m) * H false) / m.growth

end FinancialDerivatives.FD02
Source
Original derived definition based on Wilmott, Howison and Dewynne (1995), §10.1, equation (10.2), and §10.3, printed pp. 182 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 two-state real payoff HH with H+=H(true)H_+=H(\mathrm{true}) and H−=H(false)H_-=H(\mathrm{false}), the defined value is V(H)=(qH++(1−q)H−)/RV(H)=\big(qH_++(1-q)H_-\big)/R, where q=(R−D)/(U−D)q=(R-D)/(U-D). Since R>0R>0 and U−D>0U-D>0, both divisions have nonzero denominators; without an additional hypothesis the weights need not be nonnegative.

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