Black–Scholes call and put prices as risk-neutral expectations

In the constant-coefficient Black–Scholes market with interest rate r and volatility σ, the spot price after a remaining maturity τ ≥ 0, started from spot s, has under the risk-neutral measure the law of

S_τ = s * exp ((r - σ² / 2) * τ + σ * √τ * Z), Z ∼ N(0, 1).

This file works in that standard Gaussian coordinate. It defines S_τ as a function of Z (TauCeti.BlackScholes.terminalSpot), the discounted risk-neutral expectation exp (-r τ) * E[h (S_τ)] of a payoff h (TauCeti.BlackScholes.riskNeutralPrice), and the closed-form Black–Scholes prices

C = s Φ(d₊) - K e^{-rτ} Φ(d₋), P = K e^{-rτ} Φ(-d₋) - s Φ(-d₊),

with d₊ = (log (s / K) + (r + σ² / 2) τ) / (σ √τ) and d₋ = d₊ - σ √τ, where Φ is the cumulative distribution function cdf (gaussianReal 0 1) of the standard Gaussian law.

The main results identify the two: the risk-neutral price of the call payoff (x - K)⁺ is C and that of the put payoff (K - x)⁺ is P, for s, K, σ, τ > 0. Along the way the discounted stock has risk-neutral price s, and the closed forms satisfy put–call parity C - P = s - K e^{-rτ}.

The computation splits the call payoff on the in-the-money event {-d₋ < Z}. The strike part is a Gaussian tail; the stock part is an exponentially weighted Gaussian tail, which is evaluated by exponential tilting N(0, 1) ↦ N(σ √τ, 1) (TauCeti.Probability.setIntegral_exp_mul_gaussianReal), the change to the stock numéraire.

Main declarations

• TauCeti.BlackScholes.terminalSpot — the risk-neutral terminal spot as a function of the standard Gaussian coordinate.
• TauCeti.BlackScholes.riskNeutralPrice — the discounted risk-neutral expectation of a payoff.
• TauCeti.BlackScholes.dPlus, TauCeti.BlackScholes.dMinus — the Black–Scholes d₊, d₋.
• TauCeti.BlackScholes.mul_gaussianPDFReal_dPlus — the density identity s φ(d₊) = K e^{-rτ} φ(d₋), where φ is the standard Gaussian density.
• TauCeti.BlackScholes.callPrice, TauCeti.BlackScholes.putPrice — the closed-form prices.
• TauCeti.BlackScholes.riskNeutralPrice_id — the discounted stock is priced at s.
• TauCeti.BlackScholes.callPrice_sub_putPrice — put–call parity.
• TauCeti.BlackScholes.riskNeutralPrice_call — the risk-neutral price of a call is callPrice.
• TauCeti.BlackScholes.riskNeutralPrice_put — the risk-neutral price of a put is putPrice.
• TauCeti.BlackScholes.callPrice_nonneg, TauCeti.BlackScholes.callPrice_le, TauCeti.BlackScholes.putPrice_nonneg, TauCeti.BlackScholes.putPrice_le_mul_cdf, TauCeti.BlackScholes.putPrice_le — the no-arbitrage bounds 0 ≤ C ≤ s and 0 ≤ P ≤ K e^{-rτ} Φ(-d₋) ≤ K e^{-rτ}.
• ContDiffAt.callPrice, ContDiffAt.putPrice — smooth composition of the closed forms with spot and remaining maturity wherever s ≠ 0 and τ > 0, for K, σ ≠ 0.

References

• F. Black, M. Scholes, The pricing of options and corporate liabilities, J. Polit. Econ. 81 (1973), 637–654.
• S. E. Shreve, Stochastic Calculus for Finance II: Continuous-Time Models, Springer, 2004, §5.2.5.

The risk-neutral terminal spot and the pricing functional

noncomputable def TauCeti.BlackScholes.terminalSpot (s r σ τ z : ℝ) : ℝ

The risk-neutral spot price after remaining maturity τ, started from spot s, in a market with interest rate r and volatility σ, written as a function of a standard Gaussian coordinate z: s * exp ((r - σ² / 2) * τ + σ * √τ * z).

theorem TauCeti.BlackScholes.terminalSpot_def (s r σ τ z : ℝ) : terminalSpot s r σ τ z = s * Real.exp ((r - σ ^ 2 / 2) * τ + σ * √τ * z)

Unfolding lemma for terminalSpot.

@[simp]

theorem TauCeti.BlackScholes.terminalSpot_zero (s r σ z : ℝ) : terminalSpot s r σ 0 z = s

