The Black–Scholes Greeks and the Black–Scholes equation

This file differentiates the closed-form Black–Scholes prices C = s Φ(d₊) - K e^{-rτ} Φ(d₋) and P = K e^{-rτ} Φ(-d₋) - s Φ(-d₊) of TauCeti.Probability.Finance.BlackScholes.Basic in the spot s, the remaining maturity τ and the volatility σ, and shows that both prices solve the Black–Scholes equation. Here Φ is the standard Gaussian cdf and φ = gaussianPDFReal 0 1 its density.

Everything rests on the identity s φ(d₊) = K e^{-rτ} φ(d₋) (TauCeti.BlackScholes.mul_gaussianPDFReal_dPlus, proved with the formulas), which says that the terms produced by differentiating d₊ and d₋ cancel. With it the Greeks of the call are

• delta ∂C/∂s = Φ(d₊), which lies in (0, 1);
• gamma ∂²C/∂s² = φ(d₊) / (s σ √τ), positive for σ > 0;
• ∂C/∂τ = s φ(d₊) σ / (2 √τ) + r K e^{-rτ} Φ(d₋);
• vega ∂C/∂σ = s φ(d₊) √τ, which is positive.

The put has delta -Φ(-d₊) ∈ (-1, 0), the same gamma and vega, and ∂P/∂τ = s φ(d₊) σ / (2 √τ) - r K e^{-rτ} Φ(-d₋).

In calendar time t = T - τ both V(s, t) = C(s, T - t) and V(s, t) = P(s, T - t) satisfy

∂V/∂t + σ² s² / 2 ∂²V/∂s² + r (s ∂V/∂s - V) = 0

for s > 0 and t < T (TauCeti.BlackScholes.callPrice_pde, TauCeti.BlackScholes.putPrice_pde). The formulas for the derivatives and the equation only need σ ≠ 0; the signs of gamma need σ > 0.

Main declarations

• TauCeti.BlackScholes.hasDerivAt_callPrice_spot — the call delta.
• TauCeti.BlackScholes.hasDerivAt_deriv_callPrice_spot — the call gamma.
• TauCeti.BlackScholes.hasDerivAt_callPrice_maturity — the derivative of the call in τ.
• TauCeti.BlackScholes.hasDerivAt_callPrice_volatility — the call vega.
• TauCeti.BlackScholes.deriv_callPrice_spot_mem_Ioo — 0 < ∂C/∂s < 1.
• The corresponding putPrice statements.
• TauCeti.BlackScholes.abs_callPrice_sub_callPrice_le — the call is 1-Lipschitz in the spot on s > 0 (for τ > 0, σ ≠ 0, K > 0).
• TauCeti.BlackScholes.callPrice_pde, TauCeti.BlackScholes.putPrice_pde — the Black–Scholes equation.

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, §4.5.

Derivatives of d₊ and d₋ in the spot

Greeks of the call

