Chan & Tse Exercise 1.1

Chan & Tse Exercise 1.2

theorem neg_log {w : ℝ} (h₂ : w ≠ 0) (this : 1 - w > 0) : w < -Real.log (1 - w)

Here we develop interest theory, taking the force of interest δ as basic.

noncomputable def force.a_sub (δ : ℝ → ℝ) (t τ : ℝ) : ℝ

Equations

• force.a_sub δ t τ = Real.exp (∫ (s : ℝ) in t..t + τ, δ s)

noncomputable def force.a (δ : ℝ → ℝ) (t : ℝ) : ℝ

Equations

• force.a δ t = force.a_sub δ 0 t

noncomputable def force.A (δ : ℝ → ℝ) (A₀ : ℝ) : ℝ → ℝ

Equations

• force.A δ A₀ t = force.a δ t * A₀

theorem a_zero (δ : ℝ → ℝ) : force.a_sub δ 0 0 = 1

theorem a_zero' (δ : ℝ → ℝ) : force.a δ 0 = 1

In name space interest, a(0)=1 was not automatic but here it is:

Interest namespace will clash with annuity namespaces since they use a for different things.

def interest.A (A₀ : ℝ) (a : ℝ → ℝ) : ℝ → ℝ

Equations

• interest.A A₀ a t = a t * A₀

theorem interest.A_def (A₀ : ℝ) (a : ℝ → ℝ) (t : ℝ) : A A₀ a t = a t * A₀

def interest.I (A₀ : ℝ) (a : ℝ → ℝ) : ℝ → ℝ

Equations

• interest.I A₀ a t = (a t - a (t - 1)) * A₀

noncomputable def interest.i₂ (a : ℝ → ℝ) : ℝ → ℝ → ℝ

Effective interest over an interval, not annualized. i₂ u v = (a v - a u) / (a u) This should be used when u ≤ v. See Chan & Tse (1.15).

One can prove that the limit of i₂ u (u + h) / h as h → 0 is a' u / a u: (a (u+h) - a u) / (h * (a u))

Equations

• interest.i₂ a u v = a v / a u - 1

noncomputable def interest.δ (a : ℝ → ℝ) : ℝ → ℝ

Force of interest with not necessarily constant interest rates.

Equations

• interest.δ a u = deriv a u / a u

noncomputable def interest.i₂ann (a : ℝ → ℝ) : ℝ → ℝ → ℝ

Annualized effective interest over an interval. Equation (1.13) in Chan & Tse.

Equations

• interest.i₂ann a u v = (a v / a u) ^ (1 / (v - u)) - 1

noncomputable def interest.iF (a : ℝ → ℝ) : ℝ → ℝ → ℝ

Equations

• interest.iF a t τ = interest.i₂ann a t (t + τ)

noncomputable def interest.i (a : ℝ → ℝ) : ℝ → ℝ

The effective interest rate function i(t) is defined so that a t = (1 + i t) * a (t - 1).

Equations

• interest.i a t = interest.i₂ a (t - 1) t

noncomputable def interest.v (a : ℝ → ℝ) : ℝ → ℝ

Equations

• interest.v a t = 1 / a t

theorem interest.chan_tse_exe_1_33 (a : ℝ → ℝ) (h : ∀ (t : ℝ), a t = 1 / (1 - 1e-2 * t)) (t : ℝ) : v a t = 1 - 1e-2 * t

theorem interest.eq_of_deriv_eq (f g : ℝ → ℝ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) (h : deriv f = deriv g) (h₀ : f 0 = g 0) : f = g

theorem interest.solutions_of_deriv_eq_self {f : ℝ → ℝ} (hf : Differentiable ℝ f) (h : ∀ (x : ℝ), deriv f x = f x) : ∃ (c : ℝ), ∀ (x : ℝ), f x = c * Real.exp x

theorem interest.edist_mul {c : ℝ} (hδ : 0 ≤ c) (x y : ℝ) : edist (c * x) (c * y) = ENNReal.ofReal c * edist x y

theorem interest.general_force (a : ℝ → ℝ) (hnz : ∀ (t : ℝ), a t ≠ 0) (hdiff : Differentiable ℝ a) (ha₀ : a 0 = 1) {n : ℝ} (hn : 0 ≤ n) (hcontδ : ContinuousOn (δ a) (Set.Ici 0)) (hδ : ∀ t ≥ 0, 0 < δ a t ∧ δ a t ≤ 1) (hc₀ : ContinuousAt (δ a) 0) (hme : StronglyMeasurableAtFilter (δ a) (nhds 0) MeasureTheory.volume) : Set.EqOn (fun (t : ℝ) => Real.exp (∫ (s : ℝ) in 0..t, δ a s)) a (Set.Icc 0 n)

The equation a(t) = e^(∫^t δ(s) ds).

theorem interest.this_is_proved_instead₀ (a : ℝ → ℝ) (h : δ a = fun (t : ℝ) => 1 / (10 * (1 + t) ^ 3)) (hnz : ∀ (t : ℝ), a t ≠ 0) (hdiff : Differentiable ℝ a) (ha₀ : a 0 = 1) (n : ℝ) (hn : 0 ≤ n) : Set.EqOn (fun (t : ℝ) => Real.exp (∫ (s : ℝ) in 0..t, δ a s)) a (Set.Icc 0 n)

theorem interest.this_is_proved_instead (a : ℝ → ℝ) (h : δ a = fun (t : ℝ) => 1 / (10 * (1 + t) ^ 3)) (hnz : ∀ (t : ℝ), a t ≠ 0) (hdiff : Differentiable ℝ a) (ha₀ : a 0 = 1) : Set.EqOn (fun (t : ℝ) => Real.exp (∫ (s : ℝ) in 0..t, δ a s)) a (Set.Ici 0)

theorem interest.integral_one_div_ten_one_add_pow_three_0_to_5 : ∫ (s : ℝ) in 0..5, 1 / (10 * (1 + s) ^ 3) = 1 / 20 * (1 - 1 / 36)

theorem interest.integral_one_div_ten_one_add_pow_three_0_to_4 : ∫ (s : ℝ) in 0..4, 1 / (10 * (1 + s) ^ 3) = 1 / 20 * (1 - 1 / 25)

theorem interest.chan_tse_exe_1_36 (A₀ : ℝ) (a : ℝ → ℝ) (h : δ a = fun (t : ℝ) => 1 / (10 * (1 + t) ^ 3)) (h₀ : A₀ = 100) (hnz : ∀ (t : ℝ), a t ≠ 0) (hdiff : Differentiable ℝ a) (ha₀ : a 0 = 1) : I A₀ a 5 ∈ Set.Ioo 64e-3 65e-3