At zero remaining maturity the terminal spot is the current spot.

theorem TauCeti.BlackScholes.terminalSpot_pos {s : ℝ} (hs : 0 < s) (r σ τ z : ℝ) : 0 < terminalSpot s r σ τ z

The terminal spot is positive when the current spot is.

theorem TauCeti.BlackScholes.measurable_terminalSpot (s r σ τ : ℝ) : Measurable (terminalSpot s r σ τ)

The terminal spot is a measurable function of the Gaussian coordinate.

theorem TauCeti.BlackScholes.integrable_terminalSpot (s r σ τ : ℝ) : MeasureTheory.Integrable (terminalSpot s r σ τ) (ProbabilityTheory.gaussianReal 0 1)

The terminal spot is integrable against the standard Gaussian law.

theorem TauCeti.BlackScholes.setIntegral_terminalSpot {τ : ℝ} (s r σ : ℝ) (hτ : 0 ≤ τ) (A : Set ℝ) : ∫ (z : ℝ) in A, terminalSpot s r σ τ z ∂ProbabilityTheory.gaussianReal 0 1 = s * Real.exp (r * τ) * (ProbabilityTheory.gaussianReal (σ * √τ) 1).real A

Change to the stock numéraire. Over any set A of Gaussian coordinates, the terminal spot integrates to its forward value s * exp (r τ) times the mass of A under the shifted law N(σ √τ, 1).

noncomputable def TauCeti.BlackScholes.riskNeutralPrice (h : ℝ → ℝ) (s r σ τ : ℝ) : ℝ

The discounted risk-neutral expectation exp (-r τ) * E[h (S_τ)] of a payoff h of the terminal spot S_τ = terminalSpot s r σ τ Z, Z ∼ N(0, 1). For a non-integrable payoff the Bochner integral, and hence this value, is zero.

theorem TauCeti.BlackScholes.riskNeutralPrice_def (h : ℝ → ℝ) (s r σ τ : ℝ) : riskNeutralPrice h s r σ τ = Real.exp (-r * τ) * ∫ (z : ℝ), h (terminalSpot s r σ τ z) ∂ProbabilityTheory.gaussianReal 0 1

Unfolding lemma for riskNeutralPrice.

@[simp]

theorem TauCeti.BlackScholes.riskNeutralPrice_zero (h : ℝ → ℝ) (s r σ : ℝ) : riskNeutralPrice h s r σ 0 = h s

At zero remaining maturity a payoff is priced at its value at the current spot.

theorem TauCeti.BlackScholes.measurable_riskNeutralPrice {h : ℝ → ℝ} (hh : Measurable h) (r σ τ : ℝ) : Measurable fun (s : ℝ) => riskNeutralPrice h s r σ τ

The risk-neutral price of a measurable payoff is a measurable function of the spot.

theorem TauCeti.BlackScholes.riskNeutralPrice_nonneg {h : ℝ → ℝ} (hh : ∀ (x : ℝ), 0 ≤ h x) (s r σ τ : ℝ) : 0 ≤ riskNeutralPrice h s r σ τ

A nonnegative payoff has a nonnegative risk-neutral price.

theorem TauCeti.BlackScholes.riskNeutralPrice_id {τ : ℝ} (s r σ : ℝ) (hτ : 0 ≤ τ) : riskNeutralPrice id s r σ τ = s

The stock itself, as a payoff, is priced at the current spot: the discounted risk-neutral expectation exp (-r τ) * E[S_τ] of the terminal spot equals s.

The Black–Scholes formulas

noncomputable def TauCeti.BlackScholes.dPlus (s r σ K τ : ℝ) : ℝ

The Black–Scholes quantity d₊ = (log (s / K) + (r + σ² / 2) τ) / (σ √τ).

theorem TauCeti.BlackScholes.dPlus_def (s r σ K τ : ℝ) : dPlus s r σ K τ = (Real.log (s / K) + (r + σ ^ 2 / 2) * τ) / (σ * √τ)

Unfolding lemma for dPlus.

noncomputable def TauCeti.BlackScholes.dMinus (s r σ K τ : ℝ) : ℝ

The Black–Scholes quantity d₋ = d₊ - σ √τ.

theorem TauCeti.BlackScholes.dMinus_def (s r σ K τ : ℝ) : dMinus s r σ K τ = dPlus s r σ K τ - σ * √τ

Unfolding lemma for dMinus.

theorem TauCeti.BlackScholes.measurable_dPlus (r σ K : ℝ) : Measurable fun (p : ℝ × ℝ) => dPlus p.1 r σ K p.2

