Theory Interest

theory Interest
  imports Preliminaries
begin

section ‹Theory of Interest›

locale interest =
  fixes i :: real  ― ‹‹i› stands for an interest rate.›
  assumes v_futr_pos: "1 + i > 0"  ― ‹Assume that the future value is positive.›
begin

definition i_nom :: "nat ⇒ real" ("$i^{_}" [0] 200)
  where "$i^{m} ≡ m * ((1+i).^(1/m) - 1)"  ― ‹nominal interest rate›

definition i_force :: real ("$δ" 200)
  where "$δ ≡ ln (1+i)" ― ‹force of interest›

definition d_nom :: "nat ⇒ real" ("$d^{_}" [0] 200)
  where "$d^{m} ≡ $i^{m} / (1 + $i^{m}/m)"  ― ‹discount rate› 

abbreviation d_nom_yr :: real ("$d" 200)
  where "$d ≡ $d^{1}"  ― ‹Post-fix ‹yr› stands for "year".›

definition v_pres :: real ("$v" 200)
  where "$v ≡ 1 / (1+i)"  ― ‹present value factor›

definition ann :: "nat ⇒ nat ⇒ real" ("$a^{_}'__" [0,101] 200)
  where "$a^{m}_n ≡ ∑k<n*m. $v.^((k+1::nat)/m) / m"
    ― ‹present value of an immediate annuity›

abbreviation ann_yr :: "nat ⇒ real" ("$a'__" [101] 200)
  where "$a_n ≡ $a^{1}_n"

definition acc :: "nat ⇒ nat ⇒ real" ("$s^{_}'__" [0,101] 200)
  where "$s^{m}_n ≡ ∑k<n*m. (1+i).^((k::nat)/m) / m"
    ― ‹future value of an immediate annuity›
    ― ‹The name ‹acc› stands for "accumulation".›

abbreviation acc_yr :: "nat ⇒ real" ("$s'__" 200)
  where "$s_n ≡ $s^{1}_n"

definition ann_due :: "nat ⇒ nat ⇒ real" ("$a''''^{_}'__" [0,101] 200)
  where "$a''^{m}_n ≡ ∑k<n*m. $v.^((k::nat)/m) / m"
    ― ‹present value of an annuity-due›

abbreviation ann_due_yr :: "nat ⇒ real" ("$a'''''__" [101] 200)
  where "$a''_n ≡ $a''^{1}_n"

definition acc_due :: "nat ⇒ nat ⇒ real" ("$s''''^{_}'__" [0,101] 200)
  where "$s''^{m}_n ≡ ∑k<n*m. (1+i).^((k+1::nat)/m) / m"
    ― ‹future value of an annuity-due›

abbreviation acc_due_yr :: "nat ⇒ real" ("$s'''''__" [101] 200)
  where "$s''_n ≡ $s''^{1}_n"

definition ann_cont :: "real ⇒ real" ("$a'''__" [101] 200)
  where "$a'_n ≡ integral {0..n} (λt::real. $v.^t)"
    ― ‹present value of a continuous annuity›

definition acc_cont :: "real ⇒ real" ("$s'''__" [101] 200)
  where "$s'_n ≡ integral {0..n} (λt::real. (1+i).^t)"
    ― ‹future value of a continuous annuity›

definition perp :: "nat ⇒ real" ("$a^{_}'_∞" [0] 200)
  where "$a^{m}_∞ ≡ 1 / $i^{m}"
    ― ‹present value of a perpetual annuity›

abbreviation perp_yr :: real ("$a'_∞" 200)
  where "$a_∞ ≡ $a^{1}_∞"

definition perp_due :: "nat ⇒ real" ("$a''''^{_}'_∞" [0] 200)
  where "$a''^{m}_∞ ≡ 1 / $d^{m}"
    ― ‹present value of a perpetual annuity-due›

abbreviation perp_due_yr :: real ("$a'''''_∞" 200)
  where "$a''_∞ ≡ $a''^{1}_∞"

definition ann_incr :: "nat ⇒ nat ⇒ nat ⇒ real" ("$'(I^{_}a')^{_}'__" [0,0,101] 200)
  where "$(I^{l}a)^{m}_n ≡ ∑k<n*m. $v.^((k+1::nat)/m) * ⌈l*(k+1::nat)/m⌉ / (l*m)"
    ― ‹present value of an increasing annuity›
    ― ‹This is my original definition.›
    ― ‹Here, ‹l› represents the number of increments per unit time.›

abbreviation ann_incr_lvl :: "nat ⇒ nat ⇒ real" ("$'(Ia')^{_}'__" [0,101] 200)
  where "$(Ia)^{m}_n ≡ $(I^{1}a)^{m}_n"
    ― ‹The post-fix ‹lvl› stands for "level".›

abbreviation ann_incr_yr :: "nat ⇒ real" ("$'(Ia')'__" [101] 200)
  where "$(Ia)_n ≡ $(Ia)^{1}_n"

definition acc_incr :: "nat ⇒ nat ⇒ nat ⇒ real" ("$'(I^{_}s')^{_}'__" [0,0,101] 200)
  where "$(I^{l}s)^{m}_n ≡ ∑k<n*m. (1+i).^(n-(k+1::nat)/m) * ⌈l*(k+1::nat)/m⌉ / (l*m)"
    ― ‹future value of an increasing annuity›

abbreviation acc_incr_lvl :: "nat ⇒ nat ⇒ real" ("$'(Is')^{_}'__" [0,101] 200)
  where "$(Is)^{m}_n ≡ $(I^{1}s)^{m}_n"

abbreviation acc_incr_yr :: "nat ⇒ real" ("$'(Is')'__" [101] 200)
  where "$(Is)_n ≡ $(Is)^{1}_n"

