Prove2Me

Risk-neutral up probability from stock and bank factors

Definition
fd02_riskNeutralUp

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

arbitrageformal-verificationoption-pricing

The candidate up-state risk-neutral weight is (R-d)/(u-d), with positivity to be derived from no-arbitrage.

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

namespace FinancialDerivatives.FD02

/-- Unique candidate up weight from the stock martingale equation. -/
noncomputable def riskNeutralUp (m : TwoStateMarket) : ℝ :=
  (m.growth - m.down) / (m.up - m.down)

end FinancialDerivatives.FD02
Source
Original derived definition based on Wilmott, Howison and Dewynne (1995), §10.2, equation (10.8), printed p. 184; 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, the defined candidate up-state weight is the real number q=(R−D)/(U−D)q=(R-D)/(U-D). The denominator is strictly positive because D<UD<U; the definition itself imposes neither q≥0q\ge0 nor q≤1q\le1, since RR need not lie between the two factors.

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