The Gaussian coordinate d₊ is jointly measurable in spot and remaining maturity.

theorem TauCeti.BlackScholes.measurable_dMinus (r σ K : ℝ) : Measurable fun (p : ℝ × ℝ) => dMinus p.1 r σ K p.2

The Gaussian coordinate d₋ is jointly measurable in spot and remaining maturity.

theorem TauCeti.BlackScholes.dMinus_eq (s r σ K τ : ℝ) : dMinus s r σ K τ = (Real.log (s / K) + (r - σ ^ 2 / 2) * τ) / (σ * √τ)

d₋ = (log (s / K) + (r - σ² / 2) τ) / (σ √τ), for every τ: if σ √τ ≠ 0 then τ > 0, since √τ = 0 for τ ≤ 0. Lean subtlety: when σ √τ = 0 (that is, σ = 0 or τ ≤ 0) both sides are 0, by Lean's convention x / 0 = 0.

The density identity

theorem TauCeti.BlackScholes.mul_gaussianPDFReal_dPlus {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : s * ProbabilityTheory.gaussianPDFReal 0 1 (dPlus s r σ K τ) = K * Real.exp (-r * τ) * ProbabilityTheory.gaussianPDFReal 0 1 (dMinus s r σ K τ)

The Black–Scholes density identity s φ(d₊) = K e^{-rτ} φ(d₋), where φ is the standard Gaussian density. It expresses that d₊² - d₋² = 2 (log (s / K) + r τ).

noncomputable def TauCeti.BlackScholes.callPrice (s r σ K τ : ℝ) : ℝ

The closed-form Black–Scholes price s Φ(d₊) - K e^{-rτ} Φ(d₋) of a European call with strike K and remaining maturity τ, where Φ = cdf (gaussianReal 0 1).

theorem TauCeti.BlackScholes.callPrice_def (s r σ K τ : ℝ) : callPrice s r σ K τ = s * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (dPlus s r σ K τ) - K * Real.exp (-r * τ) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (dMinus s r σ K τ)

Unfolding lemma for callPrice.

noncomputable def TauCeti.BlackScholes.putPrice (s r σ K τ : ℝ) : ℝ

The closed-form Black–Scholes price K e^{-rτ} Φ(-d₋) - s Φ(-d₊) of a European put with strike K and remaining maturity τ, where Φ = cdf (gaussianReal 0 1).

theorem TauCeti.BlackScholes.putPrice_def (s r σ K τ : ℝ) : putPrice s r σ K τ = K * Real.exp (-r * τ) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-dMinus s r σ K τ) - s * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-dPlus s r σ K τ)

Unfolding lemma for putPrice.

theorem TauCeti.BlackScholes.callPrice_sub_putPrice (s r σ K τ : ℝ) : callPrice s r σ K τ - putPrice s r σ K τ = s - K * Real.exp (-r * τ)

Put–call parity for the closed-form prices: C - P = s - K e^{-rτ}.

theorem TauCeti.BlackScholes.putPrice_eq_callPrice (s r σ K τ : ℝ) : putPrice s r σ K τ = callPrice s r σ K τ - s + K * Real.exp (-r * τ)

Put–call parity, solved for the put.

Risk-neutral prices of calls and puts

theorem TauCeti.BlackScholes.lt_terminalSpot_iff {s r σ K τ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hK : 0 < K) (hτ : 0 < τ) (z : ℝ) : K < terminalSpot s r σ τ z ↔ -dMinus s r σ K τ < z

The call finishes in the money exactly on the event {-d₋ < Z}.

theorem TauCeti.BlackScholes.riskNeutralPrice_call {s r σ K τ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hK : 0 < K) (hτ : 0 < τ) : riskNeutralPrice (fun (x : ℝ) => (x - K)⁺) s r σ τ = callPrice s r σ K τ

The Black–Scholes call formula. The discounted risk-neutral expectation of the call payoff (S_τ - K)⁺ is s Φ(d₊) - K e^{-rτ} Φ(d₋).

theorem TauCeti.BlackScholes.riskNeutralPrice_put {s r σ K τ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hK : 0 < K) (hτ : 0 < τ) : riskNeutralPrice (fun (x : ℝ) => (K - x)⁺) s r σ τ = putPrice s r σ K τ

The Black–Scholes put formula. The discounted risk-neutral expectation of the put payoff (K - S_τ)⁺ is K e^{-rτ} Φ(-d₋) - s Φ(-d₊).

No-arbitrage bounds

