Annuity present value as an equivalence

theorem yield_exists.x {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : ε ≤ ↑m) ⦃x : ℝ⦄ (hx₀ : (↑m)⁻¹ ≤ 1 + x) : -1 < x

theorem yield_exists.y {n : ℕ} (hn : n ≠ 0) {ε i : ℝ} (hi : annuity.a n i = ε) (hin : -1 < i) (y : ℝ) : -1 < y → ε = annuity.a n y → y = i

theorem yield_exists.sum {n : ℕ} (hn : n ≠ 0) (hnr : ↑n ≥ 1) : ∑ k ∈ Finset.Icc 1 n, (2 * ↑n)⁻¹ ^ k ≤ ∑ x ∈ Finset.Icc 1 n, (2 * ↑n)⁻¹

theorem yield_exists.bound {n : ℕ} (hn : n ≠ 0) {ε : ℝ} (hε : 0 < ε) (hnr : ↑n ≥ 1) (hnr₀ : n > 0) (H : ε < 1) : (2 * ↑n / ε)⁻¹ ≤ 1

theorem le_geom_self {n : ℕ} (hnr : ↑n ≥ 1) (m : ℕ) (hm : m ≥ 1) : ↑m ≤ ∑ k ∈ Finset.Icc 1 n, ↑m ^ k

theorem yield_exists.small_epsilon {n : ℕ} (hn : n ≠ 0) {ε : ℝ} (hε : 0 < ε) (hnr : ↑n ≥ 1) (hnr₀ : ↑n > 0) (hnn₀ : n > 0) (H : ε < 1) : ∃! i : ℝ, i > -1 ∧ ε = annuity.a n i

noncomputable def yield_exists {n : ℕ} (hn : n ≠ 0) {ε : ℝ} (hε : 0 < ε) : ∃! i : ℝ, i > -1 ∧ ε = annuity.a n i

Equations

• ⋯ = ⋯

noncomputable def yield {n : ℕ} (hn : n ≠ 0) : ↑(Set.Ioi 0) → ℝ

Inverse of the annuity function.

Equations

• yield hn ε = Exists.choose ⋯

noncomputable def annuity_equivalence (n : ℕ) (hn : n ≥ 2) : ↑(Set.Ioi (-1)) ≃ ↑(Set.Ioi 0)

Now we can rename yield to annuity_equivalence.invFun

Equations

• annuity_equivalence n hn = { toFun := fun (i : ↑(Set.Ioi (-1))) => ⟨annuity.a n ↑i, ⋯⟩, invFun := fun (x : ↑(Set.Ioi 0)) => ⟨yield ⋯ x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem yield_zero {n : ℕ} (hn : n ≥ 2) (hd : 0 < ↑n - 1) : have hn₀ := ⋯; yield hn₀ ⟨↑n - 1, hd⟩ = 0

If the value of an annuity is n-1 then the yield interest rate i must have been 0.

theorem duration_coupon_zero {n : ℕ} {d i : ℝ} (hr : -1 < i) (h : annuity.duration_equation n i 0 d) : d = ↑n

A bond with coupon zero has duration equal to maturity.

theorem eq_CPT_I_of_D_par {n : ℕ} (hn : n ≥ 2) {i : ℝ} (hi : i > -1) {d : ℝ} (hd : 0 < d - 1) (h : annuity.duration_equation n i i d) : have hn₀ := ⋯; yield hn₀ ⟨d - 1, hd⟩ = i

Perhaps surprisingly: Let i be the implied interest rate for an n-period par bond of duration d. Then the PV of an (n-1)-period unit-payment annuity with rate i is d-1. This lets us compute i from n and d.