definition ann_due_incr :: "nat ⇒ nat ⇒ nat ⇒ real" ("$'(I^{_}a''''')^{_}'__" [0,0,101] 200)
  where "$(I^{l}a'')^{m}_n ≡ ∑k<n*m. $v.^((k::nat)/m) * ⌈l*(k+1::nat)/m⌉ / (l*m)"

abbreviation ann_due_incr_lvl :: "nat ⇒ nat ⇒ real" ("$'(Ia''''')^{_}'__" [0,101] 200)
  where "$(Ia'')^{m}_n ≡ $(I^{1}a'')^{m}_n"

abbreviation ann_due_incr_yr :: "nat ⇒ real" ("$'(Ia''''')'__" [101] 200)
  where "$(Ia'')_n ≡ $(Ia'')^{1}_n"

definition acc_due_incr :: "nat ⇒ nat ⇒ nat ⇒ real" ("$'(I^{_}s''''')^{_}'__" [0,0,101] 200)
  where "$(I^{l}s'')^{m}_n ≡ ∑k<n*m. (1+i).^(n-(k::nat)/m) * ⌈l*(k+1::nat)/m⌉ / (l*m)"

abbreviation acc_due_incr_lvl :: "nat ⇒ nat ⇒ real" ("$'(Is''''')^{_}'__" [0,101] 200)
  where "$(Is'')^{m}_n ≡ $(I^{1}s'')^{m}_n"

abbreviation acc_due_incr_yr :: "nat ⇒ real" ("$'(Is''''')'__" [101] 200)
  where "$(Is'')_n ≡ $(Is'')^{1}_n"

definition perp_incr :: "nat ⇒ nat ⇒ real" ("$'(I^{_}a')^{_}'_∞" [0,0] 200)
  where "$(I^{l}a)^{m}_∞ ≡ lim (λn. $(I^{l}a)^{m}_n)"

abbreviation perp_incr_lvl :: "nat ⇒ real" ("$'(Ia')^{_}'_∞" [0] 200)
  where "$(Ia)^{m}_∞ ≡ $(I^{1}a)^{m}_∞"

abbreviation perp_incr_yr :: real ("$'(Ia')'_∞" 200)
  where "$(Ia)_∞ ≡ $(Ia)^{1}_∞"

definition perp_due_incr :: "nat ⇒ nat ⇒ real" ("$'(I^{_}a''''')^{_}'_∞" [0,0] 200)
  where "$(I^{l}a'')^{m}_∞ ≡ lim (λn. $(I^{l}a'')^{m}_n)"

abbreviation perp_due_incr_lvl :: "nat ⇒ real" ("$'(Ia''''')^{_}'_∞" [0] 200)
  where "$(Ia'')^{m}_∞ ≡ $(I^{1}a'')^{m}_∞"

abbreviation perp_due_incr_yr :: real ("$'(Ia''''')'_∞" 200)
  where "$(Ia'')_∞ ≡ $(Ia'')^{1}_∞"

lemma v_futr_m_pos: "1 + $i^{m}/m > 0" if "m ≠ 0" for m::nat
  using v_futr_pos i_nom_def by force

lemma i_nom_1[simp]: "$i^{1} = i"
  using v_futr_pos i_nom_def by force

lemma i_nom_eff: "(1 + $i^{m}/m)^m = 1 + i" if "m ≠ 0" for m::nat
  unfolding i_nom_def using less_imp_neq v_futr_pos that
  apply (simp, subst powr_realpow[THEN sym], simp)
  by (subst powr_powr, simp)

lemma i_nom_i: "1 + $i^{m}/m = (1+i).^(1/m)" if "m ≠ 0" for m::nat
  unfolding i_nom_def by (simp add: that)

lemma i_nom_0_iff_i_0: "$i^{m} = 0 ⟷ i = 0" if "m ≠ 0" for m::nat
proof
  assume "$i^{m} = 0"
  hence ⋆: "(1+i).^(1/m) = (1+i).^0"
    unfolding i_nom_def using v_futr_pos that by simp
  show "i = 0"
  proof (rule ccontr)
    assume "i ≠ 0"
    hence "1/m = 0" using powr_inj ⋆ v_futr_pos by smt
    thus False using that by simp
  qed
next
  assume "i = 0"
  thus "$i^{m} = 0"
    unfolding i_nom_def by simp
qed

lemma i_nom_pos_iff_i_pos: "$i^{m} > 0 ⟷ i > 0" if "m ≠ 0" for m::nat
proof
  assume "$i^{m} > 0"
  hence ⋆: "(1+i).^(1/m) > 1.^(1/m)"
    unfolding i_nom_def using v_futr_pos that by (simp add: zero_less_mult_iff)
  thus "i > 0"
    using powr_less_cancel2[of "1/m" 1 "1+i"] v_futr_pos that by simp
next
  assume "i > 0"
  hence "(1+i).^(1/m) > 1.^(1/m)"
    using powr_less_mono2 v_futr_pos that by simp
  thus "$i^{m} > 0"
    unfolding i_nom_def using that by (simp add: zero_less_mult_iff)
qed

lemma e_delta: "exp ($δ) = 1 + i"
  unfolding i_force_def by (simp add: v_futr_pos)

lemma delta_0_iff_i_0: "$δ = 0 ⟷ i = 0"
proof
  assume "$δ = 0"
  thus "i = 0"
    using e_delta by auto
next
  assume "i = 0"
  thus "$δ = 0"
    unfolding i_force_def by simp
qed