theorem TauCeti.BlackScholes.hasDerivAt_callPrice_spot {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (fun (x : ℝ) => callPrice x r σ K τ) (↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (dPlus s r σ K τ)) s

Call delta. The derivative of the Black–Scholes call price in the spot is Φ(d₊).

@[simp]

theorem TauCeti.BlackScholes.deriv_callPrice_spot {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : deriv (fun (x : ℝ) => callPrice x r σ K τ) s = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (dPlus s r σ K τ)

Call delta. The derivative of the Black–Scholes call price in the spot is Φ(d₊).

theorem TauCeti.BlackScholes.deriv_callPrice_spot_mem_Ioo {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : deriv (fun (x : ℝ) => callPrice x r σ K τ) s ∈ Set.Ioo 0 1

The call delta lies strictly between 0 and 1.

theorem TauCeti.BlackScholes.abs_callPrice_sub_callPrice_le {s r σ K τ x : ℝ} (hx : 0 < x) (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : |callPrice x r σ K τ - callPrice s r σ K τ| ≤ |x - s|

The Black–Scholes call price is 1-Lipschitz in the spot on s > 0, for τ > 0, σ ≠ 0 and K > 0.

theorem TauCeti.BlackScholes.hasDerivAt_deriv_callPrice_spot {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (deriv fun (x : ℝ) => callPrice x r σ K τ) (ProbabilityTheory.gaussianPDFReal 0 1 (dPlus s r σ K τ) / (s * (σ * √τ))) s

Call gamma. The second derivative of the Black–Scholes call price in the spot is φ(d₊) / (s σ √τ).

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

Call gamma is positive when the volatility is.

theorem TauCeti.BlackScholes.hasDerivAt_callPrice_maturity {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (callPrice s r σ K) (s * ProbabilityTheory.gaussianPDFReal 0 1 (dPlus s r σ K τ) * σ / (2 * √τ) + r * K * Real.exp (-r * τ) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (dMinus s r σ K τ)) τ

The derivative of the Black–Scholes call price in the remaining maturity is s φ(d₊) σ / (2 √τ) + r K e^{-rτ} Φ(d₋).

theorem TauCeti.BlackScholes.hasDerivAt_callPrice_volatility {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (fun (v : ℝ) => callPrice s r v K τ) (s * ProbabilityTheory.gaussianPDFReal 0 1 (dPlus s r σ K τ) * √τ) σ

Call vega. The derivative of the Black–Scholes call price in the volatility is s φ(d₊) √τ.

theorem TauCeti.BlackScholes.deriv_callPrice_volatility_pos {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : 0 < deriv (fun (v : ℝ) => callPrice s r v K τ) σ

Call vega is positive.

Greeks of the put

theorem TauCeti.BlackScholes.hasDerivAt_putPrice_spot {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (fun (x : ℝ) => putPrice x r σ K τ) (-↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-dPlus s r σ K τ)) s

Put delta. The derivative of the Black–Scholes put price in the spot is -Φ(-d₊).

@[simp]

theorem TauCeti.BlackScholes.deriv_putPrice_spot {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : deriv (fun (x : ℝ) => putPrice x r σ K τ) s = -↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-dPlus s r σ K τ)

Put delta. The derivative of the Black–Scholes put price in the spot is -Φ(-d₊).

theorem TauCeti.BlackScholes.deriv_putPrice_spot_mem_Ioo {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : deriv (fun (x : ℝ) => putPrice x r σ K τ) s ∈ Set.Ioo (-1) 0

The put delta lies strictly between -1 and 0.

theorem TauCeti.BlackScholes.hasDerivAt_deriv_putPrice_spot {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (deriv fun (x : ℝ) => putPrice x r σ K τ) (ProbabilityTheory.gaussianPDFReal 0 1 (dPlus s r σ K τ) / (s * (σ * √τ))) s

Put gamma. The second derivative of the Black–Scholes put price in the spot is φ(d₊) / (s σ √τ), the call gamma.

theorem TauCeti.BlackScholes.deriv_deriv_putPrice_spot {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : deriv (deriv fun (x : ℝ) => putPrice x r σ K τ) s = deriv (deriv fun (x : ℝ) => callPrice x r σ K τ) s

Put gamma equals call gamma.

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

Put gamma is positive when the volatility is.

theorem TauCeti.BlackScholes.hasDerivAt_putPrice_maturity {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (putPrice s r σ K) (s * ProbabilityTheory.gaussianPDFReal 0 1 (dPlus s r σ K τ) * σ / (2 * √τ) - r * K * Real.exp (-r * τ) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-dMinus s r σ K τ)) τ

The derivative of the Black–Scholes put price in the remaining maturity is s φ(d₊) σ / (2 √τ) - r K e^{-rτ} Φ(-d₋).

theorem TauCeti.BlackScholes.hasDerivAt_putPrice_volatility {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : HasDerivAt (fun (v : ℝ) => putPrice s r v K τ) (s * ProbabilityTheory.gaussianPDFReal 0 1 (dPlus s r σ K τ) * √τ) σ

Put vega. The derivative of the Black–Scholes put price in the volatility is s φ(d₊) √τ, the call vega.

theorem TauCeti.BlackScholes.deriv_putPrice_volatility_pos {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) (hτ : 0 < τ) : 0 < deriv (fun (v : ℝ) => putPrice s r v K τ) σ

Put vega is positive.

The Black–Scholes equation

theorem TauCeti.BlackScholes.callPrice_pde {s r σ K : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) {T t : ℝ} (ht : t < T) : deriv (fun (u : ℝ) => callPrice s r σ K (T - u)) t + σ ^ 2 * s ^ 2 / 2 * deriv (deriv fun (x : ℝ) => callPrice x r σ K (T - t)) s + r * (s * deriv (fun (x : ℝ) => callPrice x r σ K (T - t)) s - callPrice s r σ K (T - t)) = 0

The Black–Scholes equation for the call. In calendar time t < T, the call price C(s, t) = callPrice s r σ K (T - t) satisfies ∂C/∂t + σ² s² / 2 ∂²C/∂s² + r (s ∂C/∂s - C) = 0 at every spot s > 0.

theorem TauCeti.BlackScholes.putPrice_pde {s r σ K : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) {T t : ℝ} (ht : t < T) : deriv (fun (u : ℝ) => putPrice s r σ K (T - u)) t + σ ^ 2 * s ^ 2 / 2 * deriv (deriv fun (x : ℝ) => putPrice x r σ K (T - t)) s + r * (s * deriv (fun (x : ℝ) => putPrice x r σ K (T - t)) s - putPrice s r σ K (T - t)) = 0

The Black–Scholes equation for the put. In calendar time t < T, the put price P(s, t) = putPrice s r σ K (T - t) satisfies ∂P/∂t + σ² s² / 2 ∂²P/∂s² + r (s ∂P/∂s - P) = 0 at every spot s > 0.