Financial mathematics: one-factor markets and replication
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremThe Black–Scholes call formula#
The discounted risk-neutral expectation of the call payoff
(S_τ - K)⁺ is s Φ(d₊) - K e^{-rτ} Φ(d₋).
TauCeti.BlackScholes.riskNeutralPrice_call {s r σ K τ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hK : 0 < K)
(hτ : 0 < τ) :
TauCeti.BlackScholes.riskNeutralPrice (fun x => (x - K)⁺) s r σ τ =
TauCeti.BlackScholes.callPrice s r σ K τ
Uses 2 · Used by 1
TheoremThe Black–Scholes put formula#
The discounted risk-neutral expectation of the put payoff
(K - S_τ)⁺ is K e^{-rτ} Φ(-d₋) - s Φ(-d₊).
TauCeti.BlackScholes.riskNeutralPrice_put {s r σ K τ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hK : 0 < K)
(hτ : 0 < τ) :
TauCeti.BlackScholes.riskNeutralPrice (fun x => (K - x)⁺) s r σ τ =
TauCeti.BlackScholes.putPrice s r σ K τ
TheoremThe 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.
TauCeti.BlackScholes.callPrice_pde {s r σ K : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) {T t : ℝ}
(ht : t < T) :
deriv (fun u => TauCeti.BlackScholes.callPrice s r σ K (T - u)) t +
σ ^ 2 * s ^ 2 / 2 *
deriv (deriv fun x => TauCeti.BlackScholes.callPrice x r σ K (T - t)) s +
r *
(s * deriv (fun x => TauCeti.BlackScholes.callPrice x r σ K (T - t)) s -
TauCeti.BlackScholes.callPrice s r σ K (T - t)) =
0
Uses 1
TheoremThe 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.
TauCeti.BlackScholes.putPrice_pde {s r σ K : ℝ} (hs : 0 < s) (hK : 0 < K) (hσ : σ ≠ 0) {T t : ℝ}
(ht : t < T) :
deriv (fun u => TauCeti.BlackScholes.putPrice s r σ K (T - u)) t +
σ ^ 2 * s ^ 2 / 2 * deriv (deriv fun x => TauCeti.BlackScholes.putPrice x r σ K (T - t)) s +
r *
(s * deriv (fun x => TauCeti.BlackScholes.putPrice x r σ K (T - t)) s -
TauCeti.BlackScholes.putPrice s r σ K (T - t)) =
0
TheoremPut–call parity for the closed-form prices#
C - P = s - K e^{-rτ}.
TauCeti.BlackScholes.callPrice_sub_putPrice (s r σ K τ : ℝ) :
TauCeti.BlackScholes.callPrice s r σ K τ - TauCeti.BlackScholes.putPrice s r σ K τ =
s - K * Real.exp (-r * τ)
Used by 2
TheoremTauCeti.BlackScholes.deriv_callPrice_spot_mem_Ioo#
The call delta lies strictly between 0 and 1.
TauCeti.BlackScholes.deriv_callPrice_spot_mem_Ioo {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K)
(hσ : σ ≠ 0) (hτ : 0 < τ) :
deriv (fun x => TauCeti.BlackScholes.callPrice x r σ K τ) s ∈ Set.Ioo 0 1
Lean
Formalized in Tau Ceti as TauCeti.BlackScholes.deriv_callPrice_spot_mem_Ioo.
Sources
Uses 1
DefinitionTauCeti.BlackScholes.riskNeutralPrice#
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.
TauCeti.BlackScholes.riskNeutralPrice (h : ℝ → ℝ) (s r σ τ : ℝ) : ℝ
Used by 2
TheoremTauCeti.Probability.setIntegral_exp_mul_gaussianReal#
Integrating the exponential weight exp (t * x) against N(m, v) over a set s gives the
moment-generating function exp (m t + v t² / 2) times the mass of s under the tilted law
N(m + v t, v).
TauCeti.Probability.setIntegral_exp_mul_gaussianReal (m : ℝ) (v : NNReal) (t : ℝ) (s : Set ℝ) :
∫ (x : ℝ) in s, Real.exp (t * x) ∂ProbabilityTheory.gaussianReal m v =
Real.exp (m * t + ↑v * t ^ 2 / 2) * (ProbabilityTheory.gaussianReal (m + ↑v * t) v).real s
Lean
Formalized in Tau Ceti as TauCeti.Probability.setIntegral_exp_mul_gaussianReal.
Sources
TheoremTauCeti.BlackScholes.mul_gaussianPDFReal_dPlus#
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 τ).
TauCeti.BlackScholes.mul_gaussianPDFReal_dPlus {s r σ K τ : ℝ} (hs : 0 < s) (hK : 0 < K)
(hσ : σ ≠ 0) (hτ : 0 < τ) :
s * ProbabilityTheory.gaussianPDFReal 0 1 (TauCeti.BlackScholes.dPlus s r σ K τ) =
K * Real.exp (-r * τ) *
ProbabilityTheory.gaussianPDFReal 0 1 (TauCeti.BlackScholes.dMinus s r σ K τ)
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.