Five implicit functions from the Annuity Equation: duration version

The BA II Plus calculator values PMT, I/Y, N, FV, PV can each be computed from the other four. Here we replace PV by D (duration) for a speculative future calculator.

Main results:

• eq_CPT_I_of_D: if D>1, n ≥ 2, and r>0 then we can uniquely compute the yield rate i > -1 from the duration equation.
• eq_CPT_N_of_D: if i,d,r>0 and d<1+1/i then we can uniquely compute n from the duration equation.

-- * If d>1, n≥2, r>0, i>0 and d<1+1/i then i and n are both computed from -- the others.

noncomputable def D : ℕ → ℝ → ℝ → ℝ

Macaulay duration of a maturity n, level-payments bond (with redemption value 1) with coupon rate r and yield rate i.

Equations

• D n i r = (r * annuity.Ia n i + ↑n * (1 + i)⁻¹ ^ n) / annuity.bond_price n i r

theorem D_one {i r : ℝ} (hi : i > -1) (hr : r ≥ 0) : D 1 i r = 1

A bond with unit redemption value and maturity 1 has Macaulay duration 1.

theorem D_duration_equation (n : ℕ) {i r : ℝ} (hi : i > -1) (hr : r ≥ 0) : annuity.duration_equation n i r (D n i r)

The Macaulay duration does indeed satisfy the duration equation.

theorem D_upper_bound (n : ℕ) {i r : ℝ} (hi : i > -1) (hr : r ≥ 0) : D n i r ≤ ↑n

The maturity date as a trivial upper bound on the Macaulay duration.

theorem D_upper_bound_strict (n : ℕ) (hn : n ≥ 2) {i r : ℝ} (hi : i > -1) (hr : r > 0) : D n i r < ↑n

theorem duration_nonneg (n : ℕ) {i r : ℝ} (hi : i > -1) (hr : r ≥ 0) : 0 ≤ D n i r

The duration of a bond is nonnegative.

theorem par_bond_price (n : ℕ) {i : ℝ} (hi : i > 0) : annuity.bond_price n i i = 1

An at-par bond with unit (1) redemption value has price 1 as well, no matter what the maturity and interest rates are.

noncomputable def CPT_N_of_D_par (i d : ℝ) : ℝ

The maturity of an at-par bond with rate i and Macaulay duration d. Note that the input to log is only positive if d < 1 + 1 / i.

Equations

• CPT_N_of_D_par i d = Real.log (1 - d * (1 - (1 + i)⁻¹)) / Real.log (1 + i)⁻¹

theorem eq_CPT_N_of_D_par (n : ℕ) {i : ℝ} (hi : i > 0) (d : ℝ) (h : annuity.duration_equation n i i d) : ↑n = CPT_N_of_D_par i d

Determine the maturity from the duration for an at-par bond.

theorem increasing_annuity_zero {n : ℕ} : annuity.Ia n 0 = (↑n + 1) * ↑n / 2

Present value of an increasing annuity with interest rate 0.

theorem duration_yield_zero {n : ℕ} (hn : n ≠ 0) {d r : ℝ} (hr : 0 ≤ r) (h : annuity.duration_equation n 0 r d) : d = (r * (↑n + 1) * ↑n / 2 + ↑n) / (r * ↑n + 1)

A pleasant formula for the Macaulay duration of a zero-yield bond in terms of the coupon rate r and maturity n. Note that when r=0 it reduces to d=n.

theorem annuity_bond_price_ne_zero {n : ℕ} (hnn : n > 1) {i r : ℝ} (hi : i > -1) (hr : r ≥ 0) : annuity.bond_price n i r ≠ 0

theorem eq_D_of_duration_equation {n : ℕ} (hnn : n > 1) {i d r : ℝ} (hi : i > -1) (hr : r ≥ 0) (hann : annuity.duration_equation n i r d) : d = D n i r

theorem duration_bounded_by_maturity {n : ℕ} (hnn : n > 1) {i d r : ℝ} (hi : i > -1) (hr : r ≥ 0) (hann : annuity.duration_equation n i r d) : d ≤ ↑n

theorem eq_CPT_I_of_D_maturity2 {i d r : ℝ} (hi : i > -1) (hd : 1 ≠ d) (hri : r > 0) (h : annuity.duration_equation 2 i r d) : i = (2 - d) * (r + 1) / ((d - 1) * r) - 1

For a bond with maturity n=2, explicitly find the yield rate i from the Macaulay duration d and the coupon rate r. For larger n it is not generally uniquely solvable. n=3 might be an interesting quadratic equation. Note that if i=r, (d-1)r = 2-d, i.e., i = (2-d)/(d-1).

theorem deriv_bond_price_sum {n : ℕ} (r x : ℝ) : deriv (annuity.bond_price_sum n r) x = r * ∑ k ∈ Finset.Icc 1 n, ↑k * x ^ (k - 1) + ↑n * x ^ (n - 1)

theorem eq_CPT_I_of_D {n : ℕ} (hnn : n ≥ 2) {i d r : ℝ} (hd : d ∈ Set.Ioo 1 ↑n) (hr : r > 0) : ∃! i : ℝ, i > -1 ∧ annuity.duration_equation n i r d

Inferring the interest rate from the maturity, duration, and coupon rate. With great help from Aristotle.

theorem eq_CPT_N_of_D.helper₀ {n : ℕ} (hnn : n > 1) {i r : ℝ} (hi : i > 0) (hri : r ≥ i) : (r * ∑ k ∈ Finset.Icc 1 n, ↑k * (1 + i)⁻¹ ^ k + ↑n * (1 + i)⁻¹ ^ n) / (r * ∑ k ∈ Finset.Icc 1 n, (1 + i)⁻¹ ^ k + (1 + i)⁻¹ ^ n) < 1 + 1 / i

Aristotle's proof.

theorem eq_CPT_N_of_D.helper {n : ℕ} (hnn : n > 1) {i d r : ℝ} (hi : i > 0) (hri : r ≥ i) (hann : annuity.duration_equation n i r d) : d < 1 + 1 / i

Incorporate Aristotle's inequality_proof into our setting.

noncomputable def CPT_N_of_D {i d r : ℝ} (hd : 0 < d) (hi : i > 0) (hr : r > 0) (hdi : d < 1 + 1 / i) : ℝ

This version does not assume r<i or r>i.

Equations

• CPT_N_of_D hd hi hr hdi = Exists.choose ⋯

theorem equation_presented_to_aristotle {n : ℕ} {i d r : ℝ} (hi : i > 0) (hann : annuity.duration_equation n i r d) : d * (r * ((1 - (1 + i)⁻¹ ^ ↑n) / i) + (1 + i)⁻¹ ^ ↑n) - (r * ((1 + i)⁻¹ * (↑n * (1 + i)⁻¹ ^ (↑n + 1) - (↑n + 1) * (1 + i)⁻¹ ^ ↑n + 1) / ((1 + i)⁻¹ - 1) ^ 2) + ↑n * (1 + i)⁻¹ ^ ↑n) = 0

A temporary lemma to prove that the equation presented to Aristotle is indeed the duration equation.

theorem eq_CPT_N_of_D {n : ℕ} (hnn : ↑n > 0) {i d r : ℝ} (hd : 0 < d) (hi : 0 < i) (hr : 0 < r) (hdi : d < 1 + 1 / i) (hann : annuity.duration_equation n i r d) : ↑n = CPT_N_of_D hd hi hr hdi