theorem TauCeti.BlackScholes.callPrice_nonneg {s r σ K τ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hK : 0 < K) (hτ : 0 < τ) : 0 ≤ callPrice s r σ K τ

The Black–Scholes call price is nonnegative.

theorem TauCeti.BlackScholes.putPrice_nonneg {s r σ K τ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hK : 0 < K) (hτ : 0 < τ) : 0 ≤ putPrice s r σ K τ

The Black–Scholes put price is nonnegative.

theorem TauCeti.BlackScholes.callPrice_le {s r σ K τ : ℝ} (hs : 0 ≤ s) (hK : 0 ≤ K) : callPrice s r σ K τ ≤ s

The Black–Scholes call price is at most the spot.

theorem TauCeti.BlackScholes.putPrice_le_mul_cdf {s r σ K τ : ℝ} (hs : 0 ≤ s) : putPrice s r σ K τ ≤ K * Real.exp (-r * τ) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-dMinus s r σ K τ)

The Black–Scholes put price is at most its strike leg K e^{-rτ} Φ(-d₋).

theorem TauCeti.BlackScholes.putPrice_le {s r σ K τ : ℝ} (hs : 0 ≤ s) (hK : 0 ≤ K) : putPrice s r σ K τ ≤ K * Real.exp (-r * τ)

The Black–Scholes put price is at most the discounted strike K e^{-rτ}.

Smooth composition

theorem ContDiffAt.dPlus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} {r σ K : ℝ} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContDiffAt ℝ n (fun (y : E) => TauCeti.BlackScholes.dPlus (f y) r σ K (g y)) x

The Black–Scholes normal argument is smooth under composition wherever its logarithm and denominator are nonsingular.

theorem ContDiffAt.dMinus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} {r σ K : ℝ} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContDiffAt ℝ n (fun (y : E) => TauCeti.BlackScholes.dMinus (f y) r σ K (g y)) x

The lower Black–Scholes normal argument is smooth under composition on the same domain.

theorem ContDiffAt.callPrice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} {r σ K : ℝ} {n : ℕ∞} (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContDiffAt ℝ (↑n) (fun (y : E) => TauCeti.BlackScholes.callPrice (f y) r σ K (g y)) x

The closed-form call price is smooth under composition in spot and remaining maturity wherever the normal arguments are nonsingular.

theorem ContDiffAt.putPrice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} {r σ K : ℝ} {n : ℕ∞} (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContDiffAt ℝ (↑n) (fun (y : E) => TauCeti.BlackScholes.putPrice (f y) r σ K (g y)) x

The closed-form put price is smooth under composition in spot and remaining maturity wherever the normal arguments are nonsingular.

theorem ContinuousAt.dPlus {E : Type u_1} [TopologicalSpace E] {f g : E → ℝ} {x : E} {r σ K : ℝ} (hf : ContinuousAt f x) (hg : ContinuousAt g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContinuousAt (fun (y : E) => TauCeti.BlackScholes.dPlus (f y) r σ K (g y)) x

The Black–Scholes normal argument is continuous under composition wherever its logarithm and denominator are nonsingular.

theorem ContinuousAt.dMinus {E : Type u_1} [TopologicalSpace E] {f g : E → ℝ} {x : E} {r σ K : ℝ} (hf : ContinuousAt f x) (hg : ContinuousAt g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContinuousAt (fun (y : E) => TauCeti.BlackScholes.dMinus (f y) r σ K (g y)) x

The lower Black–Scholes normal argument is continuous under composition on the same domain.

theorem ContinuousAt.callPrice {E : Type u_1} [TopologicalSpace E] {f g : E → ℝ} {x : E} {r σ K : ℝ} (hf : ContinuousAt f x) (hg : ContinuousAt g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContinuousAt (fun (y : E) => TauCeti.BlackScholes.callPrice (f y) r σ K (g y)) x

The closed-form call price is continuous under composition in spot and remaining maturity wherever the normal arguments are nonsingular.

theorem ContinuousAt.putPrice {E : Type u_1} [TopologicalSpace E] {f g : E → ℝ} {x : E} {r σ K : ℝ} (hf : ContinuousAt f x) (hg : ContinuousAt g x) (hs : f x ≠ 0) (hK : K ≠ 0) (hσ : σ ≠ 0) (hτ : 0 < g x) : ContinuousAt (fun (y : E) => TauCeti.BlackScholes.putPrice (f y) r σ K (g y)) x

The closed-form put price is continuous under composition in spot and remaining maturity wherever the normal arguments are nonsingular.