# Theory Interest

```theory Interest
imports Preliminaries
begin

section ‹List of Actuarial Notations (Global Scope)›

definition i_nom :: "real ⇒ nat ⇒ real" ("\$i[_]^{_}" [0,0] 200)
where "\$i[i]^{m} ≡ m * ((1+i).^(1/m) - 1)"  ― ‹nominal interest rate›
definition i_force :: "real ⇒ real" ("\$δ[_]" [0] 200)
where "\$δ[i] ≡ ln (1+i)" ― ‹force of interest›
definition d_nom :: "real ⇒ nat ⇒ real" ("\$d[_]^{_}" [0,0] 200)
where "\$d[i]^{m} ≡ \$i[i]^{m} / (1 + \$i[i]^{m}/m)"  ― ‹discount rate›
abbreviation d_nom_yr :: "real ⇒ real" ("\$d[_]" [0] 200)
where "\$d[i] ≡ \$d[i]^{1}"  ― ‹Post-fix "yr" stands for "year".›
definition v_pres :: "real ⇒ real" ("\$v[_]" [0] 200)
where "\$v[i] ≡ 1 / (1+i)"  ― ‹present value factor›
definition ann :: "real ⇒ nat ⇒ nat ⇒ real" ("\$a[_]^{_}'__" [0,0,101] 200)
where "\$a[i]^{m}_n ≡ ∑k<n*m. \$v[i].^((k+1::nat)/m) / m"
― ‹present value of an immediate annuity›
abbreviation ann_yr :: "real ⇒ nat ⇒ real" ("\$a[_]'__" [0,101] 200)
where "\$a[i]_n ≡ \$a[i]^{1}_n"
definition acc :: "real ⇒ nat ⇒ nat ⇒ real" ("\$s[_]^{_}'__" [0,0,101] 200)
where "\$s[i]^{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 :: "real ⇒ nat ⇒ real" ("\$s[_]'__" [0] 200)
where "\$s[i]_n ≡ \$s[i]^{1}_n"
definition ann_due :: "real ⇒ nat ⇒ nat ⇒ real" ("\$a''''[_]^{_}'__" [0,0,101] 200)
where "\$a''[i]^{m}_n ≡ ∑k<n*m. \$v[i].^((k::nat)/m) / m"
― ‹present value of an annuity-due›
abbreviation ann_due_yr :: "real ⇒ nat ⇒ real" ("\$a''''[_]'__" [0,101] 200)
where "\$a''[i]_n ≡ \$a''[i]^{1}_n"
definition acc_due :: "real ⇒ nat ⇒ nat ⇒ real" ("\$s''''[_]^{_}'__" [0,0,101] 200)
where "\$s''[i]^{m}_n ≡ ∑k<n*m. (1+i).^((k+1::nat)/m) / m"
― ‹future value of an annuity-due›
abbreviation acc_due_yr :: "real ⇒ nat ⇒ real" ("\$s''''[_]'__" [0,101] 200)
where "\$s''[i]_n ≡ \$s''[i]^{1}_n"
definition ann_cont :: "real ⇒ real ⇒ real" ("\$a''[_]'__" [0,101] 200)
where "\$a'[i]_n ≡ integral {0..n} (λt::real. \$v[i].^t)"
― ‹present value of a continuous annuity›
definition acc_cont :: "real ⇒ real ⇒ real" ("\$s''[_]'__" [0,101] 200)
where "\$s'[i]_n ≡ integral {0..n} (λt::real. (1+i).^t)"
― ‹future value of a continuous annuity›
definition perp :: "real ⇒ nat ⇒ real" ("\$a[_]^{_}'_∞" [0,0] 200)
where "\$a[i]^{m}_∞ ≡ 1 / \$i[i]^{m}"
― ‹present value of a perpetual annuity›
abbreviation perp_yr :: "real ⇒ real" ("\$a[_]'_∞" [0] 200)
where "\$a[i]_∞ ≡ \$a[i]^{1}_∞"
definition perp_due :: "real ⇒ nat ⇒ real" ("\$a''''[_]^{_}'_∞" [0,0] 200)
where "\$a''[i]^{m}_∞ ≡ 1 / \$d[i]^{m}"
― ‹present value of a perpetual annuity-due›
abbreviation perp_due_yr :: "real ⇒ real" ("\$a''''[_]'_∞" [0] 200)
where "\$a''[i]_∞ ≡ \$a''[i]^{1}_∞"
definition ann_incr :: "nat ⇒ real ⇒ nat ⇒ nat ⇒ real"
("\$'(I^{_}a')[_]^{_}'__" [0,0,0,101] 200)
where "\$(I^{l}a)[i]^{m}_n ≡ ∑k<n*m. \$v[i].^((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 :: "real ⇒ nat ⇒ nat ⇒ real"
("\$'(Ia')[_]^{_}'__" [0,0,101] 200)
where "\$(Ia)[i]^{m}_n ≡ \$(I^{1}a)[i]^{m}_n"
― ‹The post-fix "lvl" stands for "level".›
abbreviation ann_incr_yr :: "real ⇒ nat ⇒ real" ("\$'(Ia')[_]'__" [0,101] 200)
where "\$(Ia)[i]_n ≡ \$(Ia)[i]^{1}_n"
definition acc_incr :: "nat ⇒ real ⇒ nat ⇒ nat ⇒ real"
("\$'(I^{_}s')[_]^{_}'__" [0,0,0,101] 200)
where "\$(I^{l}s)[i]^{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 :: "real ⇒ nat ⇒ nat ⇒ real"
("\$'(Is')[_]^{_}'__" [0,0,101] 200)
where "\$(Is)[i]^{m}_n ≡ \$(I^{1}s)[i]^{m}_n"
abbreviation acc_incr_yr :: "real ⇒ nat ⇒ real" ("\$'(Is')[_]'__" [0,101] 200)
where "\$(Is)[i]_n ≡ \$(Is)[i]^{1}_n"
definition ann_due_incr :: "nat ⇒ real ⇒ nat ⇒ nat ⇒ real"
("\$'(I^{_}a''''')[_]^{_}'__" [0,0,0,101] 200)
where "\$(I^{l}a'')[i]^{m}_n ≡ ∑k<n*m. \$v[i].^((k::nat)/m) * ⌈l*(k+1::nat)/m⌉ / (l*m)"
abbreviation ann_due_incr_lvl :: "real ⇒ nat ⇒ nat ⇒ real"
("\$'(Ia''''')[_]^{_}'__" [0,0,101] 200)
where "\$(Ia'')[i]^{m}_n ≡ \$(I^{1}a'')[i]^{m}_n"
abbreviation ann_due_incr_yr :: "real ⇒ nat ⇒ real" ("\$'(Ia''''')[_]'__" [0,101] 200)
where "\$(Ia'')[i]_n ≡ \$(Ia'')[i]^{1}_n"
definition acc_due_incr :: "nat ⇒ real ⇒ nat ⇒ nat ⇒ real"
("\$'(I^{_}s''''')[_]^{_}'__" [0,0,0,101] 200)
where "\$(I^{l}s'')[i]^{m}_n ≡ ∑k<n*m. (1+i).^(n-(k::nat)/m) * ⌈l*(k+1::nat)/m⌉ / (l*m)"
abbreviation acc_due_incr_lvl :: "real ⇒ nat ⇒ nat ⇒ real"
("\$'(Is''''')[_]^{_}'__" [0,0,101] 200)
where "\$(Is'')[i]^{m}_n ≡ \$(I^{1}s'')[i]^{m}_n"
abbreviation acc_due_incr_yr :: "real ⇒ nat ⇒ real" ("\$'(Is''''')[_]'__" [0,101] 200)
where "\$(Is'')[i]_n ≡ \$(Is'')[i]^{1}_n"
definition perp_incr :: "nat ⇒ real ⇒ nat ⇒ real" ("\$'(I^{_}a')[_]^{_}'_∞" [0,0,0] 200)
where "\$(I^{l}a)[i]^{m}_∞ ≡ lim (λn. \$(I^{l}a)[i]^{m}_n)"
abbreviation perp_incr_lvl :: "real ⇒ nat ⇒ real" ("\$'(Ia')[_]^{_}'_∞" [0,0] 200)
where "\$(Ia)[i]^{m}_∞ ≡ \$(I^{1}a)[i]^{m}_∞"
abbreviation perp_incr_yr :: "real ⇒ real" ("\$'(Ia')[_]'_∞" [0] 200)
where "\$(Ia)[i]_∞ ≡ \$(Ia)[i]^{1}_∞"
definition perp_due_incr :: "nat ⇒ real ⇒ nat ⇒ real" ("\$'(I^{_}a''''')[_]^{_}'_∞" [0,0,0] 200)
where "\$(I^{l}a'')[i]^{m}_∞ ≡ lim (λn. \$(I^{l}a'')[i]^{m}_n)"
abbreviation perp_due_incr_lvl :: "real ⇒ nat ⇒ real" ("\$'(Ia''''')[_]^{_}'_∞" [0,0] 200)
where "\$(Ia'')[i]^{m}_∞ ≡ \$(I^{1}a'')[i]^{m}_∞"
abbreviation perp_due_incr_yr :: "real ⇒ real" ("\$'(Ia''''')[_]'_∞" [0] 200)
where "\$(Ia'')[i]_∞ ≡ \$(Ia'')[i]^{1}_∞"

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.›

context interest
begin

abbreviation i_nom' :: "nat ⇒ real" ("\$i^{_}" [0] 200)
where "\$i^{m} ≡ \$i[i]^{m}"
abbreviation i_force' :: real ("\$δ")
where "\$δ ≡ \$δ[i]"
abbreviation d_nom' :: "nat ⇒ real" ("\$d^{_}" [0] 200)
where "\$d^{m} ≡ \$d[i]^{m}"
abbreviation d_nom_yr' :: real ("\$d")
where "\$d ≡ \$d[i]"
abbreviation v_pres' :: real ("\$v")
where "\$v ≡ \$v[i]"
abbreviation ann' :: "nat ⇒ nat ⇒ real" ("\$a^{_}'__" [0,101] 200)
where "\$a^{m}_n ≡ \$a[i]^{m}_n"
abbreviation ann_yr' :: "nat ⇒ real" ("\$a'__" [101] 200)
where "\$a_n ≡ \$a[i]_n"
abbreviation acc' :: "nat ⇒ nat ⇒ real" ("\$s^{_}'__" [0,101] 200)
where "\$s^{m}_n ≡ \$s[i]^{m}_n"
abbreviation acc_yr' :: "nat ⇒ real" ("\$s'__" [101] 200)
where "\$s_n ≡ \$s[i]_n"
abbreviation ann_due' :: "nat ⇒ nat ⇒ real" ("\$a''''^{_}'__" [0,101] 200)
where "\$a''^{m}_n ≡ \$a''[i]^{m}_n"
abbreviation ann_due_yr' :: "nat ⇒ real" ("\$a'''''__" [101] 200)
where "\$a''_n ≡ \$a''[i]_n"
abbreviation acc_due' :: "nat ⇒ nat ⇒ real" ("\$s''''^{_}'__" [0,101] 200)
where "\$s''^{m}_n ≡ \$s''[i]^{m}_n"
abbreviation acc_due_yr' :: "nat ⇒ real" ("\$s'''''__" [101] 200)
where "\$s''_n ≡ \$s''[i]_n"
abbreviation ann_cont' :: "real ⇒ real" ("\$a'''__" [101] 200)
where "\$a'_n ≡ \$a'[i]_n"
abbreviation acc_cont' :: "real ⇒ real" ("\$s'''__" [101] 200)
where "\$s'_n ≡ \$s'[i]_n"
abbreviation perp' :: "nat ⇒ real" ("\$a^{_}'_∞" [0] 200)
where "\$a^{m}_∞ ≡ \$a[i]^{m}_∞"
abbreviation perp_yr' :: real ("\$a'_∞")
where "\$a_∞ ≡ \$a[i]_∞"
abbreviation perp_due' :: "nat ⇒ real" ("\$a''''^{_}'_∞" [0] 200)
where "\$a''^{m}_∞ ≡ \$a''[i]^{m}_∞"
abbreviation perp_due_yr' :: real ("\$a'''''_∞")
where "\$a''_∞ ≡ \$a''[i]_∞"
abbreviation ann_incr' :: "nat ⇒ nat ⇒ nat ⇒ real" ("\$'(I^{_}a')^{_}'__" [0,0,101] 200)
where "\$(I^{l}a)^{m}_n ≡ \$(I^{l}a)[i]^{m}_n"
abbreviation ann_incr_lvl' :: "nat ⇒ nat ⇒ real" ("\$'(Ia')^{_}'__" [0,101] 200)
where "\$(Ia)^{m}_n ≡ \$(Ia)[i]^{m}_n"
abbreviation ann_incr_yr' :: "nat ⇒ real" ("\$'(Ia')'__" [101] 200)
where "\$(Ia)_n ≡ \$(Ia)[i]_n"
abbreviation acc_incr' :: "nat ⇒ nat ⇒ nat ⇒ real" ("\$'(I^{_}s')^{_}'__" [0,0,101] 200)
where "\$(I^{l}s)^{m}_n ≡ \$(I^{l}s)[i]^{m}_n"
abbreviation acc_incr_lvl' :: "nat ⇒ nat ⇒ real" ("\$'(Is')^{_}'__" [0,101] 200)
where "\$(Is)^{m}_n ≡ \$(Is)[i]^{m}_n"
abbreviation acc_incr_yr' :: "nat ⇒ real" ("\$'(Is')'__" [101] 200)
where "\$(Is)_n ≡ \$(Is)[i]_n"
abbreviation ann_due_incr' :: "nat ⇒ nat ⇒ nat ⇒ real" ("\$'(I^{_}a''''')^{_}'__" [0,0,101] 200)
where "\$(I^{l}a'')^{m}_n ≡ \$(I^{l}a'')[i]^{m}_n"
abbreviation ann_due_incr_lvl' :: "nat ⇒ nat ⇒ real" ("\$'(Ia''''')^{_}'__" [0,101] 200)
where "\$(Ia'')^{m}_n ≡ \$(Ia'')[i]^{m}_n"
abbreviation ann_due_incr_yr' :: "nat ⇒ real" ("\$'(Ia''''')'__" [101] 200)
where "\$(Ia'')_n ≡ \$(Ia'')[i]_n"
abbreviation acc_due_incr' :: "nat ⇒ nat ⇒ nat ⇒ real" ("\$'(I^{_}s''''')^{_}'__" [0,0,101] 200)
where "\$(I^{l}s'')^{m}_n ≡ \$(I^{l}s'')[i]^{m}_n"
abbreviation acc_due_incr_lvl' :: "nat ⇒ nat ⇒ real" ("\$'(Is''''')^{_}'__" [0,101] 200)
where "\$(Is'')^{m}_n ≡ \$(Is'')[i]^{m}_n"
abbreviation acc_due_incr_yr' :: "nat ⇒ real" ("\$'(Is''''')'__" [101] 200)
where "\$(Is'')_n ≡ \$(Is'')[i]_n"
abbreviation perp_incr' :: "nat ⇒ nat ⇒ real" ("\$'(I^{_}a')^{_}'_∞" [0,0] 200)
where "\$(I^{l}a)^{m}_∞ ≡ \$(I^{l}a)[i]^{m}_∞"
abbreviation perp_incr_lvl' :: "nat ⇒ real" ("\$'(Ia')^{_}'_∞" [0] 200)
where "\$(Ia)^{m}_∞ ≡ \$(Ia)[i]^{m}_∞"
abbreviation perp_incr_yr' :: real ("\$'(Ia')'_∞")
where "\$(Ia)_∞ ≡ \$(Ia)[i]_∞"
abbreviation perp_due_incr' :: "nat ⇒ nat ⇒ real" ("\$'(I^{_}a''''')^{_}'_∞" [0,0] 200)
where "\$(I^{l}a'')^{m}_∞ ≡ \$(I^{l}a'')[i]^{m}_∞"
abbreviation perp_due_incr_lvl' :: "nat ⇒ real" ("\$'(Ia''''')^{_}'_∞" [0] 200)
where "\$(Ia'')^{m}_∞ ≡ \$(Ia'')[i]^{m}_∞"
abbreviation perp_due_incr_yr' :: real ("\$'(Ia''''')'_∞")
where "\$(Ia'')_∞ ≡ \$(Ia'')[i]_∞"

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 "\$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))"
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)
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)

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

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

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 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"
hence "⋀j k. j*m ≤ k ∧ k < (j+1)*m ⟹ ⌈(k+1)/m⌉ = j+1"
with v_pos show ?thesis
apply (intro 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 "\$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)
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)

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)
by (smt (verit, del_insts) i_v_powr powr_add powr_zero_eq_one)

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 sum_distrib_left using that
apply (intro sum.cong; 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 (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 (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)