lemma lim_i_nom: "(λm. $i^{m}) ⇢ $δ"
proof -
  let ?f = "λh. ((1+i).^h - 1) / h"
  have D1ipwr: "DERIV (λh. (1+i).^h) 0 :> $δ"
    unfolding i_force_def
    using has_real_derivative_powr2[OF v_futr_pos, where x=0] v_futr_pos by simp
  hence limf: "(?f ⤏ $δ) (at 0)"
    unfolding DERIV_def using v_futr_pos by auto
  hence "(λm. $i^{Suc m}) ⇢ $δ"
    unfolding i_nom_def using tendsto_at_iff_sequentially[of ?f "$δ" 0 ℝ, THEN iffD1]
    apply simp
    apply (drule_tac x="λm. 1 / Suc m" in spec, simp, drule mp)
    subgoal using lim_1_over_n LIMSEQ_Suc by force
    by (simp add: o_def mult.commute)
  thus ?thesis
    by (simp add: LIMSEQ_imp_Suc)
qed

lemma d_nom_0_iff_i_0: "$d^{m} = 0 ⟷ i = 0" if "m ≠ 0" for m::nat
proof -
  have "$d^{m} = 0 ⟷ $i^{m} = 0"
    unfolding d_nom_def using v_futr_m_pos by (smt (verit) divide_eq_0_iff of_nat_0)
  thus ?thesis
    using i_nom_0_iff_i_0 that by auto
qed

lemma d_nom_pos_iff_i_pos: "$d^{m} > 0 ⟷ i > 0" if "m ≠ 0" for m::nat
proof -
  have "$d^{m} > 0 ⟷ $i^{m} > 0"
    unfolding d_nom_def using zero_less_divide_iff i_nom_pos_iff_i_pos v_futr_m_pos that by smt
  thus ?thesis
    using i_nom_pos_iff_i_pos that by auto
qed

lemma d_nom_i_nom: "1 - $d^{m}/m = 1 / (1 + $i^{m}/m)" if "m ≠ 0" for m::nat
proof -
  have "1 - $d^{m}/m = 1 - ($i^{m}/m) / (1 + $i^{m}/m)"
    by (simp add: d_nom_def)
  also have "… = 1 / (1 + $i^{m}/m)"
    using v_futr_m_pos
    by (smt (verit, ccfv_SIG) add_divide_distrib that div_self)
  finally show ?thesis .
qed

lemma lim_d_nom: "(λm. $d^{m}) ⇢ $δ"
proof -
  have "(λm. $i^{m}/m) ⇢ 0"
    using lim_i_nom tendsto_divide_0 tendsto_of_nat by blast
  hence "(λm. 1 + $i^{m}/m) ⇢ 1"
    by (metis add.right_neutral tendsto_add_const_iff)
  thus ?thesis
    unfolding d_nom_def using lim_i_nom tendsto_divide div_by_1 by fastforce
qed

lemma v_pos: "$v > 0"
  unfolding v_pres_def using v_futr_pos by auto

lemma v_1_iff_i_0: "$v = 1 ⟷ i = 0"
proof
  assume "$v = 1"
  thus "i = 0"
    unfolding v_pres_def by simp
next
  assume "i = 0"
  thus "$v = 1"
    unfolding v_pres_def by simp
qed

lemma v_lt_1_iff_i_pos: "$v < 1 ⟷ i > 0"
proof
  assume "$v < 1"
  thus "i > 0"
    unfolding v_pres_def by (simp add: v_futr_pos)
next
  assume "i > 0"
  thus "$v < 1"
    unfolding v_pres_def by (simp add: v_futr_pos)
qed

lemma v_i_nom: "$v = (1 + $i^{m}/m).^-m" if "m ≠ 0" for m::nat
proof -
  have "$v = (1 + i).^-1"
    unfolding v_pres_def using v_futr_pos powr_real_def that by (simp add: powr_neg_one)
  also have "… = ((1 + $i^{m}/m)^m).^-1"
    using i_nom_eff that by presburger
  also have "… = (1 + $i^{m}/m).^-m"
    using powr_powr powr_realpow[THEN sym] v_futr_m_pos that by simp
  finally show ?thesis .
qed

lemma i_v: "1 + i = $v.^-1"
  unfolding v_pres_def powr_real_def using v_futr_pos powr_neg_one by simp

lemma i_v_powr: "(1 + i).^a = $v.^-a" for a::real
  by (subst i_v, subst powr_powr, simp)

lemma v_delta: "ln ($v) = - $δ"
  unfolding i_force_def v_pres_def using v_futr_pos by (simp add: ln_div)

lemma is_derive_vpow: "DERIV (λt. $v.^t) t :> - $δ * $v.^t"
  using v_delta has_real_derivative_powr2 v_pos by (metis mult.commute)

lemma d_nom_v: "$d^{m} = m * (1 - $v.^(1/m))" if "m ≠ 0" for m::nat
proof -
  have "$d^{m} = m * (1 - 1 / (1 + $i^{m}/m))"
    using d_nom_i_nom[THEN sym] that by force
  also have "… = m * (1 - 1 / (1 + i).^(1/m))"
    using i_nom_i that powr_minus_divide by simp
  also have "… = m * (1 - $v.^(1/m))"
    using v_pres_def v_futr_pos powr_divide by simp
  finally show ?thesis .
qed

lemma d_nom_i_nom_v: "$d^{m} = $i^{m} * $v.^(1/m)" if "m ≠0" for m::nat
  unfolding d_nom_def v_pres_def using i_nom_i powr_divide v_futr_pos that by auto

