Theory Lemmas_EVT
section ‹Lemmas›
theory Lemmas_EVT
imports
"HOL-Probability.Probability"
"Regular_Variation.Regular_Variation"
begin
lemma power_of_nat_log_less_Suc:
fixes Z t :: real
assumes Z: "1 < Z"
shows "t < Z ^ (nat ⌊log Z t⌋ + 1)"
using assms le_nat_floor[OF le_log_of_power, of Z _ t]
by (meson less_add_one not_less)
subsection ‹Lemmas for Measure Theory›
lemma measure_density_on:
assumes integ:"set_integrable M A f"
and [measurable]: "f ∈ borel_measurable M"
and [measurable]:"A ∈ sets M"
and f_nonneg:"AE x ∈A in M. 0 ≤ f x"
shows "measure (density M f) A = (∫x∈A. f x ∂M)"
proof -
have "measure (density M f) A = enn2real (∫⇧+x∈A. ennreal (f x)∂M)"
by(simp add: measure_def emeasure_density)
also have "... = enn2real (∫⇧+x. ennreal (f x)∂(restrict_space M A))"
by(simp add: nn_integral_restrict_space)
also have "... = enn2real (ennreal (∫x. f x ∂(restrict_space M A)))"
using f_nonneg integ
by(subst nn_integral_eq_integral)
(auto simp: set_integrable_eq AE_restrict_space_iff)
also have "... = enn2real (ennreal (∫x∈A. f x ∂M))"
by(simp add: integral_restrict_space set_lebesgue_integral_def)
also have "... = (∫x∈A. f x ∂M)"
using f_nonneg
by(intro enn2real_ennreal)
(auto intro!: integral_nonneg_AE simp: set_lebesgue_integral_def)
finally show ?thesis .
qed
corollary measure_density:
assumes integ[measurable]:"integrable M f"
and [measurable]:"A ∈ sets M"
and f_nonneg:"AE x in M. 0 ≤ f x"
shows "measure (density M f) A = (∫x∈A. f x ∂M)"
using f_nonneg integrable_mult_indicator[OF _ integ]
by(auto intro!: measure_density_on simp: set_integrable_def)
lemma nn_integral_FTC_greaterThan:
fixes f :: "real ⇒ real" and F :: "real ⇒ real"
assumes f_borel: "f ∈ borel_measurable borel"
and cont: "continuous (at_right a) F"
and f: "⋀x. a < x ⟹ DERIV F x :> f x"
and nonneg: "⋀x. a < x ⟹ 0 ≤ f x"
and lim: "(F ⤏ T) at_top"
shows "(∫⇧+x. ennreal (f x) * indicator {a <..} x ∂lborel) = T - F a"
proof -
define lo where "lo n = a + 1 / (real n + 1)" for n :: nat
define hi where "hi n = a + (real n + 1)" for n :: nat
define g where "g n = (λx. ennreal (f x) * indicator {lo n .. hi n} x)" for n :: nat
have lo_gt: "⋀n. a < lo n" and lo_le_hi: "⋀n. lo n ≤ hi n"
by (auto simp: lo_def hi_def field_simps)
have g_eq: "integral⇧N lborel (g n) = ennreal (F (hi n) - F (lo n))" for n
unfolding g_def
by (rule nn_integral_FTC_Icc[OF f_borel]) (use f nonneg lo_gt[of n] lo_le_hi[of n] in auto)
have incseq_g: "incseq g"
unfolding incseq_def le_fun_def g_def
proof (intro allI impI)
fix m n :: nat and x :: real
assume "m ≤ n"
hence "lo n ≤ lo m" "hi m ≤ hi n"
by (auto simp: lo_def hi_def field_simps)
thus "ennreal (f x) * indicator {lo m..hi m} x ≤ ennreal (f x) * indicator {lo n..hi n} x"
using nonneg[of x] lo_gt[of m]
by (auto split: split_indicator)
qed
have lo_tendsto: "lo ⇢ a"
unfolding lo_def by real_asymp
have hi_tendsto: "filterlim hi at_top sequentially"
unfolding hi_def by real_asymp
have lo_at_right: "filterlim lo (at_right a) sequentially"
using lo_tendsto lo_gt by (rule tendsto_imp_filterlim_at_right[OF _ eventuallyI])
have pointwise: "(λn. g n x) ⇢ ennreal (f x) * indicator {a <..} x" for x
proof (cases "a < x")
case True
have "∀⇩F n in sequentially. lo n ≤ x"
using order_tendstoD(2)[OF lo_tendsto True] by (auto elim: eventually_mono)
moreover have "∀⇩F n in sequentially. x ≤ hi n"
using hi_tendsto[unfolded filterlim_at_top] by simp
ultimately have "∀⇩F n in sequentially. g n x = ennreal (f x) * indicator {a<..} x"
by eventually_elim (use True in ‹auto simp: g_def split: split_indicator›)
thus ?thesis
by (rule tendsto_eventually)
next
case False
hence "g n x = 0" for n
using lo_gt[of n] by (auto simp: g_def split: split_indicator)
thus ?thesis
using False by simp
qed
have limseq1: "(λn. integral⇧N lborel (g n)) ⇢ (∫⇧+x∈{a<..}. ennreal (f x)∂lborel)"
using f_borel pointwise
by (intro nn_integral_LIMSEQ incseq_g) (auto simp: g_def)
have limseq2: "(λn. integral⇧N lborel (g n)) ⇢ ennreal (T - F a)"
proof -
have "(λn. F (hi n) - F (lo n)) ⇢ T - F a"
using cont
by (auto intro!: tendsto_diff filterlim_compose[OF _ hi_tendsto]
filterlim_compose[OF _ lo_at_right] lim
simp: continuous_within)
from tendsto_ennrealI[OF this]
show ?thesis
by (simp add: g_eq)
qed
from LIMSEQ_unique[OF limseq1 limseq2]
show ?thesis .
qed
lemma nn_integral_FTC_lessThan:
fixes f :: "real ⇒ real" and F :: "real ⇒ real"
assumes f_borel: "f ∈ borel_measurable borel"
and cont: "continuous (at_left b) F"
and f: "⋀x. x < b ⟹ DERIV F x :> f x"
and nonneg: "⋀x. x < b ⟹ 0 ≤ f x"
and lim: "(F ⤏ S) at_bot"
shows "(∫⇧+x. ennreal (f x) * indicator {..< b} x ∂lborel) = F b - S"
proof -
define g where "g x = f (- x)" for x :: real
define G where "G x = - F (- x)" for x :: real
note f_borel[measurable]
have g_borel: "g ∈ borel_measurable borel"
unfolding g_def by (rule measurable_compose[OF _ f_borel]) simp
have G_deriv: "DERIV G x :> g x" if "-b < x" for x
proof -
have hx: "- x < b"
using that by simp
have Fd: "(F has_real_derivative f (- x)) (at (- x))"
using f[OF hx] .
have "DERIV (λz. F (- z)) x :> f (- x) * (- 1)"
by (rule DERIV_chain2[where g=uminus, OF Fd]) (auto intro!: derivative_eq_intros)
with DERIV_minus[OF this]
show ?thesis
unfolding G_def g_def by simp
qed
have G_nonneg: "0 ≤ g x" if "-b < x" for x
unfolding g_def using nonneg[of "-x"] that by simp
have G_cont: "continuous (at_right (-b)) G"
using cont[unfolded continuous_within]
unfolding G_def continuous_within
by (simp add: at_right_minus[of "-b"] filterlim_filtermap comp_def tendsto_minus)
have G_lim: "(G ⤏ - S) at_top"
unfolding G_def
using filterlim_compose[OF lim filterlim_uminus_at_bot_at_top]
by (intro tendsto_minus) simp
have eq: "(∫⇧+x. ennreal (g x) * indicator {-b <..} x ∂lborel) = F b - S"
using nn_integral_FTC_greaterThan[OF g_borel G_cont G_deriv G_nonneg G_lim]
by (simp add: G_def)
have "(∫⇧+x. ennreal (f x) * indicator {..< b} x ∂lborel)
= (∫⇧+x. ennreal (f (0 + (-1) * x)) * indicator {..< b} (0 + (-1) * x) ∂lborel)"
by (subst nn_integral_real_affine[where c="-1" and t=0
and f="λx. ennreal (f x) * indicator {..<b} x"]) auto
also have "… = (∫⇧+x. ennreal (g x) * indicator {-b <..} x ∂lborel)"
by (intro nn_integral_cong) (auto simp: g_def split: split_indicator)
finally show ?thesis
using eq by simp
qed
lemma
fixes f :: "real ⇒ real" and F :: "real ⇒ real"
assumes f_borel[measurable]: "f ∈ borel_measurable borel"
and cont: "continuous (at_right a) F"
and f: "⋀x. a < x ⟹ DERIV F x :> f x"
and nonneg: "⋀x. a < x ⟹ 0 ≤ f x"
and lim: "(F ⤏ T) at_top"
shows set_integral_FTC_atLeast:"(∫x∈{a..}. f x ∂lborel) = T - F a"
and set_integrable_FTC_atLeast:"set_integrable lborel {a..} f"
proof -
have mono:"F x ≤ F y" if ax:"a < x" and xy:"x ≤ y" for x y
by(intro DERIV_nonneg_imp_nondecreasing[OF xy])
(meson ax f nonneg order.strict_trans2)
have le_T:"F x ≤ T" if "a < x" for x
using mono[OF that] by(intro tendsto_lowerbound[OF lim])
(auto intro!: eventually_at_top_linorderI[where c=x])
have T_le:"F a ≤ T"
using cont le_T eventually_at_right_less[of a]
by(intro tendsto_upperbound[where F="at_right a"])
(auto simp: continuous_within elim!: eventually_mono)
have 1:"(∫⇧+x∈{a<..}. ennreal (f x)∂lborel)
= (∫⇧+ x. ennreal ¦indicat_real {a<..} x * f x¦ ∂lborel)"
using nonneg by(auto intro!: nn_integral_cong simp: indicator_def)
show "set_integrable lborel {a..} f"
unfolding set_integrable_atLeast_eq[symmetric]
using nn_integral_FTC_greaterThan[OF f_borel cont f nonneg lim]
by(simp add: set_integrable_def integrable_iff_bounded 1)
have "(∫x∈{a..}. f x ∂lborel) = (∫x∈{a<..}. f x ∂lborel)"
by (simp add: set_integral_atLeast_eq)
also have "... = enn2real (∫⇧+x∈{a<..}. ennreal (f x)∂lborel)"
unfolding set_lebesgue_integral_def using nonneg
by(subst integral_eq_nn_integral)
(auto simp: indicator_def intro!: arg_cong[where f=enn2real] nn_integral_cong)
also have "... = enn2real (ennreal (T - F a))"
by(simp add: nn_integral_FTC_greaterThan[OF f_borel cont f nonneg lim])
also have "... = T - F a"
by(simp add: T_le)
finally show "(∫x∈{a..}. f x ∂lborel) = T - F a" .
qed
lemma
fixes f :: "real ⇒ real" and F :: "real ⇒ real"
assumes f_borel[measurable]: "f ∈ borel_measurable borel"
assumes cont: "continuous (at_left b) F"
assumes f: "⋀x. x < b ⟹ DERIV F x :> f x"
assumes nonneg: "⋀x. x < b ⟹ 0 ≤ f x"
assumes lim: "(F ⤏ S) at_bot"
shows set_integral_FTC_atMost:"(∫x∈{..b}. f x ∂lborel) = F b - S"
and set_integrable_FTC_atMost:"set_integrable lborel {..b} f"
proof -
have mono:"F x ≤ F y" if xy:"x ≤ y" and yb:"y < b" for x y
by(intro DERIV_nonneg_imp_nondecreasing[OF xy])
(meson yb f nonneg order.strict_trans1)
have S_ge:"S ≤ F x" if "x < b" for x
using mono[OF _ that] by(intro tendsto_upperbound[OF lim])
(auto intro!: eventually_at_bot_linorderI[where c=x])
have b_left:"∀⇩F x in at_left b. x < b"
by(simp add: eventually_at_filter)
have S_le:"S ≤ F b"
using cont S_ge b_left
by(intro tendsto_lowerbound[where F="at_left b"])
(auto simp: continuous_within elim!: eventually_mono)
have 1:"(∫⇧+x∈{..<b}. ennreal (f x)∂lborel)
= (∫⇧+ x. ennreal ¦indicat_real {..<b} x * f x¦ ∂lborel)"
using nonneg by(auto intro!: nn_integral_cong simp: indicator_def)
show "set_integrable lborel {..b} f"
unfolding set_integrable_atMost_eq[symmetric]
using nn_integral_FTC_lessThan[OF f_borel cont f nonneg lim]
by(simp add: set_integrable_def integrable_iff_bounded 1)
have "(∫x∈{..b}. f x ∂lborel) = (∫x∈{..<b}. f x ∂lborel)"
by (simp add: set_integral_atMost_eq)
also have "... = enn2real (∫⇧+x∈{..<b}. ennreal (f x)∂lborel)"
unfolding set_lebesgue_integral_def using nonneg
by(subst integral_eq_nn_integral)
(auto simp: indicator_def intro!: arg_cong[where f=enn2real] nn_integral_cong)
also have "... = enn2real (ennreal (F b - S))"
by(simp add: nn_integral_FTC_lessThan[OF f_borel cont f nonneg lim])
also have "... = F b - S"
by(simp add: S_le)
finally show "(∫x∈{..b}. f x ∂lborel) = F b - S" .
qed
subsection ‹Lemmas for Limits›
lemma filterlim_log_at_top_gt_1:
fixes a :: real
assumes a:"1 < a"
shows "filterlim (log a) at_top at_top"
unfolding filterlim_at_top
proof safe
fix Z
show "∀⇩F x in at_top. Z ≤ log a x"
by(auto intro!: eventually_at_top_linorderI[where c="max (a powr Z) 1"]
le_log_iff[THEN iffD2] assms)
qed
lemma LIMSEQ_power_at_top:
fixes c :: real
assumes "1 < c"
shows "filterlim (λn. c ^ n) at_top sequentially"
using Archimedean_eventually_pow assms filterlim_at_top_dense by blast
lemma floor_log_at_top:
fixes Z :: real
assumes Z: "1 < Z"
shows "filterlim (λt. nat ⌊log Z t⌋) at_top at_top"
by(intro filterlim_compose[OF filterlim_nat_sequentially]
filterlim_compose[OF filterlim_floor_sequentially] filterlim_log_at_top_gt_1 Z)
lemma squeeze_tendsto_cont_points:
fixes f :: "real ⇒ real" and h :: "'a ⇒ real" and gr :: "real ⇒ 'a ⇒ real"
and F :: "'a filter" and y :: real
and A :: "real set"
assumes mono: "mono_on A f"
and y:"y ∈ interior A"
and cont: "isCont f y"
and conv: "⋀y'. y' ∈ A ⟹ isCont f y' ⟹ ((gr y') ⤏ f y') F"
and low: "⋀y'. y' < y ⟹ y' ∈ A ⟹ ∀⇩F t in F. gr y' t ≤ h t"
and up: "⋀y'. y < y' ⟹ y' ∈ A ⟹ ∀⇩F t in F. h t ≤ gr y' t"
shows "(h ⤏ f y) F"
proof -
obtain A' where A':"open A'" "y ∈ A'" "A' ⊆ A"
using y interiorE by blast
have cd: "countable {s ∈ A'. ¬ isCont f s}"
by (intro mono_on_ctble_discont_open) (auto intro!: mono_onI mono_on_subset[OF mono] A')
obtain δ1 where δ1: "0 < δ1" "⋀x. dist x y < δ1 ⟹ x ∈ A'"
using A'(1,2) open_dist by blast
show ?thesis
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e: "0 < e"
obtain δ0 where δ0: "0 < δ0"
"⋀y''. y'' ≠ y ∧ ¦y'' - y¦ < δ0 ⟹ ¦f y'' - f y¦ < e"
using LIM_D[OF cont[unfolded isCont_def], of e] e by auto
define δ where "δ = min δ0 δ1 / 2"
have δpos: "0 < δ" and δlt: "δ < δ0" "δ < δ1"
using δ0(1) δ1(1) by (auto simp: δ_def)
obtain ylo where ylo: "ylo ∈ {y - δ<..<y}" "ylo ∉ {s ∈ A'. ¬ isCont f s}"
using real_interval_avoid_countable_set[OF _ cd, of "y - δ" y] δpos by auto
obtain yhi where yhi: "yhi ∈ {y<..<y + δ}" "yhi ∉ {s ∈ A'. ¬ isCont f s}"
using real_interval_avoid_countable_set[OF _ cd, of y "y + δ"] δpos by auto
have ylo_lt: "ylo < y" and yhi_gt: "y < yhi"
using ylo(1) yhi(1) by auto
have ylo_A': "ylo ∈ A'" and yhi_A': "yhi ∈ A'"
using δ1(2) ylo(1) yhi(1) δlt(2) by (auto simp: dist_real_def)
have ylo_A: "ylo ∈ A" and yhi_A: "yhi ∈ A"
using ylo_A' yhi_A' A'(3) by auto
have ylo_cont: "isCont f ylo" and yhi_cont: "isCont f yhi"
using ylo(2) yhi(2) ylo_A' yhi_A' by auto
have "f y - e < f ylo"
using δ0(2)[of ylo] ylo(1) δlt(1) by auto
hence lo: "∀⇩F t in F. f y - e < gr ylo t"
by (intro order_tendstoD(1)[OF conv[OF ylo_A ylo_cont]])
have "f yhi < f y + e"
using δ0(2)[of yhi] yhi(1) δlt(1) by auto
hence hi: "∀⇩F t in F. gr yhi t < f y + e"
by (intro order_tendstoD(2)[OF conv[OF yhi_A yhi_cont]])
show "∀⇩F t in F. ¦h t - f y¦ < e"
using lo hi low[OF ylo_lt ylo_A] up[OF yhi_gt yhi_A]
by eventually_elim (simp add: abs_less_iff)
qed
qed
lemma squeeze_tendsto_local:
fixes f :: "real ⇒ real" and h :: "'a ⇒ real" and gr :: "real ⇒ 'a ⇒ real"
and F :: "'a filter" and y η :: real
assumes eta: "0 < η"
and cont: "isCont f y"
and conv: "⋀y'. ¦y' - y¦ < η ⟹ ((gr y') ⤏ f y') F"
and low: "⋀y'. y - η < y' ⟹ y' < y ⟹ ∀⇩F t in F. gr y' t ≤ h t"
and up: "⋀y'. y < y' ⟹ y' < y + η ⟹ ∀⇩F t in F. h t ≤ gr y' t"
shows "(h ⤏ f y) F"
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e: "0 < e"
obtain δ0 where δ0: "0 < δ0"
"⋀y''. y'' ≠ y ∧ ¦y'' - y¦ < δ0 ⟹ ¦f y'' - f y¦ < e"
using LIM_D[OF cont[unfolded isCont_def], of e] e by auto
define δ where "δ = min δ0 η / 2"
have δpos: "0 < δ" and δlt: "δ < η" "δ < δ0"
using δ0(1) eta by (auto simp: δ_def)
define ylo yhi where "ylo = y - δ" and "yhi = y + δ"
have ylo1: "y - η < ylo" "ylo < y" "ylo ≠ y" "¦ylo - y¦ < δ0" "¦ylo - y¦ < η"
using δpos δlt by (auto simp: ylo_def)
have yhi1: "y < yhi" "yhi < y + η" "yhi ≠ y" "¦yhi - y¦ < δ0" "¦yhi - y¦ < η"
using δpos δlt by (auto simp: yhi_def)
have "f y - e < f ylo"
using δ0(2)[of ylo] ylo1(3,4) by auto
hence lo: "∀⇩F t in F. f y - e < gr ylo t"
by (intro order_tendstoD(1)[OF conv[OF ylo1(5)]])
have "f yhi < f y + e"
using δ0(2)[of yhi] yhi1(3,4) by auto
hence hi: "∀⇩F t in F. gr yhi t < f y + e"
by (intro order_tendstoD(2)[OF conv[OF yhi1(5)]])
show "∀⇩F t in F. ¦h t - f y¦ < e"
using lo hi low[OF ylo1(1,2)] up[OF yhi1(1,2)]
by eventually_elim (simp add: abs_less_iff)
qed
corollary squeeze_tendsto_cont_points_pos:
fixes f :: "real ⇒ real" and h :: "'a ⇒ real" and gr :: "real ⇒ 'a ⇒ real"
and F :: "'a filter" and y :: real
assumes mono: "mono_on {0<..} f"
and y: "0 < y" and cont: "isCont f y"
and conv: "⋀r. 0 < r ⟹ isCont f r ⟹ ((gr r) ⤏ f r) F"
and low: "⋀r. 0 < r ⟹ r < y ⟹ ∀⇩F t in F. gr r t ≤ h t"
and up: "⋀r. y < r ⟹ ∀⇩F t in F. h t ≤ gr r t"
shows "(h ⤏ f y) F"
using assms
by(auto intro!: squeeze_tendsto_cont_points
[where f=f and F=F and h=h and gr=gr and A="{0<..}"] simp: interior_open)
corollary squeeze_tendsto_cont_points_UNIV:
fixes f :: "real ⇒ real" and h :: "'a ⇒ real" and gr :: "real ⇒ 'a ⇒ real"
and F :: "'a filter" and y :: real
assumes mono: "mono f"
and cont: "isCont f y"
and conv: "⋀y'. isCont f y' ⟹ ((gr y') ⤏ f y') F"
and low: "⋀y'. y' < y ⟹ ∀⇩F t in F. gr y' t ≤ h t"
and up: "⋀y'. y < y' ⟹ ∀⇩F t in F. h t ≤ gr y' t"
shows "(h ⤏ f y) F"
using assms
by(auto intro!: squeeze_tendsto_cont_points
[where f=f and F=F and h=h and gr=gr and A=UNIV] simp: interior_open)
lemma left_cont_agree_cocountable_eq:
fixes f h :: "real ⇒ real" and N :: "real set" and y :: real
assumes N: "countable N" and y: "0 < y"
and left_cont: "(f ⤏ f y) (at_left y)"
and left_cont_h: "(h ⤏ h y) (at_left y)"
and eq: "⋀x. 0 < x ⟹ x < y ⟹ x ∉ N ⟹ f x = h x"
shows "f y = h y"
proof -
define P where "P = (λn z. z ∈ {max 0 (y - 1 / (real n + 1))<..<y} ∧ z ∉ N)"
have exP: "∃z. P n z" for n
unfolding P_def
using real_interval_avoid_countable_set[OF _ N, of "max 0 (y - 1 / (real n + 1))" y]
y by auto
define zseq where "zseq = (λn. SOME z. P n z)"
have zseqP: "P n (zseq n)" for n
unfolding zseq_def using exP by (rule someI_ex)
have z_pos: "0 < zseq n" and z_lt: "zseq n < y" and z_notin: "zseq n ∉ N" for n
using zseqP by (auto simp: P_def)
have z_gt: "y - 1 / (real n + 1) < zseq n" for n
using zseqP by (auto simp: P_def)
have diff_bound: "y - zseq n < 1 / (real n + 1)" for n
using z_gt by (simp add: cross3_simps)
have diff_pos: "0 ≤ y - zseq n" for n
using z_lt less_eq_real_def by auto
have "(λn. y - zseq n) ⇢ 0"
proof (rule tendsto_sandwich)
show "∀⇩F n in sequentially. 0 ≤ y - zseq n"
using diff_pos by simp
show "∀⇩F n in sequentially. y - zseq n ≤ 1 / (real n + 1)"
using diff_bound by (simp add: less_le_not_le)
show "(λn. 1 / (real n + 1)) ⇢ (0::real)"
using LIMSEQ_inverse_real_of_nat by (simp add: inverse_eq_divide add.commute)
qed simp
from tendsto_diff[OF tendsto_const this, of y]
have z_tendsto: "(λn. zseq n) ⇢ y"
by simp
have z_at_left: "filterlim zseq (at_left y) sequentially"
by (rule tendsto_imp_filterlim_at_left[OF z_tendsto]) (simp add: z_lt)
have f_lim: "(λn. f (zseq n)) ⇢ f y"
using filterlim_compose[OF left_cont z_at_left] by (simp add: comp_def)
have h_lim: "(λn. h (zseq n)) ⇢ h y"
using filterlim_compose[OF left_cont_h z_at_left] by (simp add: comp_def)
have "f (zseq n) = h (zseq n)" for n
using eq[OF z_pos z_lt z_notin] .
with h_lim have "(λn. f (zseq n)) ⇢ h y"
by simp
from LIMSEQ_unique[OF f_lim this] show ?thesis .
qed
lemma power_tendsto_iff_tendsto_tail:
fixes p :: "nat ⇒ real" and q :: real
assumes p_nonneg: "⋀n. 0 ≤ p n" and p_le1: "⋀n. p n ≤ 1"
and q_pos: "0 < q" and q_le1: "q ≤ 1"
shows "(λn. p n ^ n) ⇢ q ⟷ (λn. real n * (1 - p n)) ⇢ - ln q"
proof -
have lb: "1 - p n ≤ - ln (p n)" if "0 < p n" for n
using ln_le_minus_one[OF that] by simp
have ub: "p n * (- ln (p n)) ≤ 1 - p n" if "0 < p n" for n
proof -
have "ln (1 / p n) ≤ 1 / p n - 1"
using that by (intro ln_le_minus_one) simp
hence "- ln (p n) ≤ (1 - p n) / p n"
using that by (simp add: ln_div field_simps)
thus ?thesis
using that by (simp add: field_simps)
qed
show ?thesis
proof
assume T: "(λn. real n * (1 - p n)) ⇢ - ln q"
have p_to_1: "(λn. p n) ⇢ 1"
proof -
have "(λn. (real n * (1 - p n)) * (1 / real n)) ⇢ 0"
using tendsto_mult[OF T lim_1_over_n] by simp
moreover have "∀⇩F n in sequentially. (real n * (1 - p n)) * (1 / real n) = 1 - p n"
using eventually_gt_at_top[of 0] by eventually_elim auto
ultimately have "(λn. 1 - p n) ⇢ 0"
by (rule Lim_transform_eventually)
hence "(λn. 1 - (1 - p n)) ⇢ 1 - 0"
by (intro tendsto_diff tendsto_const)
thus ?thesis
by simp
qed
have ev_pos: "∀⇩F n in sequentially. 1 / 2 < p n"
by (rule order_tendstoD(1)[OF p_to_1]) simp
have nlnp: "(λn. real n * (- ln (p n))) ⇢ - ln q"
proof (rule tendsto_sandwich)
show "∀⇩F n in sequentially. real n * (1 - p n) ≤ real n * (- ln (p n))"
using ev_pos by eventually_elim (fastforce intro!: mult_left_mono lb)
show "∀⇩F n in sequentially. real n * (- ln (p n)) ≤ real n * (1 - p n) / p n"
using ev_pos
by eventually_elim
(use mult_left_mono[OF ub, of _ "real n" for n] in ‹simp add: field_simps›)
show "(λn. real n * (1 - p n)) ⇢ - ln q"
by fact
show "(λn. real n * (1 - p n) / p n) ⇢ - ln q"
using tendsto_divide[OF T p_to_1] by simp
qed
have "∀⇩F n in sequentially. exp (real n * ln (p n)) = p n ^ n"
using ev_pos by eventually_elim (simp add: exp_of_nat_mult)
moreover have "(λn. exp (real n * ln (p n))) ⇢ exp (ln q)"
using tendsto_minus[OF nlnp] by (intro tendsto_exp) simp
ultimately show "(λn. p n ^ n) ⇢ q"
using q_pos by (auto intro: Lim_transform_eventually)
next
assume P: "(λn. p n ^ n) ⇢ q"
have p_to_1: "(λn. p n) ⇢ 1"
proof (rule tendsto_sandwich)
have ev1: "∀⇩F n in sequentially. q / 2 < p n ^ n"
by (rule order_tendstoD(1)[OF P]) (use q_pos q_le1 in simp)
hence ev2: "∀⇩F n in sequentially. q / 2 < p n ^ n ∧ 0 < n"
using eventually_gt_at_top[of 0] by (auto intro: eventually_conj)
show "∀⇩F n in sequentially. (q / 2) powr (1 / real n) ≤ p n"
using ev2
proof eventually_elim
case (elim n)
hence pn_pos: "0 < p n"
using q_pos p_nonneg[of n] by (cases "p n = 0") (auto simp: zero_power)
have "(q / 2) powr (1 / real n) ≤ (p n ^ n) powr (1 / real n)"
using elim q_pos by (intro powr_mono2) auto
also have "(p n ^ n) powr (1 / real n) = (p n powr real n) powr (1 / real n)"
using pn_pos by (simp add: powr_realpow)
also have "… = p n"
using elim pn_pos by (simp add: powr_powr)
finally show ?case .
qed
show "∀⇩F n in sequentially. p n ≤ 1"
using p_le1 by simp
have "(λn. (q / 2) powr (1 / real n)) ⇢ (q / 2) powr 0"
using q_pos by (intro tendsto_powr tendsto_const lim_1_over_n) auto
thus "(λn. (q / 2) powr (1 / real n)) ⇢ 1"
using q_pos q_le1 by simp
show "(λn. 1::real) ⇢ 1"
by simp
qed
have ev_pos: "∀⇩F n in sequentially. 1 / 2 < p n"
by (rule order_tendstoD(1)[OF p_to_1]) simp
have nlnp: "(λn. real n * (- ln (p n))) ⇢ - ln q"
proof -
have "(λn. ln (p n ^ n)) ⇢ ln q"
using q_pos by (intro isCont_tendsto_compose[OF _ P] isCont_ln) simp
moreover have "∀⇩F n in sequentially. ln (p n ^ n) = real n * ln (p n)"
using ev_pos by eventually_elim (simp add: ln_realpow)
ultimately have "(λn. real n * ln (p n)) ⇢ ln q"
by (simp add: filterlim_cong)
thus ?thesis
by(auto dest: tendsto_minus)
qed
show "(λn. real n * (1 - p n)) ⇢ - ln q"
proof (rule tendsto_sandwich)
show "∀⇩F n in sequentially. p n * (real n * (- ln (p n))) ≤ real n * (1 - p n)"
using ev_pos
by eventually_elim
(use mult_left_mono[OF ub, of _ "real n" for n] in ‹simp add: field_simps›)
show "∀⇩F n in sequentially. real n * (1 - p n) ≤ real n * (- ln (p n))"
using ev_pos by eventually_elim (fastforce intro!: mult_left_mono lb)
qed(use tendsto_mult[OF p_to_1 nlnp] nlnp in auto)
qed
qed
lemma filterlim_shift_scale_at_top:
fixes μ σ ξ :: real
assumes [arith]:"0 < σ" "0 < ξ"
shows "LIM x at_top. 1 + ξ * ((x - μ) / σ) :> at_top"
using filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of "1 / σ"]
_ filterlim_tendsto_add_at_top[OF tendsto_const[of "- μ" at_top],of "λx. x"]]
by(intro filterlim_tendsto_add_at_top[OF tendsto_const]
filterlim_tendsto_pos_mult_at_top[OF tendsto_const])
(auto simp: filterlim_ident)
lemma filterlim_shift_scale_at_bot:
fixes μ σ ξ :: real
assumes sigma: "0 < σ" and xi_neg: "ξ < 0"
shows "LIM x at_bot. 1 + ξ * ((x - μ) / σ) :> at_top"
proof -
have eq: "(λx. 1 + ξ * ((x - μ) / σ)) = (λx. 1 + (- ξ / σ) * (μ - x))"
by (rule ext) (use sigma in ‹simp add: field_simps›)
have "LIM x at_bot. μ - x :> at_top"
by real_asymp
hence "LIM x at_bot. (- ξ / σ) * (μ - x) :> at_top"
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const])
(use assms in ‹auto intro: divide_neg_pos›)
hence "LIM x at_bot. 1 + (- ξ / σ) * (μ - x) :> at_top"
by (intro filterlim_tendsto_add_at_top[OF tendsto_const])
thus ?thesis
unfolding eq .
qed
subsection ‹Lemmas for Weak Convergence›
lemma weak_conv_ignore_initial_segment:
assumes "weak_conv a A"
shows "weak_conv (λn. a (n + k)) A"
using assms by(auto simp: weak_conv_def intro!: LIMSEQ_ignore_initial_segment)
lemma weak_conv_offset:
assumes "weak_conv (λn. a (n + k)) A"
shows "weak_conv a A"
using assms LIMSEQ_offset by(fastforce simp: weak_conv_def)
lemma weak_conv_cong:
assumes ev:"⋀x. isCont A x ⟹ ∀⇩F n in sequentially. a n x = b n x"
shows "weak_conv a A ⟷ weak_conv b A"
using tendsto_cong[OF ev] by(simp add: weak_conv_def)
lemma LIMSEQ_imp_weak_conv:
"(⋀x. (λn. a n x) ⇢ A x) ⟹ weak_conv a A"
by(simp add: weak_conv_def)
subsection ‹Generalized Inverses›
definition ginv :: "('a :: conditionally_complete_linorder ⇒ 'a) ⇒ 'a ⇒ 'a" ("_⇧←" [81]) where
"ginv F y = Inf {x. y ≤ F x}"
text ‹ The constant @{term ginv} is the same as @{const right_continuous_mono.I}.
We define @{term ginv} because @{const right_continuous_mono.I} is defined inside
the locale @{locale right_continuous_mono},
which makes it inconvenient to use.›
lemma bdd_below_ginv_set:
assumes mono:"mono F" and Fw:"F w < y"
shows "bdd_below {x::_ :: linorder. y ≤ F x}"
proof (intro bdd_belowI[of _ w])
fix x
assume x:"x ∈ {x. y ≤ F x}"
show "w ≤ x"
using x monoD[OF mono, of x w] Fw by force
qed
lemma ginv_le_iff1:
fixes y :: "'a::{linorder_topology,conditionally_complete_linorder}"
assumes mono: "mono F" and cont: "⋀x. continuous (at_right x) F"
and yFz: "y ≤ F z" and Fwy: "F w < y"
shows "F⇧← y ≤ x ⟷ y ≤ F x"
proof
have ne: "{x. y ≤ F x} ≠ {}"
using yFz by auto
show "y ≤ F x ⟹ ginv F y ≤ x"
unfolding ginv_def by (auto intro!: cInf_lower bdd_below_ginv_set[OF mono Fwy])
assume *: "ginv F y ≤ x"
have "y ≤ (INF s∈{x. y ≤ F x}. F s)"
by (rule cINF_greatest[OF ne]) auto
also have "… = F (Inf {x. y ≤ F x})"
using continuous_at_Inf_mono[OF mono cont ne bdd_below_ginv_set[OF mono Fwy]] ..
also have "… ≤ F x"
using * monoD[OF mono] by (simp add: ginv_def)
finally show "y ≤ F x" .
qed
lemma ginv_mono:
assumes mono: "mono F" and y12: "y1 ≤ y2"
and ex_z: "∃z. y2 ≤ F z" and ex_w: "∃w. F w < y1"
shows "ginv F y1 ≤ ginv F y2"
proof -
obtain z w where z: "y2 ≤ F z" and w: "F w < y1"
using ex_z ex_w by auto
have ne: "{x. y2 ≤ F x} ≠ {}"
using z by auto
have sub: "{x. y2 ≤ F x} ⊆ {x. y1 ≤ F x}"
using y12 by auto
show ?thesis
unfolding ginv_def by (rule cInf_superset_mono[OF ne bdd_below_ginv_set[OF mono w] sub])
qed
lemma ginv_compose_mono:
assumes mono: "mono F" and monog:"mono_on A g"
and ex:"∀s∈A. ∃z. g s ≤ F z" "∀r∈A. ∃w. F w < g r"
shows "mono_on A (λx. ginv F (g x))"
using ex
by(intro ginv_mono mono_onI mono_onD[OF monog] monoD[OF mono])
auto
lemma ginv_attained1:
fixes y :: "'a::{linorder_topology,conditionally_complete_linorder}"
assumes mono: "mono F" and cont: "⋀z. continuous (at_right z) F"
and ex_z: "∃z. y ≤ F z" and ex_w: "∃w. F w < y"
shows "y ≤ F (ginv F y)"
proof -
obtain z w where "y ≤ F z" "F w < y"
using ex_z ex_w by auto
thus ?thesis
using ginv_le_iff1[OF mono cont, of y z w "ginv F y"]
by simp
qed
text ‹Convergence of generalized inverses (Lemma~1.1.1 of the book by de Haan and
Ferreira~\<^cite>‹deHaanFerreira›).›
lemma tendsto_ginv:
fixes Fn :: "nat ⇒ real ⇒ real" and g :: "real ⇒ real" and y :: real
assumes mono_Fn: "⋀n. mono (Fn n)" and mono_g: "mono g"
and wc':"weak_conv Fn g"
and cont_ginv: "isCont (ginv g) y"
and yz: "y < g z" and wy: "g w < y"
shows "(λn. (Fn n)⇧← y) ⇢ g⇧← y"
proof (rule metric_LIMSEQ_I)
have wc:"⋀x. isCont g x ⟹ (λn. Fn n x) ⇢ g x"
using wc' by(simp add: weak_conv_def)
fix ε :: real
assume eps: "0 < ε"
define x0 where "x0 = ginv g y"
note cd = mono_ctble_discont[OF mono_g]
have bdd: "bdd_below {x. y ≤ g x}"
using wy by (intro bdd_below_ginv_set[OF mono_g])
have ne: "{x. y ≤ g x} ≠ {}"
using yz by (auto intro!: exI[of _ z] less_imp_le)
obtain x1 where x1: "x1 ∈ {x0 - ε<..<x0}" "isCont g x1"
using real_interval_avoid_countable_set[OF _ cd, of "x0 - ε" x0] eps by auto
have gx1: "g x1 < y"
proof (rule ccontr)
assume "¬ g x1 < y"
hence "x0 ≤ x1"
unfolding x0_def ginv_def by (auto intro!: cInf_lower bdd)
with x1(1) show False
by auto
qed
obtain s where s: "0 < s"
"⋀y'. y' ≠ y ∧ ¦y' - y¦ < s ⟹ ¦ginv g y' - ginv g y¦ < ε / 2"
using LIM_D[OF cont_ginv[unfolded isCont_def], of "ε / 2"] eps by auto
define y' where "y' = min (y + s / 2) ((y + g z) / 2)"
have y'1: "y < y'"
using s(1) yz by (simp add: y'_def)
have y'2: "y' ≤ g z"
using yz by (auto simp: y'_def min_le_iff_disj)
have y'3: "¦y' - y¦ < s"
using s(1) yz unfolding y'_def by (auto simp: min_def)
have upper': "ginv g y' < x0 + ε / 2"
using s(2)[of y'] y'1 y'3 unfolding x0_def
by (auto simp: abs_real_def split: if_split_asm)
obtain x2 where x2: "x2 ∈ {ginv g y'<..<x0 + ε}" "isCont g x2"
using real_interval_avoid_countable_set[OF _ cd, of "ginv g y'" "x0 + ε"] upper' eps by auto
have gx2: "y < g x2"
proof -
have ne': "{x. y' ≤ g x} ≠ {}"
using y'2 by auto
have "Inf {x. y' ≤ g x} < x2"
using x2(1) by (auto simp: ginv_def)
from cInf_lessD[OF ne' this] obtain x' where x': "y' ≤ g x'" "x' < x2"
by auto
hence "y' ≤ g x2"
using monoD[OF mono_g, of x' x2] by auto
with y'1 show ?thesis
by auto
qed
have ev1: "∀⇩F n in sequentially. Fn n x1 < y"
by (rule order_tendstoD(2)[OF wc[OF x1(2)] gx1])
have ev2: "∀⇩F n in sequentially. y < Fn n x2"
by (rule order_tendstoD(1)[OF wc[OF x2(2)] gx2])
have "∀⇩F n in sequentially. dist (ginv (Fn n) y) x0 < ε"
using ev1 ev2
proof eventually_elim
case (elim n)
have ne_n: "{x. y ≤ Fn n x} ≠ {}"
using elim(2) by (auto intro!: exI[of _ x2] less_imp_le)
have up: "ginv (Fn n) y ≤ x2"
unfolding ginv_def
by (intro cInf_lower bdd_below_ginv_set[OF mono_Fn elim(1)]) (use elim(2) in auto)
have low: "x1 ≤ ginv (Fn n) y"
unfolding ginv_def
by (intro cInf_greatest[OF ne_n])
(metis mono_Fn elim(1) leI mem_Collect_eq monoD order_less_le_trans less_le_not_le)
show ?case
using up low x1(1) x2(1) unfolding dist_real_def by auto
qed
thus"∃no. ∀n≥no. dist (ginv (Fn n) y) (ginv g y) < ε"
unfolding eventually_sequentially x0_def by blast
qed
context right_continuous_mono
begin
lemma ex_gt_b:
assumes "p < b"
shows "∃z. p < f z"
using order_tendstoD[OF top,of p] assms
by (auto dest!: eventually_happens'[OF trivial_limit_at_top_linorder])
lemma ex_ge_b:
assumes "p < b"
shows "∃z. p ≤ f z"
using ex_gt_b[OF assms] by(auto intro!: less_imp_le)
lemma ex_less_a:
assumes "a < p"
shows "∃w. f w < p"
using order_tendstoD[OF bot,of p] assms
by (auto dest!: eventually_happens'[OF trivial_limit_at_bot_linorder])
lemma ex_le_a:
assumes "a < p"
shows "∃w. f w ≤ p"
using ex_less_a[OF assms] by(auto intro!: less_imp_le)
lemma a_le_b:"a ≤ b"
proof -
have "∀⇩F w in at_bot. f w ≤ f 0"
by (auto intro!: eventually_mono[OF eventually_le_at_bot[of 0]] monoD[OF mono])
from tendsto_upperbound[OF bot this]
have "a ≤ f 0"
by simp
moreover
have "∀⇩F w in at_top. f 0 ≤ f w"
by (auto intro!: eventually_mono[OF eventually_ge_at_top[of 0]] monoD[OF mono])
from tendsto_lowerbound[OF top this]
have "f 0 ≤ b"
by simp
ultimately show ?thesis
by linarith
qed
lemma ginv_le_iff:
assumes "a < p" "p < b"
shows "ginv f p ≤ x ⟷ p ≤ f x"
unfolding ginv_def
by(intro pseudoinverse[symmetric] assms)
lemma ginv_attained:
assumes "a < p" "p < b"
shows "p ≤ f (ginv f p)"
using ginv_le_iff[OF assms, of "ginv f p"] by simp
lemma
shows a_le_f: "a ≤ f x"
and f_le_b: "f x ≤ b"
proof -
have "∀⇩F w in at_bot. f w ≤ f x"
by (auto intro!: eventually_mono[OF eventually_le_at_bot[of x]] monoD[OF mono])
from tendsto_upperbound[OF bot this]
show "a ≤ f x"
by simp
have "∀⇩F w in at_top. f x ≤ f w"
by (auto intro!: eventually_mono[OF eventually_ge_at_top[of x]] monoD[OF mono])
from tendsto_lowerbound[OF top this]
show "f x ≤ b"
by simp
qed
lemma ginv_left_cont:
assumes ap: "a < p" and pb:"p < b"
shows "(ginv f ⤏ ginv f p) (at_left p)"
proof (rule order_tendstoI)
fix c
assume c: "c < ginv f p"
hence fc_less: "f c < p"
using ginv_le_iff[OF assms, of c] by simp
define p0 where "p0 = (f c + p) / 2"
have p0_pos: "a < p0" and p0_lt_p: "p0 < p" and Fc_lt_p0: "f c < p0"
using a_le_f[of c] ap fc_less by(auto simp: p0_def)
have p0_lt_1: "p0 < b"
using p0_lt_p pb by simp
have c_lt_p0: "c < ginv f p0"
using ginv_le_iff[OF p0_pos p0_lt_1, of c] Fc_lt_p0 by force
have "∀⇩F x in at_left p. p0 < x ∧ x < p"
using eventually_at_left_field[where x = p] p0_lt_p by auto
thus "∀⇩F x in at_left p. c < ginv f x"
by eventually_elim
(metis c_lt_p0 pb dual_order.strict_trans ginv_le_iff linorder_not_less p0_pos)
next
fix c
assume c: "ginv f p < c"
have "∀⇩F x in at_left p. a < x ∧ x < p"
using eventually_at_left_field[where x = p] ap by auto
thus "∀⇩F x in at_left p. ginv f x < c"
by eventually_elim (smt (verit) c pb ginv_le_iff)
qed
lemma f_eq_b:
assumes "f y = b"
and "y ≤ x"
shows "f x = b"
using assms f_le_b mono monoD order_antisym by blast
lemma f_eq_a:
assumes "f y = a"
and "x ≤ y"
shows "f x = a"
by (metis a_le_f assms dual_order.eq_iff mono monoD)
corollary regularly_varying_less_b:
assumes "regularly_varying (λx. b - f x) ρ"
shows "f x < b"
proof(rule ccontr)
assume "¬ f x < b"
hence eq:"⋀y. x ≤ y ⟹ f y = b"
by (metis f_eq_b f_le_b not_le order_antisym)
show False
using regularly_varying_pos[OF assms,of "max 1 x"]
by(cases "1 ≤ x") (auto simp: eq)
qed
lemma ex_gt_less:
assumes z: "f z < c"
shows "∃w>z. f w < c"
proof -
have "∀⇩F y in at_right z. f y < c ∧ z < y"
using order_tendstoD(2)[OF cont[of z, unfolded continuous_within] z]
eventually_at_right_less by eventually_elim simp
from eventually_happens'[OF trivial_limit_at_right_real this]
show ?thesis
by blast
qed
lemma upper_semicontinuous: "upper_semicontinuous_map euclidean f"
proof -
have "open {x. f x < c}" for c
proof -
have *:"(⋃w∈{w. f w < c}. {..<w}) = {x. f x < c}"
proof (intro set_eqI iffI)
fix x
assume "x ∈ (⋃w∈{w. f w < c}. {..<w})"
then obtain w where "f w < c" "x < w"
by auto
thus "x ∈ {x. f x < c}"
using monoD[OF mono, of x w] by simp
next
fix x
assume "x ∈ {x. f x < c}"
thus "x ∈ (⋃w∈{w. f w < c}. {..<w})"
using ex_gt_less[of x c] by auto
qed
have "open (⋃w∈{w. f w < c}. {..<w})"
by fastforce
thus ?thesis
unfolding * .
qed
thus ?thesis
by(auto simp: upper_semicontinuous_map_def)
qed
corollary open_less: "open {x. f x < c}"
using upper_semicontinuous by(simp add: upper_semicontinuous_map_def)
lemma strict_mono_of_deriv:
assumes deriv: "⋀z. x0 < z ⟹ f z < c ⟹ (f has_real_derivative f' z) (at z)"
and pos: "⋀z. x0 < z ⟹ f z < c ⟹ 0 < f' z"
and x: "x0 < x" and xy: "x < y" and fy: "f y < c"
shows "f x < f y"
proof (rule DERIV_pos_imp_increasing[OF xy])
fix z
assume z: "x ≤ z" "z ≤ y"
hence "x0 < z" "f z < c"
using x fy monoD[OF mono, of z y] by auto
thus "∃w. (f has_real_derivative w) (at z) ∧ 0 < w"
using deriv pos by blast
qed
lemma ginv_f_eq:
assumes fmono: "⋀x y. x0 < x ⟹ x < y ⟹ f y < b ⟹ f x < f y"
and z: "x0 < z" and fz: "f z < b"
shows "ginv f (f z) = z"
proof -
have w: "x0 < (x0 + z) / 2" "(x0 + z) / 2 < z"
using z by simp_all
have "f ((x0 + z) / 2) < f z"
by (rule fmono[OF w fz])
hence p: "a < f z"
using a_le_f[of "(x0 + z) / 2"] by simp
have "z ≤ ginv f (f z)"
proof (rule ccontr)
assume "¬ z ≤ ginv f (f z)"
hence lt: "ginv f (f z) < z"
by simp
define v where "v = (max x0 (ginv f (f z)) + z) / 2"
have vx0: "x0 < v" and vginv: "ginv f (f z) < v" and vz: "v < z"
using lt z by (auto simp: v_def)
have "f z ≤ f v"
using ginv_le_iff[OF p fz, of v] vginv by simp
moreover have "f v < f z"
by (rule fmono[OF vx0 vz fz])
ultimately show False
by simp
qed
moreover have "ginv f (f z) ≤ z"
using ginv_le_iff[OF p fz, of z] by simp
ultimately show ?thesis
by simp
qed
end
sublocale real_distribution ⊆ right_continuous_mono "cdf M" 0 1
by standard
(auto intro!: monoI cdf_nondecreasing cdf_is_right_cont cdf_lim_at_bot cdf_lim_at_top_prob)
corollary right_continuous_mono_cdf:
assumes "real_distribution M"
shows "right_continuous_mono (cdf M) 0 1"
proof -
interpret real_distribution M by fact
show ?thesis
by unfold_locales
qed
lemma one_less_of_inverse_tail_less:
fixes F :: "real ⇒ real"
assumes F: "right_continuous_mono F 0 1" and x0: "F x0 < 1"
and t: "1 / (1 - F x0) < t"
shows "1 < t"
proof -
have "1 ≤ 1 / (1 - F x0)"
using x0 right_continuous_mono.a_le_f[OF F, of x0] by simp
thus ?thesis
using t by linarith
qed
subsection ‹Lemmas for Infinite Sums›
text ‹ The following are used to prove relation~(1.2.21) of \<^cite>‹deHaanFerreira›. ›
lemma geometric_ratio_chain_ge:
fixes d :: "nat ⇒ real"
assumes pos: "⋀n. 0 < d n"
and r: "0 < r"
and bound: "⋀j. M ≤ j ⟹ r ≤ d (Suc j) / d j"
and k: "M ≤ k"
shows "d k * r ^ m ≤ d (k + m)"
proof (induction m)
case (Suc m)
hence "d k * r ^ Suc m ≤ r * d (k + m)"
using r by (auto intro!: mult_left_mono)
also have "… ≤ d (Suc (k + m))"
using bound[of "k + m"] k pos[of "k + m"] by (simp add: field_simps)
finally show ?case
by simp
qed simp
lemma geometric_ratio_chain_le:
fixes d :: "nat ⇒ real"
assumes pos: "⋀n. 0 < d n"
and r: "0 < r"
and bound: "⋀j. M ≤ j ⟹ d (Suc j) / d j ≤ r"
and k: "M ≤ k"
shows "d (k + m) ≤ d k * r ^ m"
proof (induction m)
case (Suc m)
have "d (Suc (k + m)) ≤ r * d (k + m)"
using bound[of "k + m"] k pos[of "k + m"] by (simp add: field_simps)
also have "… ≤ d k * r ^ Suc m"
using Suc r by (auto intro!: mult_left_mono)
finally show ?case
by simp
qed simp
lemma geometric_ratio_tailsum_tendsto:
fixes d :: "nat ⇒ real" and L :: real
assumes pos: "⋀n. 0 < d n"
and L: "0 < L" "L < 1"
and ratio: "(λn. d (Suc n) / d n) ⇢ L"
shows geometric_ratio_tailsum_summable: "summable d"
and geometric_ratio_tailsum_div: "(λn. (∑k. d (k + n)) / d n) ⇢ 1 / (1 - L)"
and geometric_ratio_tailsum_ratio: "(λn. (∑k. d (k + Suc n)) / (∑k. d (k + n))) ⇢ L"
proof -
define cs where "cs = (1 + L) / 2"
have cs_bounds: "L < cs" "cs < 1" "0 < cs"
using L by (simp_all add: cs_def)
obtain N0 where N0: "⋀n. N0 ≤ n ⟹ d (Suc n) / d n < cs"
using order_tendstoD(2)[OF ratio cs_bounds(1)] unfolding eventually_sequentially by blast
have step_le0: "d (Suc n) ≤ cs * d n" if "N0 ≤ n" for n
using N0[OF that] pos[of n] by (simp add: field_simps)
show summable: "summable d"
using cs_bounds step_le0 pos
by(auto intro!: summable_ratio_test[of cs N0 d] simp: abs_of_pos)
note chain_ge = geometric_ratio_chain_ge[where d=d, OF pos]
note chain_le = geometric_ratio_chain_le[where d=d, OF pos]
define T where "T = (λn. ∑k. d (k + n))"
have shift_summable: "summable (λk. d (k + n))" for n
using summable by simp
have T_eq: "T n = suminf d - (∑i<n. d i)" for n
unfolding T_def using suminf_minus_initial_segment[OF summable, of n] by simp
have partial_tendsto: "(λn. ∑i<n. d i) ⇢ suminf d"
using summable by (rule summable_LIMSEQ)
have T_fun_eq: "T = (λn. suminf d - (∑i<n. d i))"
using T_eq by (intro ext) simp
have T_tendsto0: "T ⇢ 0"
unfolding T_fun_eq
using tendsto_diff[OF tendsto_const partial_tendsto, of "suminf d"] by simp
have T_pos: "0 < T n" for n
proof -
have I: "finite {0::nat}" "⋀k. k ∈ - {0::nat} ⟹ 0 ≤ d (k + n)"
using pos by (auto simp: less_eq_real_def)
have "(0::real) < d (0 + n)"
using pos by simp
also have "d (0 + n) = sum (λk. d (k + n)) {0}"
by simp
also have "… ≤ suminf (λk. d (k + n))"
by (rule sum_le_suminf[OF shift_summable[of n] I(1) I(2)])
finally show ?thesis
by (simp add: T_def)
qed
have T_diff: "T n - T (Suc n) = d n" for n
using T_eq[of n] T_eq[of "Suc n"] by simp
have geom_sum: "(∑k. d n * r ^ k) = d n / (1 - r)" if r: "0 < r" "r < 1" for n r
using suminf_geometric[of r] r by (simp add: suminf_mult)
have geom_summable: "summable (λk. d n * r ^ k)" if r: "0 < r" "r < 1" for n r
using summable_geometric[of r] r by (intro summable_mult) simp
have div_tendsto: "(λn. T n / d n) ⇢ 1 / (1 - L)"
proof (rule order_tendstoI)
fix c :: real
assume c: "1 / (1 - L) < c"
have c_pos: "0 < c"
using L c by (smt (verit) divide_pos_pos zero_less_divide_1_iff)
define r where "r = (L + (1 - 1 / c)) / 2"
have Lc: "L < 1 - 1 / c"
using c c_pos L by (simp add: divide_less_eq field_simps)
have r_bounds: "L < r" "r < 1 - 1 / c"
using Lc by (simp_all add: r_def)
have r_pos: "0 < r"
using L r_bounds(1) by simp
have r_lt1: "r < 1"
using r_bounds(2) c_pos by (smt (verit) zero_less_divide_1_iff)
have r_val: "1 / (1 - r) < c"
using r_bounds(2) c_pos r_lt1 by (simp add: field_simps)
obtain N where N: "⋀j. N ≤ j ⟹ d (Suc j) / d j < r"
using order_tendstoD(2)[OF ratio r_bounds(1)]
unfolding eventually_sequentially by blast
have bound_le: "⋀j. N ≤ j ⟹ d (Suc j) / d j ≤ r"
using N by (intro less_imp_le) simp
show "∀⇩F n in sequentially. T n / d n < c"
using eventually_ge_at_top[of N]
proof eventually_elim
case (elim n)
have term_le: "d (n + m) ≤ d n * r ^ m" for m
by (rule chain_le[OF r_pos bound_le]) (use elim in auto)
have term_le': "d (k + n) ≤ d n * r ^ k" for k
using term_le[of k] by (simp add: add.commute)
have "T n ≤ (∑k. d n * r ^ k)"
unfolding T_def
by (rule suminf_le[OF term_le' shift_summable[of n] geom_summable[OF r_pos r_lt1]])
also have "… = d n / (1 - r)"
by (rule geom_sum[OF r_pos r_lt1])
finally have "T n ≤ d n / (1 - r)" .
hence "T n / d n ≤ 1 / (1 - r)"
using pos[of n] by (simp add: field_simps)
thus ?case
using r_val by simp
qed
next
fix c :: real
assume c: "c < 1 / (1 - L)"
show "∀⇩F n in sequentially. c < T n / d n"
proof (cases "c ≤ 0")
case True
have "∀x. c < T x / d x"
using T_pos pos True by (auto intro: divide_pos_pos order_le_less_trans)
thus ?thesis
by (rule always_eventually)
next
case False
hence c_pos: "0 < c"
by simp
have Lc: "1 - 1 / c < L"
using c c_pos L by (simp add: divide_less_eq field_simps)
define ε where "ε = min ((L - (1 - 1 / c)) / 2) (L / 2)"
have ε_le1: "ε ≤ (L - (1 - 1 / c)) / 2"
unfolding ε_def by (rule min.cobounded1)
have ε_le2: "ε ≤ L / 2"
unfolding ε_def by (rule min.cobounded2)
have ε_pos: "0 < ε"
using Lc L by (simp add: ε_def)
define r where "r = L - ε"
have r_pos: "0 < r"
unfolding r_def using ε_le2 L by linarith
have r_lt_L: "r < L"
unfolding r_def using ε_pos by simp
have r_lt1: "r < 1"
using r_lt_L L by simp
have r_gt: "1 - 1 / c < r"
using ε_le1 Lc unfolding r_def by argo
have r_val: "c < 1 / (1 - r)"
using r_gt c_pos r_lt_L L by (simp add: field_simps)
have ev_le: "∀⇩F n in sequentially. r ≤ d (Suc n) / d n"
using order_tendstoD(1)[OF ratio r_lt_L] by eventually_elim simp
obtain N where N: "⋀j. N ≤ j ⟹ r ≤ d (Suc j) / d j"
using ev_le unfolding eventually_sequentially by blast
show "∀⇩F n in sequentially. c < T n / d n"
using eventually_ge_at_top[of N]
proof eventually_elim
case (elim n)
have term_ge: "d n * r ^ m ≤ d (n + m)" for m
by (rule chain_ge[OF r_pos N]) (use elim in auto)
have term_ge': "d n * r ^ k ≤ d (k + n)" for k
using term_ge[of k] by (simp add: add.commute)
have "d n / (1 - r) = (∑k. d n * r ^ k)"
by (rule geom_sum[OF r_pos r_lt1, symmetric])
also have "… ≤ T n"
unfolding T_def
by (rule suminf_le[OF term_ge' geom_summable[OF r_pos r_lt1] shift_summable[of n]])
finally have "d n / (1 - r) ≤ T n" .
hence "1 / (1 - r) ≤ T n / d n"
using pos[of n] by (simp add: field_simps)
thus ?case
using r_val by simp
qed
qed
qed
show div_goal: "(λn. (∑k. d (k + n)) / d n) ⇢ 1 / (1 - L)"
using div_tendsto by (simp add: T_def)
have d_over_T: "(λn. d n / T n) ⇢ (1 - L)"
proof -
have inv: "(λn. inverse (T n / d n)) ⇢ inverse (1 / (1 - L))"
by (rule tendsto_inverse[OF div_tendsto]) (use L in simp)
have eq1: "inverse (1 / (1 - L)) = 1 - L"
by simp
have eq2: "⋀n. inverse (T n / d n) = d n / T n"
using pos T_pos by (simp add: field_simps)
show ?thesis
using inv by (simp add: eq1 eq2)
qed
have T_ratio: "(λn. T (Suc n) / T n) ⇢ L"
proof -
have eqn: "T (Suc n) / T n = 1 - d n / T n" for n
using T_diff[of n] T_pos[of n] by (simp add: field_simps)
have "(λn. 1 - d n / T n) ⇢ 1 - (1 - L)"
by (intro tendsto_diff[OF tendsto_const d_over_T])
thus ?thesis
using eqn by simp
qed
show "(λn. (∑k. d (k + Suc n)) / (∑k. d (k + n))) ⇢ L"
using T_ratio by (simp add: T_def)
qed
lemma geometric_ratio_sum_tendsto:
fixes d :: "nat ⇒ real" and L :: real
assumes pos: "⋀n. 0 < d n"
and L: "1 < L"
and ratio: "(λn. d (Suc n) / d n) ⇢ L"
shows geometric_ratio_sum_div_last: "(λn. (∑k≤n. d k) / d n) ⇢ L / (L - 1)"
and geometric_ratio_sum_ratio: "(λn. (∑k≤Suc n. d k) / (∑k≤n. d k)) ⇢ L"
proof -
have d_at_top: "filterlim d at_top sequentially"
proof -
define r0 :: real where "r0 = (1 + L) / 2"
have r0_bounds: "1 < r0" "r0 < L"
using L by (simp_all add: r0_def)
obtain N where N: "⋀n. N ≤ n ⟹ r0 < d (Suc n) / d n"
using order_tendstoD(1)[OF ratio r0_bounds(2)]
unfolding eventually_sequentially by blast
have grow: "r0 ^ k * d N ≤ d (N + k)" for k
proof (induction k)
case 0
show ?case
by simp
next
case (Suc k)
have step: "r0 * d (N + k) < d (N + Suc k)"
using N[of "N + k"] pos[of "N + k"] by (simp add: field_simps)
have "r0 ^ Suc k * d N = r0 * (r0 ^ k * d N)"
by simp
also have "… ≤ r0 * d (N + k)"
using Suc r0_bounds by (intro mult_left_mono) auto
also have "… < d (N + Suc k)"
by (rule step)
finally show ?case
by simp
qed
have r0k_at_top: "filterlim (λk. r0 ^ k) at_top sequentially"
proof -
have inv0: "(λk. inverse (r0 ^ k)) ⇢ 0"
using r0_bounds(1) by (rule LIMSEQ_inverse_realpow_zero)
have posr: "∀⇩F k in sequentially. 0 < inverse (r0 ^ k)"
using r0_bounds(1) by (auto intro!: always_eventually)
from filterlim_inverse_at_top[OF inv0 posr] show ?thesis
by simp
qed
have shifted: "filterlim (λk. d (N + k)) at_top sequentially"
proof (rule filterlim_at_top_mono)
have "((λk::nat. d N) ⇢ d N)"
by (rule tendsto_const)
from filterlim_tendsto_pos_mult_at_top[OF this pos[of N] r0k_at_top]
show "filterlim (λk. d N * r0 ^ k) at_top sequentially" .
show "∀⇩F k in sequentially. d N * r0 ^ k ≤ d (N + k)"
using grow by (intro always_eventually) (simp add: mult.commute)
qed
show ?thesis
unfolding filterlim_at_top
proof
fix Z :: real
obtain M where M: "⋀k. M ≤ k ⟹ Z ≤ d (N + k)"
using shifted unfolding filterlim_at_top eventually_sequentially by blast
show "∀⇩F n in sequentially. Z ≤ d n"
unfolding eventually_sequentially
proof (intro exI[of _ "N + M"] allI impI)
fix n
assume "N + M ≤ n"
hence "M ≤ n - N" "N ≤ n"
by simp_all
with M[of "n - N"] show "Z ≤ d n"
by simp
qed
qed
qed
define S where "S = (λn. sum d {..n})"
have S_pos: "0 < S n" for n
unfolding S_def by (rule sum_pos) (auto simp: pos)
have S_split: "S n = sum d {..<N} + sum d {N..n}" if "N ≤ n" for N n
using that
by(subst sum.union_disjoint[symmetric])
(auto simp: S_def intro!: arg_cong[where f="sum d"])
note chain_ge = geometric_ratio_chain_ge[where d=d, OF pos]
note chain_le = geometric_ratio_chain_le[where d=d, OF pos]
have div_last: "(λn. S n / d n) ⇢ L / (L - 1)"
proof (rule order_tendstoI)
fix c :: real
assume c: "L / (L - 1) < c"
have c_gt1: "1 < c"
using L c by (smt (verit) divide_le_eq_1 le_divide_eq_1_pos)
have Lc: "c / (c - 1) < L"
using c c_gt1 L by (simp add: divide_less_eq field_simps)
define ε where "ε = (L - c / (c - 1)) / 2"
have ε_pos: "0 < ε"
using Lc by (simp add: ε_def)
define r where "r = L - ε"
have cc1_gt1: "1 < c / (c - 1)"
using c_gt1 by simp
have r_bounds: "1 < r" "r < L"
proof -
have h: "(2::real) < L + c / (c - 1)"
using L cc1_gt1 by linarith
show "1 < r"
unfolding r_def ε_def using h by argo
show "r < L"
using ε_pos by (simp add: r_def)
qed
have r_gt: "c / (c - 1) < r"
using Lc ε_def r_def by auto
have r_c: "r / (r - 1) < c"
using r_bounds(1) r_gt c_gt1 by (simp add: field_simps)
obtain N where N: "⋀j. N ≤ j ⟹ r < d (Suc j) / d j"
using order_tendstoD(1)[OF ratio r_bounds(2)]
unfolding eventually_sequentially by blast
have N_ge: "⋀j. N ≤ j ⟹ r ≤ d (Suc j) / d j"
using N by (intro less_imp_le) simp
have geo_bound: "(∑j≤m. (1 / r) ^ j) < r / (r - 1)" for m
proof -
have ne1: "(1::real) / r ≠ 1"
using r_bounds(1) by simp
have "(∑j≤m. (1 / r) ^ j) = (∑j<Suc m. (1 / r) ^ j)"
by (simp add: lessThan_Suc_atMost)
also have "… = (1 - (1 / r) ^ Suc m) / (1 - 1 / r)"
using sum_gp_strict[of "1 / r" "Suc m"] ne1 by simp
also have "… < 1 / (1 - 1 / r)"
proof -
have "0 < (1 / r) ^ Suc m"
using r_bounds(1) by simp
hence "1 - (1 / r) ^ Suc m < 1"
by simp
thus ?thesis
using r_bounds(1) by (intro divide_strict_right_mono) auto
qed
also have "… = r / (r - 1)"
using r_bounds(1) by (simp add: field_simps)
finally show ?thesis .
qed
have sum_bound_upper: "sum d {N..n} ≤ d n * (∑j≤n - N. (1 / r) ^ j)"
if n: "N ≤ n" for n
proof -
have term_bound: "d k ≤ d n * (1 / r) ^ (n - k)" if k: "k ∈ {N..n}" for k
proof -
have "d k * r ^ (n - k) ≤ d (k + (n - k))"
by (rule chain_ge[OF _ N_ge]) (use k r_bounds in auto)
also have "k + (n - k) = n"
using k by simp
finally have "d k * r ^ (n - k) ≤ d n" .
thus ?thesis
using r_bounds(1) by (simp add: field_simps)
qed
have "sum d {N..n} ≤ sum (λk. d n * (1 / r) ^ (n - k)) {N..n}"
by (rule sum_mono) (use term_bound in auto)
also have "… = d n * sum (λk. (1 / r) ^ (n - k)) {N..n}"
by (simp add: sum_distrib_left)
also have "sum (λk. (1 / r) ^ (n - k)) {N..n} = sum (λj. (1 / r) ^ j) {..n - N}"
by (rule sum.reindex_bij_witness[where i = "λk. n - k" and j = "λj. n - j"])
(use n in auto)
finally show ?thesis
by simp
qed
have S_bound: "S n ≤ sum d {..<N} + d n * (r / (r - 1))" if n: "N ≤ n" for n
proof -
have "S n = sum d {..<N} + sum d {N..n}"
by (rule S_split[OF n])
also have "… ≤ sum d {..<N} + d n * (∑j≤n - N. (1 / r) ^ j)"
using sum_bound_upper[OF n] by simp
also have "… < sum d {..<N} + d n * (r / (r - 1))"
using geo_bound[of "n - N"] pos[of n]
by (intro add_strict_left_mono mult_strict_left_mono) auto
finally show ?thesis
by simp
qed
have const_over_d: "(λn. sum d {..<N} / d n) ⇢ 0"
proof -
have "(λn. inverse (d n)) ⇢ 0"
using d_at_top by (rule tendsto_inverse_0_at_top)
hence "(λn. sum d {..<N} * inverse (d n)) ⇢ sum d {..<N} * 0"
by (intro tendsto_mult tendsto_const)
thus ?thesis
by (simp add: inverse_eq_divide)
qed
have gap_pos: "0 < c - r / (r - 1)"
using r_c by simp
have ev_small: "∀⇩F n in sequentially. sum d {..<N} / d n < c - r / (r - 1)"
using order_tendstoD(2)[OF const_over_d gap_pos] .
show "∀⇩F n in sequentially. S n / d n < c"
using eventually_ge_at_top[of N] ev_small
proof eventually_elim
case (elim n)
have "S n / d n ≤ sum d {..<N} / d n + r / (r - 1)"
using S_bound[OF elim(1)] pos[of n] by (simp add: field_simps)
also have "… < c"
using elim(2) by simp
finally show ?case .
qed
next
fix c :: real
assume c: "c < L / (L - 1)"
show "∀⇩F n in sequentially. c < S n / d n"
proof (cases "c ≤ 1")
case True
show ?thesis
using eventually_ge_at_top[of 1]
proof eventually_elim
case (elim n)
have "S n = sum d {..<n} + d n"
unfolding S_def by (simp add: lessThan_Suc_atMost[symmetric])
moreover have "0 < sum d {..<n}"
using pos elim by(auto intro!: sum_pos simp: lessThan_empty_iff)
ultimately have "d n < S n"
by simp
hence "1 < S n / d n"
using pos[of n] by (simp add: field_simps)
with True show ?case
by simp
qed
next
case False
hence c_gt1: "1 < c"
by simp
have cc1: "L < c / (c - 1)"
proof -
have "c * (L - 1) < L / (L - 1) * (L - 1)"
using c L by (intro mult_strict_right_mono) auto
hence step1: "c * (L - 1) < L"
using L by simp
have step2: "L * (c - 1) < c"
using step1 by argo
show ?thesis
using step2 c_gt1 by (simp add: pos_less_divide_eq)
qed
define ε where "ε = (c / (c - 1) - L) / 2"
have ε_pos: "0 < ε"
using cc1 by (simp add: ε_def)
define r where "r = L + ε"
have r_bounds: "1 < r"
using L ε_pos by (simp add: r_def)
have r_lt: "r < c / (c - 1)"
unfolding r_def ε_def using cc1 by argo
have r_c: "c < r / (r - 1)"
proof -
have "r * (c - 1) < c / (c - 1) * (c - 1)"
using r_lt c_gt1 by (intro mult_strict_right_mono) auto
hence step1: "r * (c - 1) < c"
using c_gt1 by simp
have step2: "c * (r - 1) < r"
using step1 by argo
show ?thesis
using step2 r_bounds by (simp add: pos_less_divide_eq)
qed
have L_lt_r: "L < r"
using ε_pos by (simp add: r_def)
obtain N where N: "⋀j. N ≤ j ⟹ d (Suc j) / d j < r"
using order_tendstoD(2)[OF ratio L_lt_r]
unfolding eventually_sequentially by blast
have N_le: "⋀j. N ≤ j ⟹ d (Suc j) / d j ≤ r"
using N by (intro less_imp_le) simp
have sum_bound_lower: "d n * (∑j≤n - N. (1 / r) ^ j) ≤ sum d {N..n}"
if n: "N ≤ n" for n
proof -
have term_bound: "d n * (1 / r) ^ (n - k) ≤ d k" if k: "k ∈ {N..n}" for k
proof -
have "d (k + (n - k)) ≤ d k * r ^ (n - k)"
by (rule chain_le[OF _ N_le]) (use k r_bounds in auto)
also have "k + (n - k) = n"
using k by simp
finally have "d n ≤ d k * r ^ (n - k)" .
thus ?thesis
using r_bounds by (simp add: field_simps)
qed
have "d n * sum (λk. (1 / r) ^ (n - k)) {N..n} ≤ sum d {N..n}"
unfolding sum_distrib_left by (rule sum_mono) (use term_bound in auto)
moreover have "sum (λk. (1 / r) ^ (n - k)) {N..n} = sum (λj. (1 / r) ^ j) {..n - N}"
by (rule sum.reindex_bij_witness[where i = "λk. n - k" and j = "λj. n - j"])
(use n in auto)
ultimately show ?thesis
by simp
qed
have S_bound: "d n * (∑j≤n - N. (1 / r) ^ j) ≤ S n" if n: "N ≤ n" for n
proof -
have "d n * (∑j≤n - N. (1 / r) ^ j) ≤ sum d {N..n}"
by (rule sum_bound_lower[OF n])
also have "… ≤ sum d {..<N} + sum d {N..n}"
using sum_nonneg[of "{..<N}" d] pos by (simp add: less_imp_le)
also have "… = S n"
using S_split[OF n] by simp
finally show ?thesis .
qed
have geo_tendsto: "(λm. ∑j≤m. (1 / r) ^ j) ⇢ r / (r - 1)"
proof -
have "norm (1 / r) < 1"
using r_bounds by simp
from geometric_sums[OF this]
have "(λn. ∑i<n. (1 / r) ^ i) ⇢ 1 / (1 - 1 / r)"
unfolding sums_def by simp
from LIMSEQ_Suc[OF this]
show ?thesis
using r_bounds by (simp add: lessThan_Suc_atMost field_simps)
qed
have ev_close: "∀⇩F m in sequentially. r / (r - 1) - (r / (r - 1) - c)
< (∑j≤m. (1 / r) ^ j)"
using order_tendstoD(1)[OF geo_tendsto, of "r / (r - 1) - (r / (r - 1) - c)"]
r_c by simp
obtain M where M: "⋀m. M ≤ m ⟹
r / (r - 1) - (r / (r - 1) - c) < (∑j≤m. (1 / r) ^ j)"
using ev_close unfolding eventually_sequentially by blast
show ?thesis
unfolding eventually_sequentially
proof (intro exI[of _ "N + M"] allI impI)
fix n
assume "N + M ≤ n"
hence nN: "N ≤ n" and Mn: "M ≤ n - N"
by simp_all
have "d n * (r / (r - 1) - (r / (r - 1) - c)) < d n * (∑j≤n - N. (1 / r) ^ j)"
using M[OF Mn] pos[of n] by (intro mult_strict_left_mono) auto
also have "… ≤ S n"
by (rule S_bound[OF nN])
finally have "d n * c < S n"
by simp
thus "c < S n / d n"
using pos[of n] by (simp add: field_simps)
qed
qed
qed
show geometric_ratio_sum_div_last: "(λn. (∑k≤n. d k) / d n) ⇢ L / (L - 1)"
using div_last by (simp add: S_def)
show geometric_ratio_sum_ratio: "(λn. (∑k≤Suc n. d k) / (∑k≤n. d k)) ⇢ L"
proof -
have L1ne0: "L / (L - 1) ≠ 0"
using L by simp
have d_div_S: "(λn. d n / S n) ⇢ (L - 1) / L"
proof -
have "(λn. inverse (S n / d n)) ⇢ inverse (L / (L - 1))"
by (rule tendsto_inverse[OF div_last L1ne0])
moreover have "⋀n. inverse (S n / d n) = d n / S n"
using pos S_pos by (simp add: inverse_eq_divide)
moreover have "inverse (L / (L - 1)) = (L - 1) / L"
using L by (simp add: field_simps)
ultimately show ?thesis
by simp
qed
note prod_lim = tendsto_mult[OF ratio d_div_S]
have step: "(λn. 1 + (d (Suc n) / d n) * (d n / S n)) ⇢ 1 + L * ((L - 1) / L)"
by (intro tendsto_add tendsto_const prod_lim)
have eq: "1 + (d (Suc n) / d n) * (d n / S n) = S (Suc n) / S n" for n
proof -
have "(d (Suc n) / d n) * (d n / S n) = d (Suc n) / S n"
using pos[of n] by (simp add: field_simps)
hence "1 + (d (Suc n) / d n) * (d n / S n) = (S n + d (Suc n)) / S n"
using S_pos[of n] by (simp add: field_simps)
also have "S n + d (Suc n) = S (Suc n)"
unfolding S_def by simp
finally show ?thesis .
qed
have val_eq: "1 + L * ((L - 1) / L) = L"
using L by (simp add: field_simps)
have "(λn. S (Suc n) / S n) ⇢ L"
using step unfolding eq val_eq .
thus ?thesis
by (simp add: S_def)
qed
qed
lemma geometric_ratio_forward_telescope:
fixes g :: "real ⇒ real" and Z c :: real
assumes power_ratio: "⋀t0. 0 < t0 ⟹ (λn. g (t0 * Z ^ Suc n) / g (t0 * Z ^ n)) ⇢ c"
and Z: "1 < Z" and c: "c ≠ 0"
shows "(λn. g (Z ^ (n + j)) / g (Z ^ n)) ⇢ c ^ j"
proof (induction j)
case 0
have ratio0: "(λn. g (Z ^ Suc n) / g (Z ^ n)) ⇢ c"
using power_ratio[OF zero_less_one] by simp
have ev_ne0: "∀⇩F n in sequentially. g (Z ^ n) ≠ 0"
using tendsto_imp_eventually_ne[OF ratio0 c] by eventually_elim force
have eq0: "∀⇩F n in sequentially. (1::real) = g (Z ^ (n + 0)) / g (Z ^ n)"
using ev_ne0 by eventually_elim simp
show ?case
using Lim_transform_eventually[OF tendsto_const eq0] by simp
next
case (Suc j)
have Zjpos: "0 < Z ^ j"
using Z by simp
have step: "(λn. g (Z ^ (Suc n + j)) / g (Z ^ (n + j))) ⇢ c"
using power_ratio[OF Zjpos] by (simp add: algebra_simps power_add)
have ev_ne: "∀⇩F n in sequentially. g (Z ^ (n + j)) ≠ 0"
using tendsto_imp_eventually_ne[OF step c] by eventually_elim force
have eq: "∀⇩F n in sequentially.
g (Z ^ (Suc n + j)) / g (Z ^ (n + j)) * (g (Z ^ (n + j)) / g (Z ^ n))
= g (Z ^ (Suc n + j)) / g (Z ^ n)"
by(auto intro!: eventually_mono[OF ev_ne])
show ?case
using Lim_transform_eventually[OF tendsto_mult[OF step Suc.IH] eq] by simp
qed
lemma monotone_geometric_ratio_imp_ratio:
fixes g :: "real ⇒ real" and ρ y :: real
assumes gmono: "⋀s t. 1 < s ⟹ s ≤ t ⟹ g s ≤ g t"
and gpos: "∀⇩F t in at_top. 0 < g t"
and rho: "0 < ρ"
and power_ratio: "⋀Z t0. 1 < Z ⟹ 0 < t0 ⟹
(λn. g (t0 * Z ^ Suc n) / g (t0 * Z ^ n)) ⇢ Z powr ρ"
and y: "0 < y"
shows "((λt. g (t * y) / g t) ⤏ y powr ρ) at_top"
proof -
have Zseq_at_top: "filterlim (λn. Z ^ n) at_top sequentially"
if Z: "1 < Z" for Z :: real
by (rule LIMSEQ_power_at_top[OF Z])
have n_at_top: "filterlim (λt::real. nat ⌊log Z t⌋) at_top at_top"
if Z: "1 < Z" for Z :: real
using Z by (rule floor_log_at_top)
have Zn_cont_at_top: "filterlim (λt::real. Z ^ nat ⌊log Z t⌋) at_top at_top"
if Z: "1 < Z" for Z :: real
by (rule filterlim_compose[OF Zseq_at_top[OF Z] n_at_top[OF Z]])
have Un_pos_ev: "∀⇩F t in at_top. 0 < g (Z ^ nat ⌊log Z t⌋)" if Z: "1 < Z"
for Z :: real
using eventually_compose_filterlim[OF gpos Zn_cont_at_top[OF Z]] .
have Zpowr_ne: "Z powr ρ ≠ 0" if Z: "1 < Z" for Z :: real
using Z by simp
have telescope: "(λn. g (Z ^ (n + j)) / g (Z ^ n))
⇢ (Z powr ρ) ^ j"
if Z: "1 < Z" for Z :: real and j :: nat
by (rule geometric_ratio_forward_telescope[OF power_ratio[OF Z] Z Zpowr_ne[OF Z]])
have telescope_cont: "((λt. g (Z ^ (nat ⌊log Z t⌋ + j))
/ g (Z ^ nat ⌊log Z t⌋))
⤏ (Z powr ρ) ^ j) at_top"
if Z: "1 < Z" for Z :: real and j :: nat
by (rule filterlim_compose[OF telescope[OF Z] n_at_top[OF Z]])
have t_bracket: "∀⇩F t in at_top. Z ^ nat ⌊log Z t⌋ ≤ t ∧ t < Z ^ (nat ⌊log Z t⌋ + 1)"
if Z: "1 < Z" for Z :: real
using eventually_ge_at_top[of "1::real"]
by eventually_elim (use power_of_nat_log_le power_of_nat_log_less_Suc Z in auto)
have n_ge1: "∀⇩F t in at_top. 1 ≤ nat ⌊log Z t⌋" if Z: "1 < Z" for Z :: real
using n_at_top[OF Z, unfolded filterlim_at_top, rule_format, of 1]
by eventually_elim simp
have sandwich_upper: "∀⇩F t in at_top. g (t * y) / g t
≤ g (Z ^ (nat ⌊log Z t⌋ + m + 2)) / g (Z ^ nat ⌊log Z t⌋)"
if y1: "1 ≤ y" and Z1: "1 < Z" and mlo: "Z ^ m ≤ y" and mhi: "y < Z ^ (m + 1)"
for Z :: real and m :: nat and y :: real
using t_bracket[OF Z1] n_ge1[OF Z1] Un_pos_ev[OF Z1]
proof eventually_elim
case (elim t)
define n where "n = nat ⌊log Z t⌋"
have tb1: "Z ^ n ≤ t" and tb2: "t < Z ^ (n + 1)"
using elim unfolding n_def by auto
have n1: "1 ≤ n"
using elim unfolding n_def by simp
have Zn_gt1: "1 < Z ^ n"
using Z1 n1 by simp
have Un_pos: "0 < g (Z ^ n)"
using elim unfolding n_def by simp
have tpos: "0 < t"
using Zn_gt1 tb1 by simp
have ypos: "0 < y"
using y1 by simp
have ty_lt: "t * y < Z ^ (n + m + 2)"
proof -
have "t * y < Z ^ (n + 1) * Z ^ (m + 1)"
using tb2 mhi tpos ypos by (intro mult_strict_mono') auto
also have "… = Z ^ (n + m + 2)"
by (simp add: power_add)
finally show ?thesis .
qed
have t_gt1: "1 < t"
using Zn_gt1 tb1 by simp
have ty_gt1: "1 < t * y"
using y1 t_gt1 mult_left_mono[of 1 y t] by linarith
have Uty_le: "g (t * y) ≤ g (Z ^ (n + m + 2))"
using gmono[OF ty_gt1] ty_lt by simp
have Ut_ge: "g (Z ^ n) ≤ g t"
using gmono[OF Zn_gt1 tb1] .
have Ut_pos: "0 < g t"
using Un_pos Ut_ge by simp
have Unm2_ge: "Z ^ n ≤ Z ^ (n + m + 2)"
using Z1 by (intro power_increasing) auto
have Unm2_gt1: "1 < Z ^ (n + m + 2)"
using Unm2_ge Zn_gt1 by simp
have Utym2_pos: "0 < g (Z ^ (n + m + 2))"
using gmono[OF Zn_gt1 Unm2_ge] Un_pos by simp
show ?case
unfolding n_def[symmetric]
using frac_le[OF Utym2_pos[THEN less_imp_le] Uty_le Un_pos Ut_ge] .
qed
have sandwich_lower:
"∀⇩F t in at_top. g (Z ^ (nat ⌊log Z t⌋ + m)) / g (Z ^ (nat ⌊log Z t⌋ + 1))
≤ g (t * y) / g t"
if y1: "1 ≤ y" and Z1: "1 < Z" and mlo: "Z ^ m ≤ y"
for Z :: real and m :: nat and y :: real
using t_bracket[OF Z1] n_ge1[OF Z1] Un_pos_ev[OF Z1]
proof eventually_elim
case (elim t)
define n where "n = nat ⌊log Z t⌋"
have tb1: "Z ^ n ≤ t" and tb2: "t < Z ^ (n + 1)"
using elim unfolding n_def by auto
have n1: "1 ≤ n"
using elim unfolding n_def by simp
have Zn_gt1: "1 < Z ^ n"
using Z1 n1 by simp
have Un_pos: "0 < g (Z ^ n)"
using elim unfolding n_def by simp
have Znm_ge: "Z ^ n ≤ Z ^ (n + m)"
using Z1 by (intro power_increasing) auto
have Znm_gt1: "1 < Z ^ (n + m)"
using Znm_ge Zn_gt1 by simp
have ty_ge: "Z ^ (n + m) ≤ t * y"
using tb1 mlo Z1 Zn_gt1 by(auto intro!: mult_mono simp: power_add)
have Unm_pos: "0 < g (Z ^ (n + m))"
using gmono[OF Zn_gt1 Znm_ge] Un_pos by simp
have t_gt1: "1 < t"
using Zn_gt1 tb1 by simp
show ?case
unfolding n_def[symmetric]
by(intro frac_le[OF less_imp_le] gmono Znm_gt1 ty_ge
t_gt1 tb2[THEN less_imp_le]
order.strict_trans2[OF Un_pos gmono[OF Zn_gt1 tb1]]
order.strict_trans2[OF Unm_pos gmono[OF Znm_gt1 ty_ge]])
qed
have main: "((λt. g (t * y) / g t) ⤏ y powr ρ) at_top"
if y1: "1 ≤ y" for y
proof -
have Z_of_ratio: "∃Z. 1 < Z ∧ Z ^ 2 < R" if Rgt1: "1 < R" for R :: real
proof -
define B where "B = sqrt R"
define Z where "Z = (1 + B) / 2"
have B1: "1 < B"
unfolding B_def using real_sqrt_less_mono[OF Rgt1] by simp
have Zbounds1: "1 < Z"
unfolding Z_def using B1 by argo
have Zbounds2: "Z < B"
unfolding Z_def using B1 by argo
have ZltB2: "Z ^ 2 < B ^ 2"
using Zbounds1 Zbounds2 by (simp add: power_strict_mono)
have B2: "B ^ 2 = R"
unfolding B_def using Rgt1 by simp
show ?thesis
using Zbounds1 ZltB2 B2 by (intro exI[of _ Z]) simp
qed
show ?thesis
proof (rule order_tendstoI)
fix a :: real
assume a: "a < y powr ρ"
show "∀⇩F t in at_top. a < g (t * y) / g t"
proof (cases "a ≤ 0")
case True
have ypos: "0 < y"
using y1 by simp
have y_at_top: "filterlim (λt::real. t * y) at_top at_top"
using filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of y] ypos filterlim_ident]
by (simp add: mult.commute)
have ev_pos: "∀⇩F t in at_top. 0 < g (t * y) / g t"
using eventually_compose_filterlim[OF gpos y_at_top] gpos
by eventually_elim simp
show ?thesis
using ev_pos
by eventually_elim (use True in linarith)
next
case False
hence apos: "0 < a"
by simp
have alt: "a powr (1 / ρ) < y"
using powr_less_mono2[OF _ _ a, of "1 / ρ"] apos rho y1
by (simp add: powr_powr)
have ratio_gt1: "1 < y / a powr (1 / ρ)"
using alt apos by (simp add: field_simps)
obtain Z where Zbounds1: "1 < Z" and ZltR: "Z ^ 2 < y / a powr (1 / ρ)"
using Z_of_ratio[OF ratio_gt1] by auto
have Zpos: "0 < Z"
using Zbounds1 by simp
have key: "a < (y / Z ^ 2) powr ρ"
proof -
have "a powr (1 / ρ) < y / Z ^ 2"
using ZltR Zpos apos by (simp add: field_simps)
hence "(a powr (1 / ρ)) powr ρ < (y / Z ^ 2) powr ρ"
using rho apos Zpos y1 by (intro powr_less_mono2) auto
also have "(a powr (1 / ρ)) powr ρ = a"
using rho apos by (simp add: powr_powr)
finally show ?thesis .
qed
define m where "m = nat ⌊log Z y⌋"
have ybracket: "Z ^ m ≤ y" "y < Z ^ (m + 1)"
using power_of_nat_log_le power_of_nat_log_less_Suc Zbounds1 y1
unfolding m_def by auto
have tel_m: "((λt. g (Z ^ (nat ⌊log Z t⌋ + m))
/ g (Z ^ nat ⌊log Z t⌋)) ⤏ (Z powr ρ) ^ m) at_top"
using telescope_cont[OF Zbounds1, of m] .
have tel_1: "((λt. g (Z ^ (nat ⌊log Z t⌋ + 1))
/ g (Z ^ nat ⌊log Z t⌋)) ⤏ Z powr ρ) at_top"
using telescope_cont[OF Zbounds1, of 1] by simp
have Zρne: "Z powr ρ ≠ 0"
using Zpos by simp
have div_lim: "((λt. (g (Z ^ (nat ⌊log Z t⌋ + m))
/ g (Z ^ nat ⌊log Z t⌋))
/ (g (Z ^ (nat ⌊log Z t⌋ + 1))
/ g (Z ^ nat ⌊log Z t⌋)))
⤏ (Z powr ρ) ^ m / Z powr ρ) at_top"
by (intro tendsto_divide[OF tel_m tel_1 Zρne])
have eq_ev: "∀⇩F t in at_top. (g (Z ^ (nat ⌊log Z t⌋ + m)) / g (Z ^ nat ⌊log Z t⌋))
/ (g (Z ^ (nat ⌊log Z t⌋ + 1)) / g (Z ^ nat ⌊log Z t⌋))
= g (Z ^ (nat ⌊log Z t⌋ + m)) / g (Z ^ (nat ⌊log Z t⌋ + 1))"
using Un_pos_ev[OF Zbounds1]
by eventually_elim (simp add: field_simps)
have ratio_lim: "((λt. g (Z ^ (nat ⌊log Z t⌋ + m))
/ g (Z ^ (nat ⌊log Z t⌋ + 1)))
⤏ (Z powr ρ) ^ m / Z powr ρ) at_top"
using Lim_transform_eventually[OF div_lim eq_ev] .
have val_gt: "a < (Z powr ρ) ^ m / Z powr ρ"
proof -
have "y / Z ^ 2 < Z ^ m / Z"
using ybracket(2) Zpos by (simp add: field_simps power2_eq_square)
moreover have "0 ≤ y / Z ^ 2"
using y1 Zpos by simp
ultimately have "(y / Z ^ 2) powr ρ < (Z ^ m / Z) powr ρ"
using rho by (intro powr_less_mono2)
also have "(Z ^ m / Z) powr ρ = (Z ^ m) powr ρ / Z powr ρ"
by (simp add: powr_divide)
also have "(Z ^ m) powr ρ = (Z powr ρ) ^ m"
by (metis Zpos less_eq_real_def linorder_not_less powr_power powr_powr powr_realpow)
finally show ?thesis
using key by simp
qed
have ev_val: "∀⇩F t in at_top. a <
g (Z ^ (nat ⌊log Z t⌋ + m)) / g (Z ^ (nat ⌊log Z t⌋ + 1))"
using order_tendstoD(1)[OF ratio_lim val_gt] .
show ?thesis
using ev_val sandwich_lower[OF y1 Zbounds1 ybracket(1)]
by eventually_elim linarith
qed
next
fix c :: real
assume c: "y powr ρ < c"
have cpos: "0 < c"
by(auto intro!: order.strict_trans1[OF _ c])
have alt: "y < c powr (1 / ρ)"
using powr_less_mono2[OF _ _ c, of "1 / ρ"] rho y1
by (simp add: powr_powr)
have ratio_gt1: "1 < c powr (1 / ρ) / y"
using alt y1 by (simp add: field_simps)
obtain Z where Zbounds1: "1 < Z" and ZltR: "Z ^ 2 < c powr (1 / ρ) / y"
using Z_of_ratio[OF ratio_gt1] by auto
have Zpos: "0 < Z"
using Zbounds1 by simp
have key: "(y * Z ^ 2) powr ρ < c"
proof -
have "y * Z ^ 2 < c powr (1 / ρ)"
using ZltR y1 by (simp add: field_simps)
hence "(y * Z ^ 2) powr ρ < (c powr (1 / ρ)) powr ρ"
using rho y1 Zpos by (intro powr_less_mono2) auto
also have "(c powr (1 / ρ)) powr ρ = c"
using rho cpos by (simp add: powr_powr)
finally show ?thesis .
qed
define m where "m = nat ⌊log Z y⌋"
have ybracket: "Z ^ m ≤ y" "y < Z ^ (m + 1)"
using power_of_nat_log_le power_of_nat_log_less_Suc Zbounds1 y1
unfolding m_def by auto
have tel_m2: "((λt. g (Z ^ (nat ⌊log Z t⌋ + (m + 2)))
/ g (Z ^ nat ⌊log Z t⌋)) ⤏ (Z powr ρ) ^ (m + 2)) at_top"
using telescope_cont[OF Zbounds1, of "m + 2"] .
have val_lt: "(Z powr ρ) ^ (m + 2) < c"
proof -
have step1: "Z ^ (m + 2) = Z ^ m * Z ^ 2"
by (rule power_add)
have step2: "Z ^ m * Z ^ 2 ≤ y * Z ^ 2"
using ybracket(1) Zpos by (intro mult_right_mono) auto
have step3: "Z ^ (m + 2) ≤ y * Z ^ 2"
unfolding step1 by (rule step2)
have step3pos: "0 ≤ Z ^ (m + 2)"
using Zpos by simp
have step4: "(Z ^ (m + 2)) powr ρ ≤ (y * Z ^ 2) powr ρ"
by (rule powr_mono2[OF less_imp_le[OF rho] step3pos step3])
have step5: "(Z ^ (m + 2)) powr ρ < c"
using step4 key by linarith
have step6: "(Z ^ (m + 2)) powr ρ = (Z powr ρ) ^ (m + 2)"
by (metis Zpos less_eq_real_def linorder_not_less powr_power powr_powr powr_realpow)
show ?thesis
using step5 step6 by simp
qed
have ev_val:
"∀⇩F t in at_top. g (Z ^ (nat ⌊log Z t⌋ + (m + 2))) / g (Z ^ nat ⌊log Z t⌋) < c"
using order_tendstoD(2)[OF tel_m2 val_lt] .
have ev_val':
"∀⇩F t in at_top. g (Z ^ (nat ⌊log Z t⌋ + m + 2)) / g (Z ^ nat ⌊log Z t⌋) < c"
using ev_val by (simp add: add.assoc)
show "∀⇩F t in at_top. g (t * y) / g t < c"
using ev_val' sandwich_upper[OF y1 Zbounds1 ybracket(1) ybracket(2)]
by eventually_elim linarith
qed
qed
show ?thesis
proof (cases "1 ≤ y")
case False
hence y01: "0 < y" "y < 1"
using y by auto
have yinv1: "1 ≤ 1 / y"
using y01 by (simp add: field_simps)
have base: "((λt. g (t * (1 / y)) / g t)
⤏ (1 / y) powr ρ) at_top"
using main[OF yinv1] .
have ty_at_top: "filterlim (λs::real. s * y) at_top at_top"
using filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of y] y01(1) filterlim_ident]
by (simp add: mult.commute)
have comp: "((λs. g (s * y * (1 / y)) / g (s * y))
⤏ (1 / y) powr ρ) at_top"
by (rule filterlim_compose[OF base ty_at_top])
have simp1: "s * y * (1 / y) = s" for s :: real
using y01 by simp
have base2: "((λs. g s / g (s * y)) ⤏ (1 / y) powr ρ) at_top"
using comp y01 by (simp add: simp1)
have nz: "(1 / y) powr ρ ≠ 0"
using y01 by simp
have recip: "((λs. inverse (g s / g (s * y)))
⤏ inverse ((1 / y) powr ρ)) at_top"
by (rule tendsto_inverse[OF base2 nz])
note ev_ne = tendsto_imp_eventually_ne[OF base2 nz]
have eq: "∀⇩F s in at_top. inverse (g s / g (s * y))
= g (s * y) / g s"
using ev_ne by eventually_elim (simp add: field_simps)
have final: "((λs. g (s * y) / g s)
⤏ inverse ((1 / y) powr ρ)) at_top"
using Lim_transform_eventually[OF recip eq] .
have val: "inverse ((1 / y) powr ρ) = y powr ρ"
by (simp add: powr_divide)
show ?thesis
using final val by simp
qed(simp add: main)
qed
lemma galois_inverse_ratio_tendsto:
fixes W s :: "real ⇒ real" and ρ x :: real
assumes W: "filterlim W at_top at_top"
and s: "filterlim s at_top at_top"
and s_pos: "⋀w. 0 < w ⟹ 0 < s w"
and le_iff: "⋀t w. 1 < t ⟹ (W t ≤ w) = (t ≤ s w)"
and rho[arith]: "0 < ρ"
and lim: "⋀y. 0 < y ⟹ ((λt. W (t * y) / W t) ⤏ y powr ρ) at_top"
and x[arith]: "0 < x"
shows "((λu. s (u * x) / s u) ⤏ x powr (1 / ρ)) at_top"
proof -
have galois_strict: "(w < W t) = (s w < t)" if t1: "1 < t" for t w
using le_iff[OF t1, of w] by linarith
have s_gt1: "∀⇩F u in at_top. 1 < s u"
using s unfolding filterlim_at_top_dense by blast
have Ws_pos: "∀⇩F u in at_top. 0 < W (s u)"
using filterlim_compose[OF W s] unfolding filterlim_at_top_dense by blast
have s_gt1_mult: "∀⇩F u in at_top. 1 < s u * c" if c: "0 < c" for c
proof -
have "∀⇩F u in at_top. 1 / c < s u"
using s unfolding filterlim_at_top_dense by blast
thus ?thesis
by eventually_elim (use c in "simp add: field_simps")
qed
have u_pos: "∀⇩F u in at_top. (0::real) < u"
by (rule eventually_gt_at_top)
have upper: "∀⇩F u in at_top. W (s u) ≤ u"
using s_gt1 by eventually_elim (use le_iff in auto)
have near_inv: "((λu. W (s u) / u) ⤏ 1) at_top"
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e: "0 < e"
define e' where "e' = min (1 / 2) e"
have e'_pos[arith]: "0 < e'" and e'_le: "e' ≤ e" and e'_lt1: "e' < 1"
using e by (simp_all add: e'_def)
have cpos[arith]: "0 < 1 - e'"
using e'_lt1 by simp
have c_lt1: "1 - e' < 1"
using e'_pos by simp
define K where "K = (1 / (1 - e')) powr (1 / ρ)"
have K_gt1[arith]: "1 < K"
using rho cpos c_lt1 by (simp add: K_def)
define δ where "δ = (K - 1) / 2"
have δ_pos[arith]: "0 < δ"
using K_gt1 by (simp add: δ_def)
have δ1_pos: "0 < 1 + δ"
using δ_pos by simp
have δ_lt_K: "1 + δ < K"
using K_gt1 by (simp add: δ_def field_simps)
have δ_lt: "(1 + δ) powr ρ < 1 / (1 - e')"
using powr_less_mono2[OF rho _ δ_lt_K] δ_pos rho cpos
by (simp add: K_def powr_powr)
have ev_ratio: "∀⇩F u in at_top. W (s u * (1 + δ)) / W (s u) < 1 / (1 - e')"
using order_tendstoD(2)[OF filterlim_compose[OF lim[OF δ1_pos] s] δ_lt] .
have ev_lower: "∀⇩F u in at_top. u < W (s u * (1 + δ))"
using s_gt1_mult[OF δ1_pos] s_gt1
proof eventually_elim
case (elim u)
hence "s u < s u * (1 + δ)"
using δ_pos by simp
thus ?case
using galois_strict[OF elim(1), of u] by simp
qed
have lower: "∀⇩F u in at_top. 1 - e' < W (s u) / u"
using ev_ratio ev_lower upper Ws_pos u_pos
proof eventually_elim
case (elim u)
have "u / W (s u) < W (s u * (1 + δ)) / W (s u)"
using elim(2,4) by (rule divide_strict_right_mono)
also have "… < 1 / (1 - e')"
using elim(1) .
finally have lt: "u / W (s u) < 1 / (1 - e')" .
have "u * (1 - e') < W (s u)"
using lt elim(4,5) cpos by (simp add: field_simps)
thus ?case
using elim(5) cpos by (simp add: field_simps)
qed
have e'1: "1 < 1 + e'"
using e'_pos by simp
have upperb: "∀⇩F u in at_top. W (s u) / u < 1 + e'"
using upper u_pos
proof eventually_elim
case (elim u)
have "W (s u) < u * (1 + e')"
using elim(1) mult_strict_left_mono[OF e'1 elim(2)] by simp
thus ?case
using elim(2) by (simp add: divide_less_eq mult.commute)
qed
show "∀⇩F u in at_top. ¦W (s u) / u - 1¦ < e"
using lower upperb
by eventually_elim (use e'_le in linarith)
qed
have Winv_ratio: "((λu. W (s u * y) / u) ⤏ y powr ρ) at_top" if y: "0 < y" for y
proof -
have eq: "∀⇩F u in at_top.
(W (s u * y) / W (s u)) * (W (s u) / u) = W (s u * y) / u"
using Ws_pos by eventually_elim (simp add: field_simps)
from Lim_transform_eventually[OF
tendsto_mult[OF filterlim_compose[OF lim[OF y] s] near_inv] eq]
show ?thesis
by simp
qed
define L where "L = x powr (1 / ρ)"
have L_pos: "0 < L"
using x by (simp add: L_def)
show ?thesis
unfolding L_def[symmetric] tendsto_iff dist_real_def
proof safe
fix e :: real
assume e: "0 < e"
define e' where "e' = min (L / 2) e"
have e'_pos: "0 < e'" and e'_le: "e' ≤ e" and e'_lt: "e' < L"
using e L_pos by (simp_all add: e'_def)
have cpos: "0 < L - e'"
using e'_lt by simp
define ylo where "ylo = (L - e' + L) / 2"
have ylo_pos: "0 < ylo"
using cpos L_pos by (simp add: ylo_def)
have c_lt_ylo: "L - e' < ylo"
using e'_pos by (simp add: ylo_def)
have ylo_lt_L: "ylo < L"
using e'_pos by (simp add: ylo_def)
have ylo_powr_lt_x: "ylo powr ρ < x"
using powr_less_mono2[OF rho less_imp_le[OF ylo_pos] ylo_lt_L] x rho
by (simp add: L_def powr_powr)
have ev_lt: "∀⇩F u in at_top. W (s u * ylo) < u * x"
using order_tendstoD(2)[OF Winv_ratio[OF ylo_pos] ylo_powr_lt_x] u_pos
by eventually_elim (simp add: field_simps)
have lower: "∀⇩F u in at_top. L - e' < s (u * x) / s u"
using ev_lt s_gt1_mult[OF ylo_pos] u_pos
proof eventually_elim
case (elim u)
have le: "s u * ylo ≤ s (u * x)"
using le_iff[OF elim(2), of "u * x"] elim(1) by simp
have "(L - e') * s u < ylo * s u"
using c_lt_ylo s_pos[OF elim(3)] by (intro mult_strict_right_mono) auto
also have "… ≤ s (u * x)"
using le by (simp add: mult.commute)
finally have "(L - e') * s u < s (u * x)" .
thus ?case
using s_pos[OF elim(3)] by (simp add: field_simps)
qed
define yhi where "yhi = (L + (L + e')) / 2"
have yhi_pos: "0 < yhi"
using L_pos e'_pos by (simp add: yhi_def)
have yhi_lt_c: "yhi < L + e'"
using e'_pos by (simp add: yhi_def)
have L_lt_yhi: "L < yhi"
using e'_pos by (simp add: yhi_def)
have x_lt_yhi_powr: "x < yhi powr ρ"
using powr_less_mono2[OF rho less_imp_le[OF L_pos] L_lt_yhi] x rho
by (simp add: L_def powr_powr)
have ev_gt: "∀⇩F u in at_top. u * x < W (s u * yhi)"
using order_tendstoD(1)[OF Winv_ratio[OF yhi_pos] x_lt_yhi_powr] u_pos
by eventually_elim (simp add: field_simps)
have upperb: "∀⇩F u in at_top. s (u * x) / s u < L + e'"
using ev_gt s_gt1_mult[OF yhi_pos] u_pos
proof eventually_elim
case (elim u)
have "s (u * x) < s u * yhi"
using galois_strict[OF elim(2)] elim(1) by simp
also have "s u * yhi < s u * (L + e')"
using yhi_lt_c s_pos[OF elim(3)] by (intro mult_strict_left_mono) auto
finally have "s (u * x) < s u * (L + e')" .
thus ?case
using s_pos[OF elim(3)] by (simp add: field_simps)
qed
show "∀⇩F u in at_top. ¦s (u * x) / s u - L¦ < e"
using lower upperb
by eventually_elim (use e'_le in linarith)
qed
qed
end