Risk-neutral probabilities are positive and normalised

Proved

FinancialDerivatives.FD02.riskNeutral_weights_sum

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

arbitrageformal-verificationoption-pricing

The unique up/down risk-neutral weights sum to one and each is strictly positive under strong no-arbitrage.

This is an original derived theorem target; a remote compiler must validate its declaration and proof.

Preamble

import Mathlib.Data.Real.Basic
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_riskNeutralUp
import Definitions.Def_fd02_NoArbitrage

Formal statement

namespace FinancialDerivatives.FD02

/-- Risk-neutral probabilities are positive and normalised. -/
theorem riskNeutral_weights_sum (m : TwoStateMarket) (hNA : NoArbitrage m) :
  riskNeutralUp m + (1 - riskNeutralUp m) = 1 ∧ 0 < riskNeutralUp m ∧ 0 < 1 - riskNeutralUp m := by sorry

end FinancialDerivatives.FD02

Source

Derived from Wilmott, Howison and Dewynne (1995), §10.2, equations (10.4) and (10.8), pp. 183–184. https://doi.org/10.1017/CBO9780511812545.

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$ , if every signed real pair $(x,c)$ with $xS+c=0$ , $xSU+cR\ge0$ , and $xSD+cR\ge0$ has $xSU+cR=0$ and $xSD+cR=0$ , then, with $q=(R-D)/(U-D)$ , all three conclusions hold: $q+(1-q)=1$ , $0<q$ , and $0<1-q$ . Thus both named weights are strictly positive and sum exactly to one.

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