Asset-or-nothing call and put: $SN(\pm d_+)$

Proved

BlackScholesModel.asset_or_nothing_value

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

black-scholesmathematical-financeoption-pricing

Let $K>0$ , $\sigma>0$ , $S>0$ , $t<T$ , $r\in\mathbb R$ , $\tau=T-t$ , and let $S_T=S\exp\big((r-\frac{\sigma^2}2)\tau+\sigma\sqrt\tau Z\big)$ with $Z$ standard normal be the risk-neutral terminal price. The risk-neutral value of a binary option paying one unit of the asset if the spot ends above (respectively below) the strike is

e^{-r\tau}\,\mathbb E\big[S_T\,\mathbf 1_{\{S_T>K\}}\big]=SN(d_+),\qquad e^{-r\tau}\,\mathbb E\big[S_T\,\mathbf 1_{\{S_T<K\}}\big]=SN(-d_+).

Together with the cash-or-nothing values, this splits the call price into an asset-or-nothing call minus $K$ cash-or-nothing calls.

Formalization Note The source's formulas include a dividend yield $q$ ; this is the non-dividend case $q=0$ , with $d_1=d_+$ .

Preamble

import Mathlib
import Definitions.Def_BlackScholesModel_Core

open Real MeasureTheory ProbabilityTheory Filter Topology
open scoped ContDiff

Formal statement

namespace BlackScholesModel

theorem asset_or_nothing_value (K r σ T S t : ℝ) (hK : 0 < K) (hσ : 0 < σ) (hS : 0 < S) (ht : t < T) :
    Real.exp (-r * (T - t))
        * ∫ z in {z | K < terminalPrice S r σ (T - t) z}, terminalPrice S r σ (T - t) z
            ∂(gaussianReal 0 1)
      = S * stdNormalCDF (dPlus S K r σ (T - t)) ∧
    Real.exp (-r * (T - t))
        * ∫ z in {z | terminalPrice S r σ (T - t) z < K}, terminalPrice S r σ (T - t) z
            ∂(gaussianReal 0 1)
      = S * stdNormalCDF (-dPlus S K r σ (T - t)) := by sorry

end BlackScholesModel

Source

Wikipedia, "Black–Scholes model" (snapshot supplied as Black–Scholes_model.pdf, 22 pp.), https://en.wikipedia.org/wiki/Black%E2%80%93Scholes_model; p. 11 (Binary options: asset-or-nothing call and put), p. 6 (SN(d+) is the present value of the expected asset price given exercise)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (at the explicit instruction of the proposal owner), not by an independent blind auditor. It is not independent testimony; reviewers should compare it against the Lean code themselves.

Here $K,r,\sigma,T,S,t$ are arbitrary real numbers subject to the hypotheses $K>0$ , $\sigma>0$ , $S>0$ and $t<T$ (so $\tau:=T-t>0$ ); $r$ is unrestricted (it may be zero or negative). $N$ , $N'$ , $d_\pm$ , $C$ , $P$ are the functions of the companion definition file (normal distribution function given by its integral, normal density in closed form, $d_\pm=d_\pm(S,K,r,\sigma,T-t)$ , call price $C(S,t)=N(d_+)S-N(d_-)Ke^{-r(T-t)}$ , put price $P(S,t)=N(-d_-)Ke^{-r(T-t)}-N(-d_+)S$ ).

Let $\gamma$ be the standard Gaussian probability measure on $\mathbb R$ and $S_T(z)=S\exp\big((r-\sigma^2/2)(T-t)+\sigma\sqrt{T-t}\,z\big)$ . The theorem asserts both

e^{-r(T-t)}\int_{\{z:\,K<S_T(z)\}}S_T(z)\,d\gamma(z)=S\,N(d_+)\quad\text{and}\quad e^{-r(T-t)}\int_{\{z:\,S_T(z)<K\}}S_T(z)\,d\gamma(z)=S\,N(-d_+),

with $d_+=d_+(S,K,r,\sigma,T-t)$ ; the integrals are Bochner integrals over the indicated sets (set to $0$ by convention if not integrable).

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Asset-or-nothing call and put: SN(±d+)SN(\pm d_+)SN(±d+​)

Asset-or-nothing call and put: $SN(\pm d_+)$