Five implicit functions from the Annuity Equation

The BA II Plus calculator values PMT, I/Y, N, FV, PV can each be computed from the other four.

Main results:

• annuity_equation_unique_solvability
• TVM_equation_unique_solvability: by setting PMT=0 in the annuity equation we obtain unique solution for the Time Value of Money equation as well.

theorem sum_pow (n : ℕ) {x : ℝ} (hx : x ≠ 1) : ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)

The sum of a finite geometric series.

theorem sum_pow_interest (n : ℕ) {i : ℝ} (hi : i ≠ 0) (hi' : 1 + i ≠ 0) : ∑ k ∈ Finset.range (n + 1), (1 + i)⁻¹ ^ k - 1 = (1 - (1 + i)⁻¹ ^ n) / i

theorem sum_Icc_succ_eq_sum_range (f : ℕ → ℝ) (n : ℕ) : f 0 + ∑ k ∈ Finset.Icc 1 n, f k = ∑ k ∈ Finset.range (n + 1), f k

def annuity.geom_sum : ℕ → ℝ → ℝ

The present value of the first n payments of an annuity of 1 per period, with interest rate i. There is a notation clash with the accumulation function a. annuity.a versus a. Etymology: a for annuity.

Equations

• annuity.geom_sum n v = ∑ k ∈ Finset.Icc 1 n, v ^ k

def annuity.id_mul_geom_sum : ℕ → ℝ → ℝ

Equations

• annuity.id_mul_geom_sum n v = ∑ k ∈ Finset.Icc 1 n, ↑k * v ^ k

theorem annuity.id_mul_geom_sum_formula₀ (x : ℝ) (hx : x ≠ 1) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ↑k * x ^ k = x * (↑n * x ^ (n + 1) - (↑n + 1) * x ^ n + 1) / (x - 1) ^ 2

theorem annuity.id_mul_geom_sum_formula (x : ℝ) (hx : x ≠ 1) (n : ℕ) : id_mul_geom_sum n x = x * (↑n * x ^ (n + 1) - (↑n + 1) * x ^ n + 1) / (x - 1) ^ 2

Rename to id_mul_geom_sum_formula

noncomputable def annuity.a : ℕ → ℝ → ℝ

Equations

• annuity.a n i = annuity.geom_sum n (1 + i)⁻¹

theorem annuity.annuity_zero (n : ℕ) : a n 0 = ↑n

noncomputable def annuity.Ia : ℕ → ℝ → ℝ

Increasing annuity.

Equations

• annuity.Ia n i = annuity.id_mul_geom_sum n (1 + i)⁻¹

def annuity.bond_price_sum : ℕ → ℝ → ℝ → ℝ

Equations

• annuity.bond_price_sum n r v = r * annuity.geom_sum n v + v ^ n

noncomputable def annuity.bond_price : ℕ → ℝ → ℝ → ℝ

Price of a bond with unit redemption value, coupon rate r, interest rate i.

Equations

• annuity.bond_price n i r = annuity.bond_price_sum n r (1 + i)⁻¹

theorem annuity.Ia_eq_Ia_formula (n : ℕ) (i : ℝ) (hi : i ≠ 0) : have x := (1 + i)⁻¹; Ia n i = x * (↑n * x ^ (n + 1) - (↑n + 1) * x ^ n + 1) / (x - 1) ^ 2

theorem annuity.annuity_positive {n : ℕ} (hn : n ≠ 0) {i : ℝ} (hi : i > -1) : a n i > 0

The present value of a level-payments annuity with at least one payment is positive.

theorem annuity.geom_sum_positive {n : ℕ} (hnn : n > 1) {i : ℝ} (hi : i > -1) : 0 < geom_sum n (1 + i)⁻¹

theorem annuity.annuity_nonneg (n : ℕ) {i : ℝ} (hi : i > -1) : a n i ≥ 0

The present value of a level-payments annuity is nonnegative.

theorem annuity.bond_price_pos (n : ℕ) {i r : ℝ} (hi : i > -1) (hr : 0 ≤ r) : 0 < bond_price n i r

theorem annuity.increasing_annuity_nonneg (n : ℕ) {i : ℝ} (hi : i > -1) : Ia n i ≥ 0

noncomputable def annuity.s : ℕ → ℝ → ℝ

Future value of an annuity-immediate. s for sum.

Equations

• annuity.s n i = (1 + i) ^ n * annuity.a n i

noncomputable def annuity.a_dots : ℕ → ℝ → ℝ

Present value of an annuity-due. Because double-dot notation is used, we call it a_double_dot or for short a_dots.

Equations

• annuity.a_dots n i = ∑ k ∈ Finset.Ico 0 n, (1 + i)⁻¹ ^ k

noncomputable def annuity.s_dots : ℕ → ℝ → ℝ

Future value of an annuity-due.

Equations

• annuity.s_dots n i = (1 + i) ^ n * annuity.a_dots n i

@[simp]

theorem annuity.annuity_due_interest_zero {n : ℕ} : a_dots n 0 = ↑n

In case of zero interest, the present value of the n payments of 1 is simply n.

@[simp]

theorem annuity.annuity_immediate_interest_zero {n : ℕ} : a n 0 = ↑n

theorem annuity.future_value_annuity_due_interest_zero {n : ℕ} : s_dots n 0 = ↑n

In case of zero interest, the future value of the n payments of 1 is simply n.

noncomputable def annuity.a_formula : ℕ → ℝ → ℝ

Formula for the present value of an annuity-immediate. This formula is only valid when i ≠ 0.

Equations

• annuity.a_formula n i = (1 - (1 + i)⁻¹ ^ n) / i

noncomputable def annuity.Ia_formula : ℕ → ℝ → ℝ

Equations

• annuity.Ia_formula n i = (1 + i)⁻¹ * (↑n * (1 + i)⁻¹ ^ (n + 1) - (↑n + 1) * (1 + i)⁻¹ ^ n + 1) / ((1 + i)⁻¹ - 1) ^ 2

def annuity.duration_equation (n : ℕ) (i r d : ℝ) : Prop

Equations

• annuity.duration_equation n i r d = (d * annuity.bond_price n i r - (r * annuity.Ia n i + ↑n * (1 + i)⁻¹ ^ n) = 0)

noncomputable def annuity.a_variant : ℕ → ℝ → ℝ

Annuities. Another variant.

Equations

• annuity.a_variant n i = ∑ k ∈ Finset.range (n + 1), (1 + i)⁻¹ ^ k - 1

theorem annuity.a_eq_a_variant (n : ℕ) (i : ℝ) : a n i = a_variant n i

theorem annuity.a_eq_a_formula {i : ℝ} (hi : i ≠ 0) (hi' : 1 + i ≠ 0) : (fun (n : ℕ) => a n i) = fun (n : ℕ) => a_formula n i

theorem annuity.annuity_limiting_value {i : ℝ} (hi : 0 < i) : Filter.Tendsto (fun (n : ℕ) => a n i) Filter.atTop (nhds (1 / i))

The value of a perpetuity of 1 per period with interest rate i is 1 / i. For example, if i = 1 we get 1/2 + 1/4 + ... = 1.

theorem annuity.annuity_antitone {N : ℕ} (hN : N ≠ 0) ⦃a b : ℝ⦄ (hab : a < b) (ha : -1 < a) : annuity.a N b < annuity.a N a

theorem annuity.annuity_value_decreasing_with_rising_interest {n : ℕ} {i j : ℝ} (hj : 0 < i) (hij : i ≤ j) : a_formula n j ≤ a_formula n i

The value of an annuity decreases with rising interest.

theorem annuity.annuity_value_pos {i : ℝ} (hi : i > 0) (n : ℕ) (hn : n > 0) : 0 < a_formula n i

theorem annuity.annuity_value_bounded {i : ℝ} (hi : i > 0) (n : ℕ) : a_formula n i ≤ 1 / i

theorem annuity.annuity_value_increasing_with_time {n : ℕ} {i : ℝ} (hi : 0 < i) : a_formula n i ≤ a_formula (n + 1) i

The value of an annuity increases with the number of payments.

def annuity_equation (IY PMT PV FV : ℝ) (N : ℕ) : Prop

The BA II Plus Professional equation.

Equations

• annuity_equation IY PMT PV FV N = (PV + PMT * annuity.a N (IY / 100) + FV * (1 + IY / 100)⁻¹ ^ N = 0)

noncomputable def CPT_PV (IY PMT FV : ℝ) (N : ℕ) : ℝ

Equations

• CPT_PV IY PMT FV N = -PMT * annuity.a N (IY / 100) - FV * (1 + IY / 100)⁻¹ ^ N

noncomputable def CPT_FV (IY PMT PV : ℝ) (N : ℕ) : ℝ

Equations

• CPT_FV IY PMT PV N = (-PV - PMT * annuity.a N (IY / 100)) / (1 + IY / 100)⁻¹ ^ N

noncomputable def CPT_N (IY PMT PV FV : ℝ) : ℝ

Equations

• CPT_N IY PMT PV FV = Real.log ((PV * (IY / 100) + PMT) / (PMT - FV * (IY / 100))) / Real.log (1 + IY / 100)⁻¹

theorem PV_eq_CPT_PV {IY PMT PV FV : ℝ} {N : ℕ} (h : annuity_equation IY PMT PV FV N) : PV = CPT_PV IY PMT FV N

[CPT] [PV] is quite simple:

theorem FV_eq_CPT_FV {IY PMT PV FV : ℝ} {N : ℕ} (h : annuity_equation IY PMT PV FV N) (h₀ : IY ≠ -100) : FV = CPT_FV IY PMT PV N

[CPT] [FV] is simple as long as [I/Y] is not -100:

theorem N_eq_CPT_N {IY PMT PV FV : ℝ} {N : ℕ} (h : annuity_equation IY PMT PV FV N) (h₀ : IY ≠ 0) (h₁ : IY ≠ -100) (h₂ : IY / 100 ≠ -2) (h_nonpar : FV * (IY / 100) - PMT ≠ 0) : ↑N = CPT_N IY PMT PV FV

theorem discount_continuity₀ (k : ℕ) : ContinuousOn (fun (y : ℝ) => (1 + y)⁻¹ ^ k) (Set.Ioi (-1))

theorem discount_continuity {i : ℝ} (k : ℕ) : ContinuousOn (fun (y : ℝ) => (1 + y)⁻¹ ^ k) (Set.Ioc (-1) i)

theorem annuity_continuous {i : ℝ} {N : ℕ} : ContinuousOn (fun (i : ℝ) => annuity.a N i) (Set.Ioc (-1) i)

theorem annuity_equation_continuity {PMT PV FV i : ℝ} {N : ℕ} : ContinuousOn (fun (i : ℝ) => PV + PMT * annuity.a N i + FV * (1 + i)⁻¹ ^ N) (Set.Ioc (-1) i)

theorem of_IY_nonneg {IY PV PMT FV : ℝ} {N : ℕ} (h : annuity_equation IY PMT PV FV N) (hIY : IY ≥ 0) (hPMT : PMT ≥ 0) (hFV : FV > 0) : 0 ≤ PV + PMT * ↑N + FV

We can eliminate the unnatural assumption by going to IY ≥ 0.

theorem CPT_IY_unique.aux {PMT PV FV : ℝ} (hPMT : PMT > 0) (hPV : PV < 0) (hFV : FV > 0) : have ι := 2 * max FV PMT / -PV; PV + PMT * (1 / ι) + FV * (1 + ι)⁻¹ < 0

theorem natpow_rpow (M : ℕ) (x : ℝ) (hx : x > 0) : x ^ M = Real.exp (↑M * Real.log x)

theorem TVM_interest_exists {PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hPV : PV < 0) (h : 0 ≤ PV + FV) : ∃ (i : ℝ), 0 ≤ i ∧ PV + FV * ((1 + i) ^ N)⁻¹ = 0

theorem PV_FV_aux {PV FV : ℝ} (hPV : PV < 0) (hFV : FV > 0) : have ι := 2 * FV / -PV; ι ≥ 0 → PV + FV * (1 + ι)⁻¹ < 0

theorem CPT_IY.concrete.aux₀ {PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hPV : PV < 0) (hFV : FV > 0) : have ι := 2 * FV / -PV; PV + FV * (1 + ι)⁻¹ ^ N < 0

theorem CPT_IY.concrete {PMT PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hPV : PV < 0) (hFV : FV > 0) (H : ¬PMT = 0) : have ι := 2 * max FV PMT / -PV; ι > 0 → PV + PMT * annuity.a N ι + FV * (1 + ι)⁻¹ ^ N < 0

theorem CPT_IY.aux₀ {PMT PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (h : 0 ≤ PV + PMT * ↑N + FV) (hPV : PV < 0) (hFV : FV > 0) : ∃ i ≥ 0, PV + PMT * annuity.a N i + FV * (1 + i)⁻¹ ^ N = 0

Existence of interest rate satisfying annuity equation.

theorem annuity_strictAnti {PMT PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hPMT : PMT ≥ 0) (hFV : FV > 0) : StrictAntiOn (fun (i : ℝ) => PV + PMT * annuity.a N i + FV * (1 + i)⁻¹ ^ N) (Set.Ioi (-1))

theorem CPT_IY_unique {PMT PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hPMT : PMT ≥ 0) (h : 0 ≤ PV + PMT * ↑N + FV) (hPV : PV < 0) (hFV : FV > 0) : ∃ (IY : ℝ), (IY ≥ 0 ∧ annuity_equation IY PMT PV FV N) ∧ ∀ (IY' : ℝ), IY' > -100 ∧ annuity_equation IY' PMT PV FV N → IY' = IY

Unique solution of annuity equation for interest rate, via the Intermediate Value Theorem.

noncomputable def CPT_IY_of_IY_nonneg {PMT PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hPMT : PMT ≥ 0) (h : 0 ≤ PV + PMT * ↑N + FV) (hPV : PV < 0) (hFV : FV > 0) : ℝ

The [CPT] [IY] button combination on the BA II Plus Financial.

Equations

• CPT_IY_of_IY_nonneg hN hPMT h hPV hFV = ⋯.choose

noncomputable def CPT_IY {IY PMT PV FV : ℝ} {N : ℕ} (hann : annuity_equation IY PMT PV FV N) (hN : N ≠ 0) (hPMT : PMT ≥ 0) (hPV : PV < 0) (hFV : FV > 0) (h₀ : IY ≥ 0) : ℝ

Equations

• CPT_IY hann hN hPMT hPV hFV h₀ = CPT_IY_of_IY_nonneg hN hPMT ⋯ hPV hFV

theorem IY_eq_CPT_IY {PMT PV FV IY : ℝ} {N : ℕ} (hN : N ≠ 0) (hPMT : PMT ≥ 0) (h : 0 ≤ PV + PMT * ↑N + FV) (hPV : PV < 0) (hFV : FV > 0) (hann : annuity_equation IY PMT PV FV N) (h₀ : IY > -100) : IY = CPT_IY_of_IY_nonneg hN hPMT h hPV hFV

[CPT] [IY] gives the only solution for interest rate per year.

noncomputable def CPT_PMT (IY PV FV : ℝ) (N : ℕ) : ℝ

Equations

• CPT_PMT IY PV FV N = (-PV - FV * (1 + IY / 100)⁻¹ ^ N) / annuity.a N (IY / 100)

theorem PMT_eq_CPT_PMT.aux {IY : ℝ} {N : ℕ} (h₀ : IY > -100) (hN : N ≠ 0) (h₂ : (100 / (100 + IY)) ^ N = 1 ^ N) : 100 / (100 + IY) = 1

theorem PMT_eq_CPT_PMT {IY PMT PV FV : ℝ} {N : ℕ} (h : annuity_equation IY PMT PV FV N) (h₀ : IY > -100) (hN : N ≠ 0) : PMT = CPT_PMT IY PV FV N

[CPT] [PMT] gives the only solution for payment.

theorem annuity_equation_unique_solvability {IY PMT PV FV : ℝ} {N : ℕ} (hann : annuity_equation IY PMT PV FV N) (hPMT : PMT ≥ 0) (hPV : PV < 0) (hFV : FV > 0) (hIY : IY > 0) : (∀ (hN : N ≠ 0), PMT = CPT_PMT IY PV FV N ∧ IY = CPT_IY hann hN hPMT hPV hFV ⋯) ∧ PV = CPT_PV IY PMT FV N ∧ FV = CPT_FV IY PMT PV N ∧ (FV * (IY / 100) - PMT ≠ 0 → ↑N = CPT_N IY PMT PV FV)

Main theorem on unique solvability of the Annuity Equation. To deduce interest rate we need time to pass, and hence the number of periods N>0. To deduce the payment there must be at least one payment, and hence again N>0. To deduce N, the coupon rate should not equal the yield rate and hence FV * (IY / 100) - PMT ≠ 0. These assumptions, together with appropriate positivity and negativity, suffice for unique existence of all variables.

theorem TVM_equation_unique_solvability {IY PV FV : ℝ} {N : ℕ} (hann : annuity_equation IY 0 PV FV N) (hPV : PV < 0) (hFV : FV > 0) (hIY : IY > 0) : (∀ (hN : N ≠ 0), 0 = CPT_PMT IY PV FV N ∧ IY = CPT_IY hann hN ⋯ hPV hFV ⋯) ∧ PV = CPT_PV IY 0 FV N ∧ FV = CPT_FV IY 0 PV N ∧ ↑N = CPT_N IY 0 PV FV

By setting PMT=0 we obtain the unique solvability of the Time Value of Money equation.

theorem CPT_IY_satisfies {PV PMT FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hFV : FV > 0) (hPV : PV < 0) (hPMT : PMT ≥ 0) (h : 0 ≤ PV + PMT * ↑N + FV) : have hann := ⋯; have IY := CPT_IY ⋯ hN hPMT hPV hFV ⋯; annuity_equation IY PMT PV FV N

CPT_IY returns a value satisfying the annuity equation.

theorem CPT_IY_satisfies_iff {PV PMT FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hFV : FV > 0) (hPV : PV < 0) (hPMT : PMT ≥ 0) : 0 ≤ PV + PMT * ↑N + FV ↔ ∃ IY ≥ 0, annuity_equation IY PMT PV FV N

theorem CPT_N_satisfies {IY PMT PV FV : ℝ} (N : ℕ) (hIY₁ : IY / 100 > 0) (h_nonpar : PMT - FV * (IY / 100) ≠ 0) (hNat : ↑N = CPT_N IY PMT PV FV) : 0 < (PV * (IY / 100) + PMT) / (PMT - FV * (IY / 100)) ↔ annuity_equation IY PMT PV FV N

If CPT_N returns a Nat then it satisfies the annuity equation. (If it doesn't, we could prove it satisfies a modified annuity equation.)

theorem CPT_PV_satisfies {IY PMT FV : ℝ} {N : ℕ} : annuity_equation IY PMT (CPT_PV IY PMT FV N) FV N

theorem CPT_FV_satisfies {IY PMT PV : ℝ} {N : ℕ} (hIY : IY > -100) : annuity_equation IY PMT PV (CPT_FV IY PMT PV N) N

theorem CPT_PMT_satisfies {IY PV FV : ℝ} {N : ℕ} (hN : N ≠ 0) (hIY : IY > -100) : annuity_equation IY (CPT_PMT IY PV FV N) PV FV N

theorem CPT_PMT_satisfies_when_PV_eq_zero {FV PMT : ℝ} {N : ℕ} (hN : N ≠ 0) : annuity_equation (-100) PMT 0 FV N

If PV=0 and i=-1, the annuity equation holds for PMT = CPT_PMT or any other PMT value.