# 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
thus ?thesis
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)"
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"
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 "(m)" "nm"]; 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))"
also have " = (\$v^n - 1) / (m * (1 - 1 / \$v.^(1/m)))"
apply (subst [of "nm::nat", THEN sym], simp only: of_nat_simps)
apply (subst nonzero_mult_div_cancel_right[where 'a=, of m n], simp add: that)
apply (subst powr_realpow[OF v_pos])
apply (subst times_divide_eq_right[of _ _ "(m)", THEN sym])
using v_pos by (subst diff_divide_distrib[of _ _ "(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)
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 _ "nm" , 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)

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)

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)

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)

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)

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  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"
hence "j k. j*m  k  k < (j+1)*m  (k+1)/m = j+1"
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)

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)
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 "(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 , 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)
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 "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)

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)

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)

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)

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. nmn  n)"])
apply (rule always_eventually, rule allI)
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(m))(nn))"])
apply (rule always_eventually, rule allI)
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