lemma a_calc: "$a^{m}_n = (1 - $v^n) / $i^{m}" if "m ≠ 0" "i ≠ 0" for n m ::nat
proof -
  have "⋀l::nat. l/m = (1/m) * l" by simp
  hence ⋆: "⋀l::nat. $v.^(l/m) = ($v.^(1/m))^l"
    using powr_powr powr_realpow v_pos by (metis powr_gt_zero)
  hence "$a^{m}_n = (∑k<n*m. ($v.^(1/m))^(k+1::nat) / m)"
    unfolding ann_def by presburger
  also have "… = $v.^(1/m) * (∑k<n*m. ($v.^(1/m))^k) / m"
    by (simp, subst sum_divide_distrib[THEN sym], subst sum_distrib_left[THEN sym], simp)
  also have "… = $v.^(1/m) * ((($v.^(1/m))^(n*m) - 1) / ($v.^(1/m) - 1)) / m"
    apply (subst geometric_sum[of "$v.^(1/m)" "n*m"]; simp?)
    using powr_zero_eq_one[of "$v"] v_pos v_1_iff_i_0 powr_inj that
    by (smt (verit, del_insts) divide_eq_0_iff of_nat_eq_0_iff)
  also have "… = (($v.^(1/m))^(n*m) - 1) / (m * ($v.^(1/m) - 1) / $v.^(1/m))"
    by (simp add: field_simps)
  also have "… = ($v^n - 1) / (m * (1 - 1 / $v.^(1/m)))"
    apply (subst ⋆[of "n*m::nat", THEN sym], simp only: of_nat_simps)
    apply (subst nonzero_mult_div_cancel_right[where 'a=real, of m n], simp add: that)
    apply (subst powr_realpow[OF v_pos])
    apply (subst times_divide_eq_right[of _ _ "$v.^(1/m)", THEN sym])
    using v_pos by (subst diff_divide_distrib[of _ _ "$v.^(1/m)"], simp)
  also have "… = (1 - $v^n) / (m * (1 / $v.^(1/m) - 1))"
    using minus_divide_divide by (smt mult_minus_right)
  also have "… = (1 - $v^n) / $i^{m}"
    unfolding i_nom_def v_pres_def using v_futr_pos powr_divide by auto
  finally show ?thesis .
qed

lemma a_calc_i_0: "$a^{m}_n = n" if "m ≠ 0" "i = 0" for n m :: nat 
  unfolding ann_def v_pres_def using that by simp

lemma s_calc_i_0: "$s^{m}_n = n" if "m ≠ 0" "i = 0" for n m :: nat
  unfolding acc_def using that by simp

lemma s_a: "$s^{m}_n = (1+i)^n * $a^{m}_n" if "m ≠ 0" for n m :: nat
proof -
  have "(1+i)^n * $a^{m}_n = (∑k<n*m. (1+i)^n * ($v.^((k+1::nat)/m) / m))"
    unfolding ann_def using sum_distrib_left by blast
  also have "… = (∑k<n*m. (1+i).^((n*m - Suc k)/m) / m)"
  proof -
    have "⋀k::nat. k < n*m ⟹ (1+i)^n * ($v.^((k+1::nat)/m) / m) = (1+i).^((n*m - Suc k)/m) / m"
      unfolding v_pres_def
      apply (subst powr_realpow[THEN sym], simp add: v_futr_pos)
      apply (subst inverse_powr, simp add: v_futr_pos)
      apply (subst times_divide_eq_right, subst powr_add[THEN sym], simp add: that)
      by (subst of_nat_diff, simp add: Suc_le_eq, simp add: diff_divide_distrib that)
    thus ?thesis by (meson lessThan_iff sum.cong)
  qed
  also have "… = (∑k<n*m. (1+i).^(k/m) / m)"
    apply (subst atLeast0LessThan[THEN sym])+
    by (subst sum.atLeastLessThan_rev[THEN sym, of _ "n*m" 0, simplified add_0_right], simp)
  also have "… = $s^{m}_n"
    unfolding acc_def by simp
  finally show ?thesis ..
qed

lemma s_calc: "$s^{m}_n = ((1+i)^n - 1) / $i^{m}" if "m ≠ 0" "i ≠ 0" for n m :: nat
  using that v_futr_pos
  apply (subst s_a, simp, subst a_calc; simp?)
  apply (rule disjI2)
  apply (subst right_diff_distrib, simp)
  apply (rule left_right_inverse_power)
  unfolding v_pres_def by auto

lemma a''_a: "$a''^{m}_n = (1+i).^(1/m) * $a^{m}_n" if "m ≠ 0" for m::nat
  unfolding ann_def ann_due_def
  apply (subst sum_distrib_left, subst times_divide_eq_right, simp)
  by (subst i_v, subst powr_powr, subst powr_add[THEN sym], simp, subst add_divide_distrib, simp)

lemma a_a'': "$a^{m}_n = $v.^(1/m) * $a''^{m}_n" if "m ≠ 0" for m::nat
  unfolding ann_def ann_due_def
  apply (subst sum_distrib_left, subst times_divide_eq_right, simp)
  by (subst powr_add[THEN sym], subst add_divide_distrib, simp)

lemma a''_calc_i_0: "$a''^{m}_n = n" if "m ≠ 0" "i = 0" for n m :: nat
  unfolding ann_due_def v_pres_def using that by simp

lemma s''_calc_i_0: "$s''^{m}_n = n" if "m ≠ 0" "i = 0" for n m :: nat
  unfolding acc_due_def using that by simp

lemma a''_calc: "$a''^{m}_n = (1 - $v^n) / $d^{m}" if "m ≠ 0" "i ≠ 0" for n m :: nat
proof -
  have "$a''^{m}_n = (1+i).^(1/m) * ((1 - $v^n) / $i^{m})"
    using a''_a a_calc times_divide_eq_right that by simp
  also have "… = (1 - $v^n) / ($v.^(1/m) * $i^{m})"
    by (subst i_v, subst powr_powr, simp, subst powr_minus_divide, simp)
  also have "… = (1 - $v^n) / $d^{m}"
    using d_nom_i_nom_v that by simp
  finally show ?thesis .
qed

lemma s''_s: "$s''^{m}_n = (1+i).^(1/m) * $s^{m}_n" if "m ≠ 0" for m::nat
  unfolding acc_def acc_due_def
  apply (subst sum_distrib_left, subst times_divide_eq_right)
  by (subst powr_add[THEN sym], simp, subst add_divide_distrib, simp)

lemma s_s'': "$s^{m}_n = $v.^(1/m) * $s''^{m}_n" if "m ≠ 0" for m::nat
  unfolding acc_def acc_due_def v_pres_def using v_futr_pos
  apply (subst sum_distrib_left, subst times_divide_eq_right, simp)
  by (subst inverse_powr, simp, subst powr_add[THEN sym], subst add_divide_distrib, simp)

lemma s''_calc: "$s''^{m}_n = ((1+i)^n - 1) / $d^{m}" if "m ≠ 0" "i ≠ 0" for n m :: nat
proof -
  have "$s''^{m}_n = (1+i).^(1/m) * ((1+i)^n - 1) / $i^{m}"
    using s''_s s_calc times_divide_eq_right that by simp
  also have "… = ((1+i)^n - 1) / ($v.^(1/m) * $i^{m})"
    by (subst i_v, subst powr_powr, simp, subst powr_minus_divide, simp)
  also have "… = ((1+i)^n - 1) / $d^{m}"
    using d_nom_i_nom_v that by simp
  finally show ?thesis .
qed

lemma s''_a'': "$s''^{m}_n = (1+i)^n * $a''^{m}_n" if "m ≠ 0" for m::nat
  using that s''_s a''_a s_a by simp

lemma a'_calc: "$a'_n = (1 - $v.^n) / $δ" if "i ≠ 0" "n ≥ 0" for n::real
  unfolding ann_cont_def
  apply (rule integral_unique)
  using has_integral_powr2_from_0[OF v_pos _ that(2)] v_delta v_1_iff_i_0 that
  by (smt minus_divide_divide)

lemma a'_calc_i_0: "$a'_n = n" if "i = 0" "n ≥ 0" for n::real
  unfolding ann_cont_def
  apply (subst iffD2[OF v_1_iff_i_0], simp add: that)
  by (simp add: integral_cong that)

lemma s'_calc: "$s'_n = ((1+i).^n - 1) / $δ" if "i ≠ 0" "n ≥ 0" for n::real
  unfolding acc_cont_def
  apply (rule integral_unique)
  using has_integral_powr2_from_0[OF v_futr_pos _ that(2)] i_force_def that
  by simp

lemma s'_calc_i_0: "$s'_n = n" if "i = 0" "n ≥ 0" for n::real
  unfolding acc_cont_def
  apply (subst ‹i = 0›, simp)
  by (simp add: integral_cong that)

lemma s'_a': "$s'_n = (1+i).^n * $a'_n" if "n ≥ 0" for n::real
proof -
  have "(1+i).^n * $a'_n = integral {0..n} (λt. (1+i).^(n-t))"
    unfolding ann_cont_def
    using integrable_on_powr2_from_0_general[of "$v" n] v_pos v_futr_pos that
    apply (subst integral_mult, simp)
    apply (rule integral_cong)
    unfolding v_pres_def using inverse_powr powr_add[THEN sym] by smt
  also have "… = $s'_n"
    unfolding acc_cont_def using v_futr_pos that
    apply (subst has_integral_interval_reverse[of 0 n, simplified, THEN integral_unique]; simp?)
    by (rule continuous_on_powr; auto)
  finally show ?thesis ..
qed

lemma lim_m_a: "(λm. $a^{m}_n) ⇢ $a'_n" for n::nat
proof (rule LIMSEQ_imp_Suc)
  show "(λm. $a^{Suc m}_n) ⇢ $a'_n"
  proof (cases "i = 0")
    case True
    show ?thesis
      using a_calc_i_0 a'_calc_i_0 True by simp
  next
    case False
    show ?thesis
      using False v_pos delta_0_iff_i_0
      apply (subst a_calc; simp?)
      apply (subst a'_calc; simp?)
      apply (subst powr_realpow, simp)
      apply (rule tendsto_divide; simp?)
      by (rule LIMSEQ_Suc[OF lim_i_nom])
  qed
qed

lemma lim_m_a'': "(λm. $a''^{m}_n) ⇢ $a'_n" for n::nat
proof (rule LIMSEQ_imp_Suc)
  show "(λm. $a''^{Suc m}_n) ⇢ $a'_n"
  proof (cases "i = 0")
    case True
    show ?thesis
      using a''_calc_i_0 a'_calc_i_0 True by simp
  next
    case False
    show ?thesis
      using False v_pos delta_0_iff_i_0
      apply (subst a''_calc; simp?)
      apply (subst a'_calc; simp?)
      apply (subst powr_realpow, simp)
      apply (rule tendsto_divide; simp?)
      by (rule LIMSEQ_Suc[OF lim_d_nom])
  qed
qed

lemma lim_m_s: "(λm. $s^{m}_n) ⇢ $s'_n" for n::nat
proof (rule LIMSEQ_imp_Suc)
  show "(λm. $s^{Suc m}_n) ⇢ $s'_n"
  proof (cases "i = 0")
    case True
    show ?thesis
      using s_calc_i_0 s'_calc_i_0 True by simp
  next
    case False
    show ?thesis
      using False v_futr_pos delta_0_iff_i_0
      apply (subst s_calc; simp?)
      apply (subst s'_calc; simp?)
      apply (subst powr_realpow, simp)
      apply (rule tendsto_divide; simp?)
      by (rule LIMSEQ_Suc[OF lim_i_nom])
  qed
qed

lemma lim_m_s'': "(λm. $s''^{m}_n) ⇢ $s'_n" for n::nat
proof (rule LIMSEQ_imp_Suc)
  show "(λm. $s''^{Suc m}_n) ⇢ $s'_n"
  proof (cases "i = 0")
    case True
    show ?thesis
      using s''_calc_i_0 s'_calc_i_0 True by simp
  next
    case False
    show ?thesis
      using False v_futr_pos delta_0_iff_i_0
      apply (subst s''_calc; simp?)
      apply (subst s'_calc; simp?)
      apply (subst powr_realpow, simp)
      apply (rule tendsto_divide; simp?)
      by (rule LIMSEQ_Suc[OF lim_d_nom])
  qed
qed

lemma lim_n_a: "(λn. $a^{m}_n) ⇢ $a^{m}_∞" if "m ≠ 0" "i > 0" for m::nat
proof -
  have "$i^{m} ≠ 0" using i_nom_pos_iff_i_pos that by smt
  moreover have "(λn. $v^n) ⇢ 0"
    using LIMSEQ_realpow_zero[of "$v"] v_pos v_lt_1_iff_i_pos that by simp
  ultimately show ?thesis
    using that apply (subst a_calc; simp?)
    unfolding perp_def apply (rule tendsto_divide; simp?)
    using tendsto_diff[where a=1 and b=0] by auto
qed

lemma lim_n_a'': "(λn. $a''^{m}_n) ⇢ $a''^{m}_∞" if "m ≠ 0" "i > 0" for m::nat
proof -
  have "$d^{m} ≠ 0" using d_nom_pos_iff_i_pos that by smt
  moreover have "(λn. $v^n) ⇢ 0"
    using LIMSEQ_realpow_zero[of "$v"] v_pos v_lt_1_iff_i_pos that by simp
  ultimately show ?thesis
    using that apply (subst a''_calc; simp?)
    unfolding perp_due_def apply (rule tendsto_divide; simp?)
    using tendsto_diff[where a=1 and b=0] by auto
qed

lemma Ilsm_Ilam: "$(I^{l}s)^{m}_n = (1+i)^n * $(I^{l}a)^{m}_n"
  if "l ≠ 0" "m ≠ 0" for l n m :: nat
  unfolding acc_incr_def ann_incr_def v_pres_def using v_futr_pos powr_realpow
  apply (subst inverse_powr, simp)
  apply (subst sum_distrib_left)
  by (subst minus_real_def, subst powr_add, subst times_divide_eq_right, subst mult.assoc, simp)

lemma Iam_calc: "$(Ia)^{m}_n = (∑j<n. (j+1)/m * (∑k=j*m..<(j+1)*m. $v.^((k+1)/m)))"
  if "m ≠ 0" for n m :: nat
proof -
  let ?I = "{..<n}"
  let ?A = "λj. {j*m..<(j+1)*m}"
  let ?g = "λk. $v.^((k+1::nat)/m) * ⌈(k+1::nat)/m⌉ / m"
  have "$(Ia)^{m}_n = (∑j<n. ∑k=j*m..<(j+1)*m. $v.^((k+1)/m) * ⌈(k+1)/m⌉ / m)"
    unfolding ann_incr_def using seq_part_multiple that
    apply (simp only: mult_1)
    by (subst sum.UNION_disjoint[of ?I ?A ?g, THEN sym]; simp)
  also have "… = (∑j<n. (j+1)/m * (∑k=j*m..<(j+1)*m. $v.^((k+1)/m)))"
  proof -
    { fix j k
      assume "j*m ≤ k ∧ k < (j+1)*m"
      hence "j*m < k+1 ∧ k+1 ≤ (j+1)*m" by force
      hence "j < (k+1)/m ∧ (k+1)/m ≤ j+1"
        using pos_less_divide_eq pos_divide_le_eq of_nat_less_iff of_nat_le_iff that
        by (smt (verit) of_nat_le_0_iff of_nat_mult)
      hence "⌈(k+1)/m⌉ = j+1"
        by (simp add: ceiling_unique) }
    hence "⋀j k. j*m ≤ k ∧ k < (j+1)*m ⟹ ⌈(k+1)/m⌉ = j+1"
      by (metis (no_types) of_nat_1 of_nat_add)
    with v_pos show ?thesis
      apply -
      apply (rule sum.cong, simp)
      apply (subst sum_distrib_left, rule sum.cong; simp)
      by (smt (verit, ccfv_SIG) of_int_1 of_int_diff of_int_of_nat_eq)
  qed
  finally show ?thesis .
qed

lemma Ism_calc: "$(Is)^{m}_n = (∑j<n. (j+1)/m * (∑k=j*m..<(j+1)*m. (1+i).^(n-(k+1)/m)))"
  if "m ≠ 0" for n m :: nat
  using v_pos that
  apply (subst Ilsm_Ilam; simp)
  apply (subst Iam_calc[simplified]; simp?)
  apply ((subst sum_distrib_left, rule sum.cong; simp))+
  unfolding v_pres_def using v_futr_pos
  apply (subst inverse_powr; simp)
  apply (subst powr_realpow[THEN sym], simp)
  by (subst powr_add[THEN sym]; simp)

lemma Imam_calc_aux: "$(I^{m}a)^{m}_n = (∑k<n*m. $v.^((k+1)/m) * (k+1) / m^2)"
  if "m ≠ 0" for m::nat
  unfolding ann_incr_def power_def
  apply (rule sum.cong, simp)
  apply (subst of_nat_mult)
  using v_pos that
  apply (subst nonzero_mult_div_cancel_left, simp)
  by (subst ceiling_of_nat; simp)

lemma Imam_calc:
  "$(I^{m}a)^{m}_n = ($v.^(1/m) * (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m))) / (m*(1-$v.^(1/m)))^2"
  if "i ≠ 0" "m ≠ 0" for n m :: nat
proof -
  have ⋆: "$v.^(1/m) > 0" using v_pos by force
  hence "$(I^{m}a)^{m}_n = (∑k<n*m. (k+1)*($v.^(1/m))^(k+1)) / m^2"
    using that
    apply (subst Imam_calc_aux, simp)
    apply (subst sum_divide_distrib[THEN sym], simp)
    apply (rule sum.cong; simp)
    using powr_realpow[THEN sym] powr_powr by (simp add: add_divide_distrib powr_add)
  also have "… = $v.^(1/m) * (∑k<n*m. (k+1)*($v.^(1/m))^k) / m^2"
    by (subst sum_distrib_left, simp add: that, rule sum.cong; simp)
  also have "… = $v.^(1/m) *
    ((1 - (n*m+1)*($v.^(1/m))^(n*m) + n*m*($v.^(1/m))^(n*m+1)) / (1 - $v.^(1/m))^2) / m^2"
    using v_pos v_1_iff_i_0 that by (subst geometric_increasing_sum; simp?)
  also have "… = ($v.^(1/m) * (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m))) / (m*(1-$v.^(1/m)))^2"
    using ⋆
    apply (subst powr_realpow[of "$v.^(1/m)", THEN sym], simp)+
    apply (subst powr_powr)+
    apply (subst times_divide_eq_right[THEN sym], subst divide_divide_eq_left)
    apply (subst power_mult_distrib)
    using powr_eq_one_iff_gen v_pos v_1_iff_i_0 apply (simp add: field_simps)
    by ((subst powr_realpow, simp)+, simp)
  finally show ?thesis .
qed

lemma Imam_calc_i_0: "$(I^{m}a)^{m}_n = (n*m+1)*n / (2*m)" if "i = 0" "m ≠ 0" for n m :: nat
proof -
  have "$(I^{m}a)^{m}_n = (∑k<n*m. $v.^((k+1)/m) * (k+1) / m^2)"
    by (subst Imam_calc_aux, simp_all add: that)
  also have "… = (∑k<n*m. k+1) / m^2"
    apply (subst v_1_iff_i_0[THEN iffD2], simp_all add: that)
    by (subst sum_divide_distrib[THEN sym], simp)
  also have "… = (n*m*(n*m+1) div 2) / m^2"
    apply (subst Suc_eq_plus1[THEN sym], subst sum_bounds_lt_plus1[of id, simplified])
    by (subst Sum_Icc_nat, simp)
  also have "… = (n*m+1)*n / (2*m)"
    apply (subst real_of_nat_div, simp)
    using that by (subst power2_eq_square, simp add: field_simps)
  finally show ?thesis .
qed

lemma Imsm_calc:
  "$(I^{m}s)^{m}_n = ((1+i).^(n+1/m) - (n*m+1)*(1+i).^(1/m) + n*m) / (m*((1+i).^(1/m)-1))^2"
  if "i ≠ 0" "m ≠ 0" for n m :: nat
proof -
  have "$(I^{m}a)^{m}_n =
    ($v^n * ((1+i).^(n+1/m) - (n*m+1)*(1+i).^(1/m) + n*m)) / (m*((1+i).^(1/m)-1))^2"
  proof -
    have "$(I^{m}a)^{m}_n =
      ($v.^(1/m) * (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m))) / (m*(1-$v.^(1/m)))^2"
      using that by (subst Imam_calc; simp)
    also have "… = (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m)) / ($v.^(1/m)*(m*($v.^(-1/m)-1))^2)"
      apply (subgoal_tac "$v.^(-1/m) = 1 / $v.^(1/m)", erule ssubst)
       apply ((subst power2_eq_square)+, simp add: field_simps that)
      by (simp add: powr_minus_divide)
    also have "… =
      ($v.^(n+1/m) * ($v.^(-n-1/m) - (n*m+1)*$v.^(-1/m) + n*m)) / ($v.^(1/m)*(m*($v.^(-1/m)-1))^2)"
      apply (subgoal_tac "$v.^(-n-1/m) = 1 / $v.^(n+1/m)" "$v.^(-1/m) = $v^n / $v.^(n+1/m)")
        apply ((erule ssubst)+, simp_all add: field_simps)
      using v_pos
       apply (simp add: powr_diff[THEN sym] powr_realpow[THEN sym])
      by (smt powr_minus_divide)
    also have "… =
      ($v^n * ($v.^(-n-1/m) - (n*m+1)*$v.^(-1/m) + n*m)) / ((m*($v.^(-1/m)-1))^2)"
      apply (subst powr_add[of _ n "1/m"])
      using v_pos powr_realpow by simp
    also have "… =
      ($v^n * ((1+i).^(n+1/m) - (n*m+1)*(1+i).^(1/m) + n*m)) / ((m*((1+i).^(1/m)-1))^2)"
      apply (subgoal_tac "-n-1/m = -(n+1/m)" "-1/m = -(1/m)", (erule ssubst)+)
        apply (subst i_v_powr[THEN sym])+
      by simp_all
    finally show ?thesis .
  qed
  thus ?thesis
    apply -
    using that v_futr_pos
    apply (subst Ilsm_Ilam, simp)
    apply (erule ssubst, simp)
    apply (rule disjI2)
    by (subst power_mult_distrib[THEN sym], simp add: v_pres_def)
qed

lemma Imsm_calc_i_0: "$(I^{m}s)^{m}_n = (n*m+1)*n / (2*m)" if "i = 0" "m ≠ 0" for n m :: nat
  using that
  apply (subst Ilsm_Ilam, simp)
  by (subst Imam_calc_i_0; simp)

lemma Ila''m_Ilam: "$(I^{l}a'')^{m}_n = (1+i).^(1/m) * $(I^{l}a)^{m}_n"
  if "l ≠ 0" "m ≠ 0" for l m n :: nat
  unfolding ann_incr_def ann_due_incr_def using that
  apply (subst i_v, subst powr_powr, simp)
  apply (subst sum_distrib_left)
  apply (rule sum.cong; simp)
  apply (rule disjI2)
  by (smt (verit) add_divide_distrib powr_add)

lemma Ia''m_calc: "$(Ia'')^{m}_n = (∑j<n. (j+1)/m * (∑k=j*m..<(j+1)*m. $v.^(k/m)))"
  if "m ≠ 0" for n m :: nat
  using that
  apply (subst Ila''m_Ilam; simp del: One_nat_def)
  apply (subst Iam_calc; simp)
  apply (subst sum_distrib_left)
  apply (rule sum.cong; simp)
  apply (subst sum_distrib_left)+
  apply (rule sum.cong; simp)
  apply (subst i_v_powr)
  using powr_add[of "$v", THEN sym] by (simp add: field_simps)

lemma Ima''m_calc_aux: "$(I^{m}a'')^{m}_n = (∑k<n*m. $v.^(k/m) * (k+1) / m^2)"
  if "m ≠ 0" for m::nat
  using that
  apply (subst Ila''m_Ilam, simp)
  apply (subst Imam_calc_aux, simp)
  apply (subst sum_distrib_left)
  apply (rule sum.cong; simp)
  using powr_add[of "$v", THEN sym] i_v_powr by (simp add: field_simps)

lemma Ima''m_calc: "$(I^{m}a'')^{m}_n = (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m)) / (m*(1-$v.^(1/m)))^2"
  if "i ≠ 0" "m ≠ 0" for n m :: nat
  using that v_pos
  apply (subst Ila''m_Ilam, simp)
  apply (subst Imam_calc; simp)
  apply (rule disjI2)+
  by (subst i_v, subst powr_powr, subst powr_add[THEN sym], simp)

lemma Ils''m_Ilsm: "$(I^{l}s'')^{m}_n = (1+i).^(1/m) * $(I^{l}s)^{m}_n"
  if "l ≠ 0" "m ≠ 0" for l m n :: nat
  unfolding acc_incr_def acc_due_incr_def using that
  apply (subst sum_distrib_left)
  apply (rule sum.cong; simp)
  apply (rule disjI2)
  by (subst powr_add[THEN sym], subst add_divide_distrib, simp)

lemma Ims''m_calc:
  "$(I^{m}s'')^{m}_n =
    (1+i).^(1/m) * ((1+i).^(n+1/m) - (n*m+1)*(1+i).^(1/m) + n*m) / (m*((1+i).^(1/m)-1))^2"
  if "i ≠ 0" "m ≠ 0" for n m :: nat
  using that by (simp add: Ils''m_Ilsm Imsm_calc)

lemma lim_Imam: "(λn. $(I^{m}a)^{m}_n) ⇢ 1 / ($i^{m}*$d^{m})" if "m ≠ 0" "i > 0" for m::nat
proof -
  have "(λn. $(I^{m}a)^{m}_n) = 
    (λn. $v.^(1/m) * (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m)) / (m*(1-$v.^(1/m)))^2)"
    using that by (subst Imam_calc; simp)
  moreover have "(λn. $v.^(1/m) * (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m)) / (m*(1-$v.^(1/m)))^2)
    ⇢ 1 / ($i^{m}*$d^{m})"
  proof -
    have ⋆: "¦$v¦ < 1"
      using v_lt_1_iff_i_pos v_pos that by force
    hence "(λn. (n*m+1)*$v^n) ⇢ 0"
      apply (subst tendsto_cong[of _ "(λn. n*m*$v^n + $v^n)"])
       apply (rule always_eventually, rule allI)
       apply (simp add: distrib_right)
      apply (subgoal_tac "0 = 0 + 0", erule ssubst, intro tendsto_intros; simp)
      apply (subst mult.commute, subst mult.assoc)
      apply (subgoal_tac "0 = real m * 0", erule ssubst, intro tendsto_intros; simp?)
      by (rule powser_times_n_limit_0; simp)
    moreover have "(λn. n*m*$v.^(n+1/m)) ⇢ 0"
      apply (subst tendsto_cong[of _ "(λn. (m*$v.^(1/m))*(n*$v^n))"])
       apply (rule always_eventually, rule allI)
       apply (subst powr_add, subst powr_realpow; simp add: v_pos)
      apply (subgoal_tac "0 = m*$v.^(1/m) * 0", erule ssubst, intro tendsto_intros; simp?)
      by (rule powser_times_n_limit_0, simp add: ⋆)
    ultimately have "(λn. $v.^(1/m) * (1 - (n*m+1)*$v^n + n*m*$v.^(n+1/m)) / (m*(1-$v.^(1/m)))^2)
      ⇢ $v.^(1/m) * (1 - 0 + 0)/ (m*(1-$v.^(1/m)))^2"
      using v_lt_1_iff_i_pos v_pos that by (intro tendsto_intros; simp)
    thus ?thesis
      unfolding i_nom_def using v_pos that
      apply (subst i_v_powr, subst powr_minus_divide, subst d_nom_v; simp)
      by (subst(asm)(2) power2_eq_square, simp add: field_simps)
  qed
  ultimately show ?thesis by simp
qed

lemma perp_incr_calc: "$(I^{m}a)^{m}_∞ = 1 / ($i^{m}*$d^{m})" if "m ≠ 0" "i > 0" for m::nat
  unfolding perp_incr_def by (rule limI, rule lim_Imam; simp add: that)

lemma lim_Ima''m: "(λn. $(I^{m}a'')^{m}_n) ⇢ 1 / ($d^{m})^2" if "m ≠ 0" "i > 0" for m::nat
  unfolding perp_due_incr_def using that
  apply (subst Ila''m_Ilam, simp, subst mult.commute, subst i_v_powr, subst powr_minus_divide)
  apply (subgoal_tac "1/($d^{m})^2 = (1/($i^{m}*$d^{m}))*(1/$v.^(1/m))", erule ssubst)
   apply (intro tendsto_intros, simp add: lim_Imam)
  by (subst power2_eq_square, subst(1) d_nom_i_nom_v; simp add: field_simps that)

lemma perp_due_incr_calc: "$(I^{m}a'')^{m}_∞ = 1 / ($d^{m})^2" if "m ≠ 0" "i > 0" for m::nat
  unfolding perp_due_incr_def by (rule limI, rule lim_Ima''m; simp add: that)

end

end