Theory Regular_Variation
section ‹Regularly Varying Functions›
theory Regular_Variation
imports
"Lemmas_Regular_Variation"
"Cauchy_Functional_Equation.Cauchy_Functional_Equation"
begin
text ‹We refer to Chapter~1 of the book by Bingham et al.~\cite{BGT}, and
Chapter~2 of the book by Resnick~\cite{Resnick}.›
subsection ‹ Definition and Basic Properties ›
subsubsection ‹ Regularly Varying Functions ›
definition regularly_varying :: "(real ⇒ real) ⇒ real ⇒ bool" where
"regularly_varying U ρ ⟷
U ∈ borel_measurable (restrict_space borel {0<..}) ∧
U ` {0<..} ⊆ {0<..} ∧
(∀x>0. ((λt. U (t * x) / U t) ⤏ x powr ρ) at_top)"
lemma regularly_varyingI:
assumes "U ∈ borel_measurable (restrict_space borel {0<..})"
and "⋀r. 0 < r ⟹ 0 < U r"
and "⋀x. 0 < x ⟹ ((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
shows "regularly_varying U ρ"
using assms by(auto simp: regularly_varying_def)
lemma regularly_varyingI'':
assumes "set_borel_measurable borel {0<..} U"
and "⋀r. 0 < r ⟹ 0 < U r"
and "⋀x. 0 < x ⟹ ((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
shows "regularly_varying U ρ"
using assms by(auto intro!: regularly_varyingI
simp: set_borel_measurable_iff_restrict_space)
lemma regularly_varyingI_total:
assumes "U ∈ borel_measurable borel"
and "⋀r. 0 < r ⟹ 0 < U r"
and "⋀x. 0 < x ⟹ ((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
shows "regularly_varying U ρ"
using assms by(auto intro!: regularly_varyingI measurable_restrict_space1)
lemma
assumes "regularly_varying U ρ"
shows regularly_varying_meas':"set_borel_measurable borel {0<..} U"
and regularly_varying_meas:"U ∈ borel_measurable (restrict_space borel {0<..})"
and regularly_varying_pos:"⋀r. 0 < r ⟹ 0 < U r"
and regularly_varying_lim:"⋀x. x > 0 ⟹ ((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
using assms
by(auto simp: regularly_varying_def set_borel_measurable_iff_restrict_space)
lemma regularly_varying_meas_log_exp:
assumes "regularly_varying U ρ"
shows "(λt. ln (U (exp t))) ∈ borel_measurable borel"
by(intro borel_measurable_ln measurable_compose[OF _ regularly_varying_meas[OF assms]]
measurable_restrict_space2) auto
lemma
assumes "regularly_varying U ρ"
shows regularly_varying_meas_o:
"⋀a. 0 ≤ a ⟹ (λx. indicat_real {a<..} x * U x) ∈ borel_measurable borel"
and regularly_varying_meas_c:
"⋀a. 0 < a ⟹ (λx. indicat_real {a..} x * U x) ∈ borel_measurable borel"
and regularly_varying_meas_Ioo:
"⋀a b. 0 ≤ a ⟹ (λx. indicat_real {a<..<b} x * U x) ∈ borel_measurable borel"
and regularly_varying_meas_Ico:
"⋀a b. 0 < a ⟹ (λx. indicat_real {a..<b} x * U x) ∈ borel_measurable borel"
and regularly_varying_meas_Ioc:
"⋀a b. 0 ≤ a ⟹ (λx. indicat_real {a<..b} x * U x) ∈ borel_measurable borel"
and regularly_varying_meas_Icc:
"⋀a b. 0 < a ⟹ (λx. indicat_real {a..b} x * U x) ∈ borel_measurable borel"
and regularly_varying_meas_o_ennreal:
"⋀a. 0 ≤ a ⟹ (λx. ennreal (U x) * indicator {a<..} x) ∈ borel_measurable borel"
and regularly_varying_meas_c_ennreal:
"⋀a. 0 < a ⟹ (λx. ennreal (U x) * indicator {a..} x) ∈ borel_measurable borel"
and regularly_varying_meas_Ioo_ennreal:
"⋀a b. 0 ≤ a ⟹ (λx. ennreal (U x) * indicator {a<..<b} x) ∈ borel_measurable borel"
and regularly_varying_meas_Ico_ennreal:
"⋀a b. 0 < a ⟹ (λx. ennreal (U x) * indicator {a..<b} x) ∈ borel_measurable borel"
and regularly_varying_meas_Ioc_ennreal:
"⋀a b. 0 ≤ a ⟹ (λx. ennreal (U x) * indicator {a<..b} x) ∈ borel_measurable borel"
and regularly_varying_meas_Icc_ennreal:
"⋀a b. 0 < a ⟹ (λx. ennreal (U x) * indicator {a..b} x) ∈ borel_measurable borel"
proof -
have *:"(λx. indicat_real A x * U x) ∈ borel_measurable borel"
if A:"A ∈ sets borel" "A ⊆ {0<..}" for A
proof -
have "(λx. indicat_real A x * U x) = (λx. indicat_real {0<..} x * U x * indicat_real A x)"
by standard (use A in "auto simp: indicator_eq_0_iff indicator_eq_1_iff")
moreover have "... ∈ borel_measurable borel"
using regularly_varying_meas'[OF assms] A
by(auto simp: set_borel_measurable_def)
ultimately show ?thesis
by argo
qed
have **:"(λx. ennreal (U x) * indicator A x) ∈ borel_measurable borel"
if A:"A ∈ sets borel" "A ⊆ {0<..}" for A
using measurable_compose[OF *[OF A] measurable_ennreal]
by(simp add: mult.commute ennreal_mult''[OF indicator_pos_le] ennreal_indicator)
show"⋀a. 0 ≤ a ⟹ (λx. indicat_real {a<..} x * U x) ∈ borel_measurable borel"
and "⋀a. 0 < a ⟹ (λx. indicat_real {a..} x * U x) ∈ borel_measurable borel"
and "⋀a b. 0 ≤ a ⟹ (λx. indicat_real {a<..<b} x * U x) ∈ borel_measurable borel"
and "⋀a b. 0 < a ⟹ (λx. indicat_real {a..<b} x * U x) ∈ borel_measurable borel"
and "⋀a b. 0 ≤ a ⟹ (λx. indicat_real {a<..b} x * U x) ∈ borel_measurable borel"
and "⋀a b. 0 < a ⟹ (λx. indicat_real {a..b} x * U x) ∈ borel_measurable borel"
and "⋀a. 0 ≤ a ⟹ (λx. ennreal (U x) * indicator {a<..} x) ∈ borel_measurable borel"
and "⋀a. 0 < a ⟹ (λx. ennreal (U x) * indicator {a..} x) ∈ borel_measurable borel"
and "⋀a b. 0 ≤ a ⟹ (λx. ennreal (U x) * indicator {a<..<b} x) ∈ borel_measurable borel"
and "⋀a b. 0 < a ⟹ (λx. ennreal (U x) * indicator {a..<b} x) ∈ borel_measurable borel"
and "⋀a b. 0 ≤ a ⟹ (λx. ennreal (U x) * indicator {a<..b} x) ∈ borel_measurable borel"
and "⋀a b. 0 < a ⟹ (λx. ennreal (U x) * indicator {a..b} x) ∈ borel_measurable borel"
by(auto intro!: * **)
qed
lemma regularly_varying_asymp_equiv:
assumes "regularly_varying U ρ"
and x:"0 < x"
shows "(λt. U (t * x)) ∼[at_top] (λt. x powr ρ * U t)"
using x by(auto intro!: asymp_equivI'_const regularly_varying_lim assms)
lemma regularly_varying_def2:
"regularly_varying U ρ ⟷
U ∈ borel_measurable (restrict_space borel {0<..}) ∧
U ` {0<..} ⊆ {0<..} ∧
(∀x>0. (λt. U (t * x)) ∼[at_top] (λt. x powr ρ * U t))"
proof safe
assume [simp]:"U ∈ borel_measurable
(restrict_space borel {0<..})"
and h'':"U ` {0<..} ⊆ {0<..}"
and h:"∀x>0. (λt. U (t * x)) ∼[at_top] (λt. x powr ρ * U t)"
hence h':"⋀x y. x > 0 ⟹ y > 0 ⟹ ¬ (U (y * x) = 0 ∧ x powr ρ * U y = 0)"
by fastforce
have "((λt. U (t * x) / U t) ⤏ x powr ρ) at_top" if x:"x > 0" for x
proof -
have "(λt. U (t * x)) ∼[at_top] (λt. x powr ρ * U t)"
using x h by blast
hence "((λy. U (y * x) / (x powr ρ * U y)) ⤏ 1) at_top"
using x h'[of x] by(fastforce intro!: asymp_equivD_strong simp: eventually_at_top_dense)
from tendsto_mult_right[where c="x powr ρ",OF this]
show ?thesis
using x by simp
qed
thus "regularly_varying U ρ"
using h'' by(auto intro!: regularly_varyingI)
qed(auto simp: regularly_varying_asymp_equiv regularly_varying_meas regularly_varying_pos)
lemma regularly_varying_cong:
assumes "⋀x. 0 < x ⟹ U x = T x"
shows "regularly_varying U ρ ⟷ regularly_varying T ρ"
proof -
have "regularly_varying T ρ"
if U:"regularly_varying U ρ" and x:"⋀x. 0 < x ⟹ U x = T x" for U T
proof(rule regularly_varyingI)
show "T ∈ borel_measurable
(restrict_space borel {0<..})"
using regularly_varying_meas[OF U] x
by(simp cong: measurable_cong')
next
show "((λt. T (t * x) / T t) ⤏ x powr ρ) at_top" if x_pos:"0 < x" for x
by(rule tendsto_cong[THEN iffD1,OF _ regularly_varying_lim[OF U]])
(use x_pos x in "auto intro!: eventually_at_top_linorderI[where c=1]")
qed(use U x regularly_varying_pos in fastforce)
thus ?thesis
using assms by auto
qed
lemma regularly_varying_ln_exp_iff:
"regularly_varying U ρ ⟷
U ∈ borel_measurable (restrict_space borel {0<..}) ∧
U ` {0<..} ⊆ {0<..} ∧
(∀x. ((λt. ln (U (exp (t + x))) - ln (U (exp t))) ⤏ ρ * x) at_top)"
unfolding regularly_varying_def
proof safe
fix x
assume " U ` {0<..} ⊆ {0<..}"
"∀y>0. ((λt. U (t * y) / U t) ⤏ y powr ρ) at_top"
hence U:"⋀x. 0 < x ⟹ 0 < U x"
and lim:"⋀y. 0 < y ⟹ ((λt. U (t * y) / U t) ⤏ y powr ρ) at_top"
by auto
hence "⋀y. 0 < y ⟹ ((λt. U (exp t * y) / U (exp t)) ⤏ y powr ρ) at_top"
using exp_at_top filterlim_compose by fast
hence "((λt. U (exp t * exp x) / U (exp t)) ⤏ exp x powr ρ) at_top"
using exp_gt_zero by blast
hence "((λt. U (exp (t + x)) / U (exp t)) ⤏ exp (x * ρ)) at_top"
using exp_gt_zero by (simp add: exp_add exp_powr_real)
hence "((λt. ln (U (exp (t + x)) / U (exp t))) ⤏ ln (exp (x * ρ))) at_top"
by(intro tendsto_ln) auto
thus "((λt. ln (U (exp (t + x))) - ln (U (exp t))) ⤏ ρ * x) at_top"
by(subst ln_divide_pos[symmetric]) (use U in "auto simp: mult.commute")
next
fix x :: real
assume h:"U ` {0<..} ⊆ {0<..}"
"∀y. ((λt. ln (U (exp (t + y))) - ln (U (exp t))) ⤏ ρ * y) at_top"
and x:"0 < x"
hence U:"⋀x. 0 < x ⟹ 0 < U x"
by blast
obtain a where a:"x = exp a"
using x exp_total by blast
have "((λt. ln (U (exp (t + a))) - ln (U (exp t))) ⤏ ρ * a) at_top"
using h by fast
hence "((λt. ln (U (exp (t + a)) / U (exp t))) ⤏ ρ * a) at_top"
by(subst ln_divide_pos) (use U in auto)
hence "((λt. ln (U (exp (t + a)) / U (exp t))) ⤏ ln (x powr ρ)) at_top"
by(simp add: a)
from tendsto_exp[OF this]
have "((λt. U (exp (t + a)) / U (exp t)) ⤏ x powr ρ) at_top"
using exp_ln[OF powr_gt_zero[of x,THEN iffD2]] x
by(simp add: exp_ln[OF divide_pos_pos[OF U[OF exp_gt_zero] U[OF exp_gt_zero]]])
hence *:"((λt. U (exp t * exp a) / U (exp t)) ⤏ x powr ρ) at_top"
by (simp add: mult_exp_exp)
have "((λt. U (t * exp a) / U t) ⤏ x powr ρ) at_top"
by(rule tendsto_cong[THEN iffD2,OF _ filterlim_compose[OF * ln_at_top]])
(auto intro!: eventually_at_top_linorderI[where c=1])
thus "((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
by(simp add: a)
qed
lemma regularly_varying_ln_exp:
assumes "regularly_varying U ρ"
shows "((λt. ln (U (exp (t + x))) - ln (U (exp t))) ⤏ ρ * x) at_top"
using assms by(simp add: regularly_varying_ln_exp_iff)
subsubsection ‹ Slowly Varying Functions ›
abbreviation "slowly_varying L ≡ regularly_varying L 0"
lemma slowly_varyingI:
assumes "L ∈ borel_measurable (restrict_space borel {0<..})"
and "⋀r. 0 < r ⟹ 0 < L r"
and "⋀x. 0 < x ⟹ ((λt. L (t * x) / L t) ⤏ 1) at_top"
shows "slowly_varying L"
by(auto intro!: regularly_varyingI assms)
lemma slowly_varyingI_total:
assumes "L ∈ borel_measurable borel"
and "⋀r. 0 < r ⟹ 0 < L r"
and "⋀x. 0 < x ⟹ ((λt. L (t * x) / L t) ⤏ 1) at_top"
shows "slowly_varying L"
by(auto intro!: regularly_varyingI_total assms)
lemma slowly_varying_lim:
"slowly_varying L ⟹ 0 < x ⟹ ((λt. L (t * x) / L t) ⤏ 1) at_top"
by(auto dest: regularly_varying_lim)
lemma slowly_varying_asymp_equiv:
assumes "slowly_varying L"
and x:"0 < x"
shows "(λt. L (t * x)) ∼[at_top] (λt. L t)"
using assms by(auto dest: regularly_varying_asymp_equiv)
lemma slowly_varying_def2:
"slowly_varying L ⟷
L ∈ borel_measurable (restrict_space borel {0<..}) ∧
L ` {0<..} ⊆ {0<..} ∧
(∀x>0. (λt. L (t * x)) ∼[at_top] (λt. L t))"
unfolding regularly_varying_def2 by auto
lemma slowly_varying_ln_exp:
assumes "slowly_varying L"
shows "((λt. ln (L (exp (t + x))) - ln (L (exp t))) ⤏ 0) at_top"
using regularly_varying_ln_exp[OF assms] by simp
lemma slowly_varying_const[simp]: "0 < c ⟹ slowly_varying (λx. c)"
by(auto intro!: slowly_varyingI_total)
lemma regularly_varying_powr[simp]: "regularly_varying (λx. x powr ρ) ρ"
by (auto simp: powr_mult
intro!: regularly_varyingI_total tendsto_eventually
eventually_at_top_linorderI[where c=1])
lemma regularly_varying_id[simp]: "regularly_varying (λx. x) 1"
by(auto intro!: regularly_varyingI_total simp: tendsto_iff frequently_def)
lemma slowly_varying_1: "slowly_varying (λx. 1)"
by simp
lemma regularly_varying_mult:
assumes U:"regularly_varying U ρ"
and V:"regularly_varying V η"
shows "regularly_varying (λx. U x * V x) (ρ + η)"
proof(rule regularly_varyingI)
fix x :: real
assume "0 < x"
then have *:"((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
and **:"((λt. V (t * x) / V t) ⤏ x powr η) at_top"
using assms by(auto simp: regularly_varying_lim)
show "((λt. U (t * x) * V (t * x) / (U t * V t)) ⤏ x powr (ρ + η)) at_top"
using tendsto_mult[OF * **] by(simp add: powr_add)
qed(use assms in
"auto simp: regularly_varying_pos regularly_varying_meas
intro!: mult_pos_pos borel_measurable_times")
corollary
shows regularly_varying_cmult:
"0 < c ⟹ regularly_varying U ρ ⟹ regularly_varying (λx. c * U x) ρ"
and regularly_varying_multc:
"0 < c ⟹ regularly_varying U ρ ⟹ regularly_varying (λx. U x * c) ρ"
using regularly_varying_mult[OF _ slowly_varying_const[of c],of U ρ]
by(auto simp: mult.commute)
lemma regularly_varying_inverse:
assumes "regularly_varying U ρ"
shows "regularly_varying (λx. 1 / U x) (- ρ)"
proof(rule regularly_varyingI)
fix x :: real
assume [arith]:"0 < x"
then have *:"((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
by(simp add: regularly_varying_lim assms)
show "((λt. 1 / U (t * x) / (1 / U t)) ⤏ x powr - ρ) at_top"
using tendsto_inverse[OF *] by(auto simp: powr_minus[symmetric])
qed(use assms in "auto dest: regularly_varying_meas regularly_varying_pos")
corollary regularly_varying_inverse_iff:
"regularly_varying (λx. 1 / U x) (- ρ) ⟷ regularly_varying U ρ"
using regularly_varying_inverse[of "λx. 1 / U x" "- ρ"]
regularly_varying_inverse[of U ρ] by fastforce
lemma regularly_varying_divide:
assumes U:"regularly_varying U ρ"
and V:"regularly_varying V η"
shows "regularly_varying (λx. U x / V x) (ρ - η)"
using regularly_varying_mult[OF U regularly_varying_inverse[OF V]]
by simp
lemma regularly_varying_comp_cmult:
assumes rv:"regularly_varying U ρ"
and c:"0 < c"
shows "regularly_varying (λx. U (c * x)) ρ"
proof(rule regularly_varyingI)
show "(λx. U (c * x)) ∈ borel_measurable (restrict_space borel {0<..})"
by(intro measurable_compose[OF _ regularly_varying_meas[OF rv]] measurable_restrict_space3)
(use c in auto)
show "((λt. U (c * (t * x)) / U (c * t)) ⤏ x powr ρ) at_top" if x:"0 < x" for x
unfolding mult.assoc[symmetric]
by(rule filterlim_compose[OF regularly_varying_lim[OF rv x]])
(use c filterlim_ident filterlim_tendsto_pos_mult_at_top in fastforce)
qed(use assms in "auto simp: regularly_varying_pos")
lemma regularly_varying_comp_multc:
assumes "regularly_varying U ρ"
and "0 < c"
shows "regularly_varying (λx. U (x * c)) ρ"
using regularly_varying_comp_cmult[OF assms] by(simp add: mult.commute)
lemma regularly_varying_iff_slowly_varying_divide_powr:
"regularly_varying U ρ ⟷ slowly_varying (λx. U x / x powr ρ)"
proof
assume "slowly_varying (λx. U x / x powr ρ)"
from regularly_varying_mult[OF this regularly_varying_powr[of ρ],simplified]
show "regularly_varying U ρ"
by(simp cong: regularly_varying_cong)
next
assume "regularly_varying U ρ"
from regularly_varying_divide[OF this regularly_varying_powr[of ρ]]
show "slowly_varying (λx. U x / x powr ρ)"
by simp
qed
corollary regularly_varying_decomp:
assumes "regularly_varying U ρ"
obtains L where
"slowly_varying L"
"⋀x. 0 < x ⟹ U x = x powr ρ * L x"
using assms regularly_varying_iff_slowly_varying_divide_powr by fastforce
lemma slowly_varying_ln:"slowly_varying (λx. ln (1 + x))"
proof(safe intro!: slowly_varyingI_total)
fix x :: real
assume x[arith]:"0 < x"
have tendsto_add':"(f ⤏ (0::real)) F ⟹ (g ⤏ b) F
⟹ ((λx::real. f x + g x) ⤏ b) F" for f g b F
using tendsto_add by fastforce
show "((λt. ln (1 + t * x) / ln (1 + t)) ⤏ 1) at_top"
proof(rule Lim_transform_eventually)
show "((λt. ln (1 / (1 + t) + (t * x) / (1 + t)) / ln (1 + t) + 1) ⤏ 1) at_top"
proof -
have "((λy. y * x / (1 + y)) ⤏ x) at_top"
proof(rule Lim_transform_eventually)
have "((λy. x / (1 / y + 1)) ⤏ x / 1) at_top"
by(intro tendsto_divide tendsto_add')
(use filterlim_ident real_tendsto_divide_at_top in fastforce)+
thus "((λy. x / (1 / y + 1)) ⤏ x) at_top"
by simp
show " ∀⇩F y in at_top. x / (1 / y + 1) = y * x / (1 + y)"
by(rule eventually_at_top_linorderI[where c=1])
(smt (verit, ccfv_SIG) Groups.mult_ac(2) add_divide_eq_if_simps(1) div_by_1
divide_divide_eq_right)
qed
show ?thesis
apply(rule tendsto_add')
apply(rule real_tendsto_divide_at_top[where c="ln x"])
apply(rule tendsto_ln)
apply(rule tendsto_add')
apply(rule real_tendsto_divide_at_top[where c=1])
apply simp
using filterlim_ident filterlim_tendsto_add_at_top
apply fastforce
apply fact
apply arith
using filterlim_compose filterlim_ident filterlim_tendsto_add_at_top ln_at_top
apply blast
apply simp
done
qed
next
show " ∀⇩F y in at_top. ln (1 / (1 + y) + y * x / (1 + y)) / ln (1 + y) + 1 =
ln (1 + y * x) / ln (1 + y)"
proof(rule eventually_at_top_linorderI[where c=1])
fix y :: real
assume y[arith]: "1 ≤ y"
have "ln (1 / (1 + y) + y * x / (1 + y)) / ln (1 + y) + 1
= ln (1 / (1 + y) + y * x / (1 + y)) / ln (1 + y) + ln (1 + y) / ln (1 + y)"
by simp
also have "... = (ln (1 / (1 + y) + y * x / (1 + y)) + ln (1 + y)) / ln (1 + y)"
by algebra
also have "... = ln ((1 / (1 + y) + y * x / (1 + y)) * (1 + y)) / ln (1 + y)"
by(subst ln_mult_pos) (auto simp add: add_sign_intros(2))
also have "... = ln (1 + y * x) / ln (1 + y)"
by (metis add_divide_distrib divide_cancel_right ln_0 nonzero_eq_divide_eq)
finally show "ln (1 / (1 + y) + y * x / (1 + y)) / ln (1 + y) + 1 =
ln (1 + y * x) / ln (1 + y)" .
qed
qed
qed auto
text ‹ Exercise 2.8 of the book~\cite{Resnick}.›
lemma slowly_varying_tendsto_gr_le_eq:
fixes U :: "'a :: linordered_field ⇒ 'b::{real_normed_div_algebra, field}"
shows "(∀x>1. ((λt. U (t * x) / U t) ⤏ 1) at_top)
⟷ (∀x. 0 < x ⟶ x < 1 ⟶ ((λt. U (t * x) / U t) ⤏ 1) at_top)"
proof safe
assume h:"(∀x>1. ((λt. U (t * x) / U t) ⤏ 1) at_top)"
fix x :: 'a
assume x[arith]:"0 < x" "x < 1"
then have "1 < 1 / x"
by simp
hence "((λt. U (t * (1 / x)) / U t) ⤏ 1) at_top"
using h by blast
hence "((λt. U ((t * x) * (1 / x)) / U (t * x)) ⤏ 1) at_top"
by(rule filterlim_compose)
(use x in
"auto simp: filterlim_at_top eventually_at_top_linorder pos_divide_le_eq[of x,symmetric]")
hence *:"((λt. U t / U (t * x)) ⤏ 1 / 1) at_top"
by simp
thus "((λt. U (t * x) / U t) ⤏ 1) at_top"
using tendsto_inverse[OF *] by simp
next
assume h:"∀x>0. x < 1 ⟶ ((λt. U (t * x) / U t) ⤏ 1) at_top"
fix x :: 'a
assume x[arith]:"1 < x"
then have "0 < 1 / x" "1 / x < 1"
by simp_all
hence "((λt. U (t * (1 / x)) / U t) ⤏ 1) at_top"
using h by blast
hence "((λt. U ((t * x) * (1 / x)) / U (t * x)) ⤏ 1) at_top"
by(rule filterlim_compose)
(use x in
"auto simp: filterlim_at_top eventually_at_top_linorder pos_divide_le_eq[of x,symmetric]")
hence *:"((λt. U t / U (t * x)) ⤏ 1 / 1) at_top"
by simp
thus "((λt. U (t * x) / U t) ⤏ 1) at_top"
using tendsto_inverse[OF *] by simp
qed
lemma slowly_varying_iff_all_gr_1:
assumes "L ∈ borel_measurable (restrict_space borel {0<..})"
and "⋀x. 0 < x ⟹ 0 < L x"
shows "slowly_varying L ⟷ (∀x>1. ((λt. L (t * x) / L t) ⤏ 1) at_top)"
proof
assume h:"∀x>1. ((λt. L (t * x) / L t) ⤏ 1) at_top"
show "slowly_varying L"
proof(rule slowly_varyingI)
fix x :: real
have *:"x = 1 ⟹ ((λt. L (t * x) / L t) ⤏ 1) at_top"
using assms
by(intro tendsto_eventually eventually_at_top_linorderI[where c=1])
(metis divide_self less_irrefl mult_1_right less_le_trans zero_less_one)
assume "0 < x"
then consider "0 < x" "x < 1" | "x = 1" | "1 < x"
by linarith
thus "((λt. L (t * x) / L t) ⤏ 1) at_top"
by cases (use h slowly_varying_tendsto_gr_le_eq assms * in auto)
qed(use assms in auto)
qed(auto intro!: slowly_varying_lim)
lemma slowly_varying_iff_ne_1:
assumes L_meas:"L ∈ borel_measurable (restrict_space borel {0<..})"
and L_pos:"⋀x. 0 < x ⟹ 0 < L x"
and L_mono:"mono_on {0<..} L"
shows "slowly_varying L ⟷ (∃x≠1. x > 0 ∧ ((λt. L (t * x) / L t) ⤏ 1) at_top)"
proof safe
fix x' :: real
assume x'_ne1:"x' ≠ 1"
and x'_pos:"0 < x'"
and lim':"((λt. L (t * x') / L t) ⤏ 1) at_top"
have lim'':"((λt. L (t * (1 / x')) / L t) ⤏ 1) at_top"
using filterlim_compose[OF lim'
filterlim_compose[OF filterlim_ident
filterlim_tendsto_pos_mult_at_top[OF _ _ filterlim_ident,
where c="1 / x'" and f="λx. 1 / x'"]]]
tendsto_inverse_real x'_pos
by fastforce
define x where "x ≡ if 1 < x' then x' else 1 / x'"
have x1[arith]:"1 < x" and x_pos[arith]:"0 < x" and x_pos'[arith]:"0 < 1 / x" "1 / x < 1"
using x'_ne1 x'_pos
by(auto simp: x_def)
have lim_x1:"((λt. L (t * x) / L t) ⤏ 1) at_top"
and lim_x2:"((λt. L (t * (1 / x)) / L t) ⤏ 1) at_top"
using lim' lim'' by(auto simp: x_def)
have lim_y1:"((λt. L (t * y) / L t) ⤏ 1) at_top"
if y[arith]:"1 / x ≤ y" "y ≤ x" for y
by(rule tendsto_sandwich[OF _ _ lim_x2 lim_x1])
(auto intro!: eventually_at_top_linorderI[where c=1] less_imp_le[OF L_pos]
divide_right_mono mono_onD[OF L_mono] mult_pos_pos simp del: times_divide_eq_right)
have lim_y:"1 ≤ y ⟹ y ≤ x^n ⟹ ((λt. L (t * y) / L t) ⤏ 1) at_top" for y n
proof(induction n arbitrary: y)
case 0
then show ?case
using L_pos
by(auto intro!: tendsto_cong[THEN iffD1,OF _ tendsto_const]
eventually_at_top_linorderI[where c=1] simp: order.strict_iff_order)
next
fix y n
assume ih:"⋀z. 1 ≤ z ⟹ z ≤ x ^ n ⟹
((λt. L (t * z) / L t) ⤏ 1) at_top"
and y1[arith]:"1 ≤ y" and y2:"y ≤ x ^ Suc n"
show "((λt. L (t * y) / L t) ⤏ 1) at_top"
proof(cases "x < y")
assume [arith]:"x < y"
then have y:"1 ≤ y / x" "y / x ≤ x ^ n"
using y2 by (auto simp add: cross3_simps pos_divide_le_eq)
note lim_ih =ih[OF this]
have 1:"∀⇩F t in at_top. L (t * y) / L t
= (L (t * (y / x)) / L t) * (L (t * y) / L (t * y * 1 / x))"
using y order.strict_iff_order[THEN iffD1,OF L_pos]
by(auto intro!: eventually_at_top_linorderI[where c=1])
have "((λt. (L (t * (y / x)) / L t) * (L (t * y) / L (t * y * 1 / x))) ⤏ 1 * 1) at_top"
using tendsto_inverse[OF filterlim_compose[OF lim_x2
filterlim_at_top_mult_tendsto_pos[OF tendsto_const[of y] _ filterlim_ident]]]
by(intro tendsto_mult lim_ih) simp
thus ?thesis
using tendsto_cong[OF 1] by auto
qed(auto intro!: lim_y1)
qed
show "slowly_varying L"
proof(safe intro!: slowly_varying_iff_all_gr_1[THEN iffD2] assms)
fix y :: real
assume y:"1 < y"
then obtain n where n:"y ≤ x ^ n"
using power_of_nat_log_ge x1 by blast
thus "((λt. L (t * y) / L t) ⤏ 1) at_top"
using y by(auto intro!: lim_y)
qed
qed(auto simp: slowly_varying_lim intro!: exI[where x=2])
subsection ‹Uniform Convergence Theorem on Intervals›
theorem slowly_varying_UCT:
assumes sv:"slowly_varying L"
and a: "0 < a"
shows "uniform_limit {a..b} (λt x. L (t * x) / L t) (λx. 1) at_top"
proof(cases "a < b")
assume a_le_b:"a < b"
have lna_le_lnb:"ln a < ln b"
using a_le_b a by simp
have eb: "∀⇩F i in at_top.
∀x∈{ln a..ln b}. ln (L (exp i * exp x) / L (exp i)) ∈ {- 1..1}" (is ?eb)
and "uniform_limit {ln a..ln b}
(λt x. ln (L (exp (t + x)) / L (exp t))) (λx. 0) at_top" (is ?ul)
proof -
show g1:?ul
proof(safe intro!: uniform_limitI)
fix e :: real
assume e:"0 < e"
let ?h = "λt. ln (L (exp t))"
let ?A = "abs (ln b) + abs (ln a)"
have A:"0 < ?A"
using a lna_le_lnb by linarith
note [measurable] = regularly_varying_meas_log_exp[OF sv]
define I where "I ≡ λt. {t..t + 2 * ?A}"
define E where "E ≡ λt. I t ∩ {x. e / 2 ≤ ¦?h x - ?h t¦}"
define E' where "E' ≡ λt. I 0 ∩ {x. e / 2 ≤ ¦?h (x + t) - ?h t¦}"
have [measurable]: "⋀t. I t ∈ sets borel" "⋀t. E t ∈ sets borel"
"⋀t. E' t ∈ sets borel"
by(auto simp: E_def E'_def I_def)
have measE_eq_measE':"measure lborel (E t) = measure lborel (E' t)" for t
proof -
{
fix x
have "x ∈ (λx. x - t) ` E t ⟷ x + t ∈ (+) t ` (λx. x - t) ` E t"
by (simp add: image_iff)
also have "... ⟷ x + t ∈ E t"
by(auto simp: image_image)
also have "x + t ∈ E t ⟷ x ∈ E' t"
by(auto simp: E_def E'_def I_def)
finally have "x ∈ (λx. x - t) ` E t ⟷ x ∈ E' t" .
}
hence 1:"(λx. x - t) ` E t = E' t"
by blast
have "measure lborel (E t) = measure lebesgue (E t)"
by simp
also have "... = measure lebesgue ((λx. x - t) ` E t)"
by(simp add: measure_translation_subtract)
also have "... = measure lebesgue (E' t)"
by (simp add: 1)
also have "... = measure lborel (E' t)"
by simp
finally show ?thesis .
qed
have "((λt. integral⇧L lborel (indicat_real (E' t)))
⤏ integral⇧L lborel (λx::real. 0)) at_top"
proof(rule integral_dominated_convergence_real)
show "AE x in lborel. norm (indicat_real (E' t) (x :: real))
≤ indicat_real {0..2 * ?A} x" for t
by(auto simp: E'_def I_def indicator_def)
next
have "∀⇩F t in at_top. ¦?h (x + t) - ?h t¦ < e / 2" for x
using tendstoD[OF tendsto_rabs[OF regularly_varying_ln_exp[OF sv,of x]]
half_gt_zero[OF e]]
by(simp add: dist_real_def add.commute)
then obtain T where T:"⋀x t. T x ≤ t ⟹ ¦?h (x + t) - ?h t¦ < e / 2"
unfolding eventually_at_top_linorder by meson
hence "∀⇩F t in at_top. indicat_real (E' t) x = 0" for x
unfolding eventually_at_top_linorder
by(fastforce intro!: exI[where x="T x"] simp: indicator_def E'_def)
hence "((λt. indicat_real (E' t) x) ⤏ 0) at_top" for x
by (simp add: tendsto_eventually)
thus "AE x in lborel. ((λt. indicat_real (E' t) x) ⤏ 0) at_top"
by blast
qed (auto simp: emeasure_lborel_Icc_eq)
from tendstoD[OF this min_less_iff_conj[THEN iffD2
,OF conjI[OF half_gt_zero[OF e] half_gt_zero[OF A]]]]
obtain t0 where t0:"⋀t. t0 ≤ t ⟹ measure lborel (E t) < min (e / 2) (?A / 2)"
unfolding measE_eq_measE' dist_real_def eventually_at_top_linorder
by auto
show "∀⇩F i in at_top. ∀x∈{ln a..ln b}. dist (ln (L (exp (i + x)) / L (exp i))) 0 < e"
proof(safe intro!: eventually_at_top_linorderI[where c="t0 + ¦ln b¦ + ¦ln a¦"])
fix t x
assume t:"t0 + ¦ln b¦ + ¦ln a¦ ≤ t" and x:"x ∈ {ln a..ln b}"
have "(I (t + x) ∩ I t) - (E (t + x) ∪ E t) ≠ {}"
proof
assume ne:"I (t + x) ∩ I t - (E (t + x) ∪ E t) = {}"
have "0 ≤ x ⟹ I (t + x) ∩ I t = {t + x ..t + 2*?A}"
"x ≤ 0 ⟹ I (t + x) ∩ I t = {t..t + x + 2*?A}"
unfolding Int_atLeastAtMost I_def using x lna_le_lnb by force+
hence "0 ≤ x ⟹ measure lborel (I (t + x) ∩ I t) = 2 * ?A - x"
"x ≤ 0 ⟹ measure lborel (I (t + x) ∩ I t) = 2 * ?A + x"
using x lna_le_lnb by auto
hence *:"measure lborel (I (t + x) ∩ I t) ≥ ?A"
using x by fastforce
have "measure lborel (E (t + x) ∪ E t)
≤ measure lborel (E (t + x)) + measure lborel (E t)"
by(simp add: measure_Un_le)
also have "... < ?A / 2 + ?A / 2"
by(rule add_strict_mono)
(use t0[of t] t t0[of "t + x"] x in fastforce)+
finally have **:"measure lborel (E (t + x) ∪ E t) < ?A"
by argo
have "0 = ?A - ?A"
by simp
also have "... < measure lborel (I (t + x) ∩ I t) - measure lborel (E (t + x) ∪ E t)"
using * ** by argo
also have "... ≤ measure lborel ((I (t + x) ∩ I t) - (E (t + x) ∪ E t))"
by (metis Diff_Diff_Int E_def I_def ‹⋀t. E t ∈ sets borel›
‹⋀t. I t ∈ sets borel› compact_Icc fmeasurable.Un fmeasurableI2
fmeasurable_compact inf_le1 measure_diff_le_measure_setdiff
sets.Diff sets_lborel)
also have "... = 0"
unfolding ne by simp
finally show False
by simp
qed
then obtain k where k:"k ∈ I (t + x)" "k ∈ I t"
"k ∉ {y. e / 2 ≤ ¦?h y - ?h (t + x)¦}" "k ∉ {y. e / 2 ≤ ¦?h y - ?h t¦}"
unfolding E_def by blast
have "¦ln (L (exp (t + x)) / L (exp t)) - 0¦ = ¦?h (t + x) - ?h t¦"
by(auto intro!: ln_divide_pos arg_cong[where f=abs] regularly_varying_pos[OF sv])
also have "... ≤ ¦?h k - ?h (t + x) ¦ + ¦?h k - ?h t¦"
by force
also have "... < e / 2 + e / 2"
by(intro add_strict_mono) (use k in fastforce)+
finally show "dist (ln (L (exp (t + x)) / L (exp t))) 0 < e"
by (simp add: dist_real_def)
qed
qed
show ?eb
by(rule eventually_mono[OF uniform_limitD[OF g1,of 1]])
(auto simp: exp_add)
qed
hence "uniform_limit {ln a..ln b} (λt x. ln (L (exp t * exp x) / L (exp t))) (λx. 0) at_top"
by (simp add: exp_add)
hence "uniform_limit {ln a..ln b}
(λi x. exp (ln (L (exp i * exp x) / L (exp i)))) (λx. exp 0) at_top"
by(safe intro!: compact_uniformly_continuous continuous_on_exp
eb uniform_limit_compose_uniformly_continuous_on[where B="{-1..1}" and g' = "λx. 0"])
auto
hence "uniform_limit {ln a..ln b} (λi x. L (exp i * exp x) / L (exp i)) (λx. 1) at_top"
using exp_ln[OF divide_pos_pos[OF regularly_varying_pos[OF sv] regularly_varying_pos[OF sv]]]
by auto
hence "uniform_limit {a..b} (λi x. L (exp i * exp (ln x)) / L (exp i)) (λx. 1) at_top"
using uniform_limit_compose'[where A="{ln a..ln b}"
and f="λi x. L (exp i * exp x) / L (exp i)"
and g="λx. 1" and h=ln and B="{a..b}"] a by auto
hence "uniform_limit {a..b} (λi x. L (exp i * x) / L (exp i)) (λx. 1) at_top"
by(intro uniform_limit_cong[of _ _ "λi x. L (exp i * x) / L (exp i)",THEN iffD1])
(use a in auto)
hence "uniform_limit {a..b} (λi x. L (exp (ln i) * x) / L (exp (ln i))) (λx. 1) at_top"
by(intro filterlim_compose[OF _ ln_at_top])
thus "uniform_limit {a..b} (λi x. L (i * x) / L i) (λx. 1) at_top"
by(intro uniform_limit_cong[of _ _ "λi x. L (i * x) / L i",THEN iffD1]
eventually_at_top_linorderI[where c=1]) auto
next
assume "¬ a < b"
then consider "a = b" | "b < a"
by fastforce
thus ?thesis
by cases (use a slowly_varying_lim[OF sv] in auto)
qed
corollary regularly_varying_UCT_interval:
assumes sv:"regularly_varying U ρ"
and a: "0 < a"
shows "uniform_limit {a..b} (λt x. U (t * x) / U t) (λx. x powr ρ) at_top"
proof -
obtain L where L_sv: "slowly_varying L"
and eq_L: "⋀x. 0 < x ⟹ U x = x powr ρ * L x"
using regularly_varying_decomp[OF sv] by blast
have 1:"uniform_limit {a..b} (λt x. x powr ρ * (L (t * x) / L t)) (λx. x powr ρ * 1) at_top"
by(intro uniform_lim_mult_bdd1[OF slowly_varying_UCT] assms L_sv
compact_imp_bounded compact_continuous_image continuous_on_powr)
(use a in auto)
have 2:"uniform_limit {a..b} (λt x. (x powr ρ * t powr ρ * L (t * x) / (t powr ρ * L t)))
(λx. x powr ρ) at_top"
by(auto intro!: uniform_limit_cong[THEN iffD1,OF _ _ 1] eventually_at_top_linorderI[of 1])
show ?thesis
using a
by(auto intro!: uniform_limit_cong[THEN iffD1,OF _ _ 2] eventually_at_top_linorderI[of 1]
simp: powr_mult eq_L)
qed
corollary regularly_varying_UCT_interval_ln_exp:
assumes rv:"regularly_varying U ρ"
defines "h ≡ λx. ln (U (exp x))"
shows "uniform_limit {a..b} (λt x. h (t + x) - h t) (λx. ρ * x) at_top"
proof -
have 1:"uniform_limit {exp a..exp b} (λt x. U (t * x) / U t) (λx. x powr ρ) at_top"
by(auto intro!: regularly_varying_UCT_interval[OF rv])
have "uniform_limit {exp a..exp b} (λt x. ln (U (t * x) / U t)) (λx. ln (x powr ρ)) at_top"
proof(intro uniform_limit_compose_uniformly_continuous_on[OF 1]
uniform_limit_eventually_in[OF regularly_varying_UCT_interval[OF rv]])
define e where "e ≡ min (exp (a * ρ)) (exp (b * ρ))"
have e:"0 < e"
by(simp add: e_def)
define e' where "e' ≡ e / 2"
have e':"e' < e" "0 < e'"
using dense e'_def e by auto
have pos:"0 < min (exp (a * ρ)) (exp (b * ρ)) - e'"
using e' by(auto simp: e_def)
thus "uniformly_continuous_on
{min (exp (a * ρ)) (exp (b * ρ)) - e'..max (exp (a * ρ)) (exp (b * ρ)) + e'} ln"
(is "uniformly_continuous_on ?B ln")
using e' by(auto intro!: continuous_on_ln compact_uniformly_continuous)
show "0 < e'"
by fact
fix x y
assume x:"x ∈ {exp a .. exp b}"
and d:"dist (x powr ρ) y < e'"
have a_le_b:"a ≤ b"
by(rule ccontr) (use x in auto)
have xin:"x powr ρ ∈ {min (exp (a * ρ)) (exp (b * ρ))..max (exp (a * ρ)) (exp (b * ρ))}"
(is "_ ∈ ?C")
proof(cases "0 ≤ ρ")
assume h:"0 ≤ ρ"
then have mono:"mono_on {exp a .. exp b} (λx. x powr ρ)"
by(auto intro!: mono_onI powr_mono2 order.trans[OF exp_ge_zero])
have 1:"min (exp (a * ρ)) (exp (b * ρ)) = exp (a * ρ)"
and 2: "max (exp (a * ρ)) (exp (b * ρ)) = exp (b * ρ)"
using h a_le_b by (simp_all add: mult_le_cancel_right)
have "(λx. x powr ρ) ` {exp a .. exp b} = {exp (a * ρ) .. exp (b * ρ)}"
unfolding exp_powr_real[symmetric]
by(intro image_mono_on_continuous_on_Icc mono continuous_on_powr)
(use a_le_b in auto)
thus ?thesis
using x by(auto simp: 1 2)
next
assume h:"¬ 0 ≤ ρ"
then have mono:"mono_on {exp a .. exp b} (λx. - (x powr ρ))"
by(intro mono_onI)
(metis atLeastAtMost_iff basic_trans_rules(22) exp_gt_zero neg_le_iff_le nle_le
powr_mono2')
have 1:"min (exp (a * ρ)) (exp (b * ρ)) = exp (b * ρ)"
and 2: "max (exp (a * ρ)) (exp (b * ρ)) = exp (a * ρ)"
using h a_le_b by (simp_all add: mult_le_cancel_right)
have "(λx. x powr ρ) ` {exp a .. exp b} = uminus ` (λx. - (x powr ρ)) ` {exp a .. exp b}"
by force
also have "... = uminus ` {- (exp (a * ρ))..- (exp (b * ρ))}"
unfolding exp_powr_real[symmetric]
by(intro image_mono_on_continuous_on_Icc mono continuous_on_minus
continuous_on_powr arg_cong[where f="(`) uminus"])
(use a_le_b in auto)
also have "... = {exp (b * ρ) .. exp (a * ρ)}"
by auto
finally show ?thesis
using x by(auto simp: 1 2)
qed
show "y ∈ ?B"
using xin d by(auto simp: dist_real_def)
qed auto
hence "uniform_limit {exp a..exp b}
(λt x. ln (U (exp t * x) / U (exp t))) (λx. ρ * ln x) at_top"
using filterlim_compose[OF _ exp_at_top] by auto
hence "uniform_limit {a..b}
(λt x. ln (U (exp t * exp x) / U (exp t))) (λx. ρ * ln (exp x)) at_top"
by(intro uniform_limit_compose'[where h=exp]) auto
hence "uniform_limit {a..b} (λt x. ln (U (exp (t + x)) / U (exp t))) (λx. ρ * x) at_top"
by (simp add: exp_add)
thus "uniform_limit {a..b} (λt x. h (t + x) - h t) (λx. ρ * x) at_top"
using regularly_varying_pos[OF rv exp_gt_zero] ln_divide_pos
by(simp add: h_def cong: uniform_limit_cong')
qed
corollary slowly_varying_UCT_interval_ln_exp:
assumes sv:"slowly_varying L"
defines "h ≡ λx. ln (L (exp x))"
shows "uniform_limit {a..b} (λt x. h (t + x) - h t) (λx. 0) at_top"
using regularly_varying_UCT_interval_ln_exp[OF sv] by(simp add: h_def)
corollary regularly_varying_compose:
assumes rv1:"regularly_varying U ρ"
and rv2:"regularly_varying V η"
and lim:"filterlim U at_top at_top"
shows "regularly_varying (λx. V (U x)) (ρ * η)"
proof(rule regularly_varyingI)
fix x ::real
assume x:"0 < x"
hence "x powr ρ > 0"
by simp
then obtain i where i_pos:"0 < i" and i: "0 < x powr ρ - i"
by (meson diff_gt_0_iff_gt field_lbound_gt_zero)
show "((λt. V (U (t * x)) / V (U t)) ⤏ x powr (ρ * η)) at_top"
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e:"0 < e"
from regularly_varying_UCT_interval[OF rv2 i,of "x powr ρ + i"] half_gt_zero[OF e]
obtain Tv where Tv:"⋀y t. Tv ≤ t ⟹ x powr ρ - i ≤ y ⟹ y ≤ x powr ρ + i
⟹ ¦V (t * y) / V t - y powr η¦ < e / 2"
unfolding uniform_limit_iff dist_real_def eventually_at_top_linorder
by (meson atLeastAtMost_iff)
obtain T1 where T1:"⋀t. T1 ≤ t ⟹ Tv ≤ U t"
using lim unfolding filterlim_at_top eventually_at_top_linorder
by fastforce
obtain T2 where T2:"⋀t. T2 ≤ t ⟹ ¦U (t * x) / U t - x powr ρ¦ < i"
using regularly_varying_lim[OF rv1 x] i_pos
by(fastforce simp: tendsto_iff eventually_at_top_linorder dist_real_def)
obtain T3 where T3:"⋀t. T3 ≤ t ⟹ ¦(U (t * x) / U t) powr η - x powr (ρ * η)¦ < e / 2"
using tendstoD[OF tendsto_powr[OF regularly_varying_lim[OF rv1 x]
tendsto_const[of η]] half_gt_zero[OF e]]
x
by(fastforce simp: eventually_at_top_linorder powr_powr dist_real_def)
define T where "T ≡ max (max 1 T1) (max T2 T3)"
show " ∀⇩F t in at_top. ¦V (U (t * x)) / V (U t) - x powr (ρ * η)¦ < e"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
then have t_pos:"0 < t" and Tvt:"Tv ≤ U t"
and ti:"¦U (t * x) / U t - x powr ρ¦ < i"
and tpowr:"¦(U (t * x) / U t) powr η - x powr (ρ * η)¦ < e / 2"
using T1 T2 T3 by(auto simp: T_def)
have "¦V (U (t * x)) / V (U t) - x powr (ρ * η)¦
= ¦V (U t * (U (t * x) / U t)) / V (U t) - x powr (ρ * η)¦"
using regularly_varying_pos[OF rv1 t_pos] by simp
also have "... ≤ ¦V (U t * (U (t * x) / U t)) / V (U t) - (U (t * x) / U t) powr η¦
+ ¦(U (t * x) / U t) powr η - x powr (ρ * η)¦"
by linarith
also have "... < e / 2 + e / 2"
using ti by(intro add_strict_mono tpowr Tv Tvt) auto
finally show "¦V (U (t * x)) / V (U t) - x powr (ρ * η)¦ < e"
by argo
qed
qed
qed(use measurable_compose[OF
measurable_restrict_space2[OF _ regularly_varying_meas[OF rv1]]
regularly_varying_meas[OF rv2]]
in "auto intro!: regularly_varying_pos[OF rv1] regularly_varying_pos[OF rv2]")
lemma
assumes sv:"slowly_varying L"
defines "h ≡ λx. ln (L (exp x))"
shows slowly_varying_eventually_bounded_interval:
"∀⇩F x in at_top. ∀a≥x. ∀b≥a. bounded (L ` {a..b})"
and slowly_varying_eventually_bounded_interval_strong:
"∀⇩F x in at_top. ∀a≥x. ∀b≥a. ∃A>0. ∃B. L ` {a..b} ⊆ {A..B}"
and slowly_varying_eventually_bounded_interval_ln_exp:
"∀⇩F x in at_top. ∀a≥x. ∀b≥a. bounded (h ` {a..b})"
proof -
have "∃T::real. ∀t≥T. ∀n. t ≤ T + Suc n ⟶ ¦h t¦ < Suc n + ¦h T¦"
proof -
from uniform_limitD[where e=1,OF slowly_varying_UCT_interval_ln_exp[OF sv,of 0 1]]
obtain T where T':"⋀t x. t ≥ T ⟹ 0 ≤ x ⟹ x ≤ 1 ⟹ ¦h (t + x) - h t¦ < 1"
by(fastforce simp: eventually_at_top_linorder h_def)
have "⋀t. T ≤ t ⟹ t ≤ T + Suc n ⟹ ¦h t¦ < Suc n + ¦h T¦" for n
proof(induction n)
case ih:(Suc n')
then consider "t ≤ T + Suc n'" | "T + Suc n' ≤ t" "t ≤ T + Suc (Suc n')"
by argo
thus ?case
proof cases
assume t:"T + Suc n' ≤ t" "t ≤ T + Suc (Suc n')"
define t' where "t' ≡ t - 1"
have t':"T ≤ t'" "t' ≤ T + Suc n'"
using t by(auto simp: t'_def)
then have "¦h t¦ < 1 + ¦h t'¦"
using T'[of t' 1] by(simp add: t'_def)
also have "... < real (Suc (Suc n')) + ¦h T¦"
using ih t' by fastforce
finally show ?thesis .
qed(use ih in fastforce)
qed(use T'[of T "_ - T"] in fastforce)
thus ?thesis
by blast
qed
then obtain T :: real where T:"⋀t n. T ≤ t ⟹ t ≤ T + Suc n ⟹ ¦h t¦ < Suc n + ¦h T¦"
by fast
show h:"∀⇩F x in at_top. ∀a≥x. ∀b≥a. bounded (h ` {a..b})"
proof(intro eventually_at_top_linorderI[where c=T] allI impI)
fix t a b :: real
assume tab:"T ≤ t" "t ≤ a" "a ≤ b"
then obtain N where N:"b ≤ T + Suc N"
by (metis Multiseries_Expansion.intyness_simps(5) add.commute
add_mono_thms_linordered_semiring(1) arithmetic_simps(49) diff_le_eq
not0_implies_Suc of_nat_0_le_iff real_arch_simple)
show "bounded (h ` {a..b})"
using tab N
by(auto intro!: boundedI[where B="Suc N + ¦h T¦"]
less_imp_le[of _ "Suc N + ¦h T¦"] T simp del: of_nat_Suc)
qed
have *:"∀⇩F x in at_top. ∀a≥x. ∀b≥a. ∃A>0. ∃B. (λx. L (exp x)) ` {a..b} ⊆ {A..B}"
proof(safe intro!: eventually_mono[OF h])
fix t a b
assume "∀a≥t. ∀b≥a. bounded (h ` {a..b})"
and "t ≤ a" "a ≤ b"
then obtain A B where AB:"h ` {a..b} ⊆ {A..B}"
unfolding bounded_subset_cball cball_eq_atLeastAtMost by blast
show "∃A>0. ∃B. (λx. L (exp x)) ` {a..b} ⊆ {A..B}"
by(intro exI[where x="exp A"] conjI[OF _ exI[where x="exp B"]] image_subsetI exp_gt_zero)
(metis AB regularly_varying_pos[OF sv exp_gt_zero] h_def
atLeastAtMost_iff exp_le_cancel_iff exp_ln_iff image_subset_iff)
qed
then obtain T where T:
"⋀a b. T ≤ a ⟹ a ≤ b ⟹ ∃A>0. ∃B. (λx. L (exp x)) ` {a..b} ⊆ {A..B}"
unfolding eventually_at_top_linorder by metis
have **:"a ≤ b ⟹ exp ` {a..b} = {exp a..exp b}" for a b :: real
by(intro image_mono_on_continuous_on_Icc)
(auto intro!: continuous_on_exp ord.mono_onI)
show ***:"∀⇩F x in at_top. ∀a≥x. ∀b≥a. ∃A>0. ∃B. L ` {a..b} ⊆ {A..B}"
proof(safe intro!: eventually_at_top_linorderI[where c="exp T"])
fix t a b :: real
assume tab:"exp T ≤ t" "t ≤ a" "a ≤ b"
hence tab0:"0 < t" "0 < a" "0 < b"
using exp_gt_zero[of T] by linarith+
hence lnab:"T ≤ ln a" "ln a ≤ ln b"
using tab ln_ge_iff by(auto intro!: ln_mono)
then obtain A B where AB:"0 < A" "(λx. L (exp x)) ` {ln a..ln b} ⊆ {A..B}"
using T by meson
moreover have "(λx. L (exp x)) ` {ln a..ln b} = L ` {a..b}"
unfolding h_def image_image[symmetric]
by(simp add: ** lnab tab0)
ultimately show "∃A>0. ∃B. L ` {a..b} ⊆ {A..B}"
by fast
qed
show "∀⇩F x in at_top. ∀a≥x. ∀b≥a. bounded (L ` {a..b})"
by(intro eventually_mono[OF ***])
(meson bounded_closed_interval bounded_subset)
qed
lemma
assumes rv:"regularly_varying U ρ"
defines "h ≡ λx. ln (U (exp x))"
shows regularly_varying_eventually_bounded_interval:
"∀⇩F x in at_top. ∀a≥x. ∀b. bounded (U ` {a..b})"
and regularly_varying_eventually_bounded_interval_strong:
"∀⇩F x in at_top. ∀a≥x. ∀b. ∃A>0. ∃B. U ` {a..b} ⊆ {A..B}"
and regularly_varying_eventually_bounded_interval_ln_exp:
"∀⇩F x in at_top. ∀a≥x. ∀b. bounded (h ` {a..b})"
and regularly_varying_eventually_locally_integrable:
"∀⇩F x in at_top. ∀a≥x. ∀b. set_integrable lborel {a..b} U"
and regularly_varying_eventually_locally_integrable_ln_exp:
"∀⇩F x in at_top. ∀a≥x. ∀b. set_integrable lborel {a..b} h"
proof -
define L where "L ≡ λx. U x / x powr ρ"
define h' where "h' ≡ λx. ln (L (exp x))"
have sv:"slowly_varying L"
by(simp add: regularly_varying_iff_slowly_varying_divide_powr[of U,symmetric] L_def rv)
have U_L:"⋀x. 0 < x ⟹ U x = x powr ρ * L x"
by(auto simp: L_def)
have h_h':"h = (λx. ρ * x + h' x)"
using regularly_varying_pos[OF sv exp_gt_zero]
by(auto simp add: h'_def h_def U_L ln_mult less_le)
hence 1:"∀⇩F x in at_top. ∀a≥x. ∀b≥a. bounded (L ` {a..b})"
and 2:"∀⇩F x in at_top. ∀a≥x. ∀b≥a. ∃A>0. ∃B. L ` {a..b} ⊆ {A..B}"
and 3:"∀⇩F x in at_top. ∀a≥x. ∀b≥a. bounded (h' ` {a..b})"
using slowly_varying_eventually_bounded_interval
slowly_varying_eventually_bounded_interval_strong
slowly_varying_eventually_bounded_interval_ln_exp sv
by(auto simp: h'_def)
have *:"∀⇩F x in at_top. ∀a≥x. ∀b. bounded (L ` {a..b})"
by(intro eventually_mono[OF 1])
(metis atLeastatMost_empty_iff2 bounded_closed_interval image_empty)
have **:"∀⇩F x in at_top. ∀a≥x. ∀b. ∃A>0. ∃B. L ` {a..b} ⊆ {A..B}"
by(intro eventually_mono[OF 2])
(metis atLeastatMost_empty' empty_iff exp_gt_zero image_subset_iff)
have ***:"∀⇩F x in at_top. ∀a≥x. ∀b. bounded (h' ` {a..b})"
by(intro eventually_mono[OF 3])
(metis atLeastatMost_empty_iff2 bounded_closed_interval image_empty)+
have bdd1:"∀⇩F x in at_top. ∀a≥x. ∀b. bounded ((λx. x powr ρ) ` {a..b})"
by(auto intro!: compact_imp_bounded compact_continuous_image continuous_on_powr
eventually_at_top_linorderI[where c=1])
have bdd2:"bounded ((λx. ρ * x) ` {a..b})" for a b
by (metis bounded_closed_interval bounded_scaling image_cong real_scaleR_def)
have U':"∀⇩F x in at_top. ∀a≥x. ∀b. bounded ((λx. x powr ρ * L x) ` {a..b})"
by(intro eventually_mono[OF eventually_conj[OF * bdd1]] bounded_times_comp allI impI)
auto
show g1:"∀⇩F x in at_top. ∀a≥x. ∀b. bounded (U ` {a..b})"
proof(intro eventually_at_top_linorderI[where c=1,THEN eventually_mp[OF _ U']] impI allI)
fix x a b :: real
assume h:"1 ≤ x" "∀a≥x. ∀b. bounded ((λx. x powr ρ * L x) ` {a..b})" "x ≤ a"
then have "(λx. x powr ρ * L x) ` {a..b} = U ` {a..b}"
using U_L by auto
thus "bounded (U ` {a..b})"
using h by metis
qed
show g2:"∀⇩F x in at_top. ∀a≥x. ∀b. bounded (h ` {a..b})"
using bdd2 by(auto simp: h_h' intro!: bounded_plus_comp eventually_mono[OF ***])
show "∀⇩F x in at_top. ∀a≥x. ∀b. set_integrable lborel {a..b} U"
proof(safe intro!: eventually_at_top_linorderI[where c=1,THEN eventually_mp[OF _ g1]])
fix a b x :: real
assume h:"1 ≤ x" "∀a≥x. ∀b. bounded (U ` {a..b})" "x ≤ a"
then obtain K where "∀x∈{a..b}. ¦U x¦ ≤ K"
by(fastforce simp: bounded_iff)
thus "set_integrable lborel {a..b} U"
using regularly_varying_meas_Icc[OF rv] h
by(auto simp: set_integrable_def emeasure_lborel_Icc_eq
intro!: integrableI_bounded_set[where A="{a..b}" and B=K])
qed
show "∀⇩F x in at_top. ∀a≥x. ∀b. set_integrable lborel {a..b} h"
proof(safe intro!: eventually_mono[OF g2])
fix a b x :: real
assume h:"∀a≥x. ∀b. bounded (h ` {a..b})" "x ≤ a"
then obtain K where "∀x∈{a..b}. ¦h x¦ ≤ K"
by(fastforce simp: bounded_iff)
thus "set_integrable lborel {a..b} h"
using regularly_varying_meas_log_exp[OF rv]
by(auto simp: set_integrable_def emeasure_lborel_Icc_eq h_def
intro!: integrableI_bounded_set[where A="{a..b}" and B=K])
qed
have ****:"∀⇩F x in at_top. ∀a≥x. ∀b≥a. ∃A>0. ∃B. U ` {a..b} ⊆ {A..B}"
proof(safe intro!: eventually_mp[OF eventually_at_top_linorderI[of 1] **])
fix x a b :: real
assume xab:"1 ≤ x" "x ≤ a" "a ≤ b" "∀a≥x. ∀b. ∃A>0. ∃B. L ` {a..b} ⊆ {A..B}"
then obtain A B where A:"A > 0" and AB:"L ` {a..b} ⊆ {A..B}"
by blast
have a:"0 < a"
using xab by linarith
have "∃C>0. ∃D. (λx. x powr ρ) ` {a..b} = {C..D}"
proof(cases "0 ≤ ρ")
assume "0 ≤ ρ"
then have "(λx. x powr ρ) ` {a..b} = {a powr ρ..b powr ρ}"
using xab
by(intro image_mono_on_continuous_on_Icc xab mono_onI
powr_mono2 continuous_on_powr) auto
thus ?thesis
using a
by(intro exI[where x="a powr ρ"] conjI[OF _ exI[where x="b powr ρ"]]) auto
next
assume "¬ 0 ≤ ρ"
then have "(λx. x powr ρ) ` {a..b} = {b powr ρ..a powr ρ}"
using xab
by(intro image_antimono_on_continuous_on_Icc monotone_onI powr_mono2'
continuous_on_powr) auto
thus ?thesis
using xab
by(intro exI[where x="b powr ρ"] conjI[OF _ exI[where x="a powr ρ"]]) auto
qed
then obtain C D where CD:"0 < C" "(λx. x powr ρ) ` {a..b} = {C..D}"
by blast
have "U ` {a..b} ⊆ (λ(x, y). x * y) ` ((λx. x powr ρ) ` {a..b} × L ` {a..b})"
using a U_L by auto
also have "... ⊆ (λ(x, y). x * y) ` ({C..D} × {A..B})"
using AB CD by fast
also have "... ⊆ {C*A..D*B}"
using A CD mult_mono by fastforce
finally show "∃A>0. ∃B. U ` {a..b} ⊆ {A..B}"
using A CD by(intro exI[where x="C*A"]) auto
qed
show "∀⇩F x in at_top. ∀a≥x. ∀b. ∃A>0. ∃B. U ` {a..b} ⊆ {A..B}"
by(rule eventually_mono[OF ****])
(metis atLeastatMost_empty_iff dual_order.refl empty_iff image_subset_iff)
qed
subsection ‹Weakening the Definition of Regularly Varying Functions ›
text ‹We prove Proposition 2.3 in \cite{Resnick}.
In the definition of a regularly varying function,
$U(tx)/U(t)$ needs to converge to $x^\rho$ as $t\to\infty$.
However, we can weaken this assumption to: $U(tx)/U(t)$
converges to some function $h$.›
lemma
assumes [measurable]:"U ∈ borel_measurable (restrict_space borel {0<..})"
and U:"⋀x. 0 < x ⟹ 0 < U x"
and lim:"⋀x. x > 0 ⟹ ((λt. U (t * x) / U t) ⤏ h x) at_top"
shows divide_limit_power:"⋀x. x > 0 ⟹ h x = x powr ln (h (exp 1))"
and divide_limit_imp_regularly_varying:"regularly_varying U (ln (h (exp 1)))"
and divide_limit_imp_regularly_varying_ex:"∃ρ. regularly_varying U ρ"
proof -
have lim':"0 < x ⟹ 0 < y ⟹
((λt. U (t * x * y) / U (t * x)) ⤏ h y) at_top" for x y
by(rule filterlim_compose[of _ _ at_top "λt. t * x"])
(auto intro!: lim eventually_at_top_linorderI[where c="_ / x"]
simp: divide_le_eq filterlim_at_top)
have cong:"⋀x y. 0 < x ⟹ 0 < y ⟹
∀⇩F t in at_top. U (t * (x * y)) / U t
= U (t * x) / U t * (U (t * x * y) / U (t * x))"
using U by(intro eventually_at_top_linorderI[where c=1])
(simp add: mult.assoc less_le)
have lim1:"⋀x y. 0 < x ⟹ 0 < y ⟹
((λt. U (t * (x * y)) / U t) ⤏ h (x * y)) at_top"
using lim by simp
have lim2:"⋀x y. 0 < x ⟹ 0 < y ⟹
((λt. U (t * x) / U t * (U (t * x * y) / U (t * x))) ⤏ h x * h y) at_top"
by(intro tendsto_mult lim lim') simp_all
have h_eq:"0 < x ⟹ 0 < y ⟹ h (x * y) = h x * h y" for x y
using lim1[of x y] lim2[of x y]
by(intro tendsto_unique) (auto simp: tendsto_cong[OF cong[of x y]])
have [measurable]:"(*) r ∈ restrict_space borel {0::real<..} →⇩M restrict_space borel {0<..}"
if r:"r > 0" for r
using r by(auto intro!: measurable_restrict_space3)
have h_meas[measurable]:"h ∈ borel_measurable (restrict_space borel {0<..})"
by(rule borel_measurable_LIMSEQ_metric_at_top[where f="λt x. U (t * x) / U t" and K=1])
(auto intro!: lim)
have h_pos:"0 < h x" if x:"0 < x" for x
proof(rule ccontr)
assume cc:"¬ 0 < h x"
moreover have "0 ≤ h x"
by(rule tendsto_lowerbound[OF lim[OF x]])
(use U in "auto intro!: eventually_at_top_linorderI[where c=1]
order.strict_implies_order simp: x")
ultimately have "h x = 0"
by linarith
hence "h 1 = 0"
using h_eq[of x "1 / x"] x by simp
hence "((λt. U t / U t) ⤏ 0) at_top"
using lim[of 1] by auto
moreover have "((λt. U t / U t) ⤏ 1) at_top"
by(intro tendstoI eventually_at_top_linorderI[where c=1])
(metis U dist_self divide_self less_irrefl order_less_le_trans zero_less_one)
ultimately show False
using tendsto_unique by force
qed
hence "h 1 = 1"
using h_eq[of 1 1] by (metis less_irrefl mult_cancel_right1 zero_less_one)
define g where "g ≡ λr. ln (h (exp r))"
have g_meas:"g ∈ borel_measurable borel"
unfolding g_def
by(rule measurable_compose[where N=borel,OF measurable_compose
[where g=h and N="restrict_space borel {0<..}"]])
(auto simp: measurable_restrict_space2_iff)
have g_eq:"g (x + y) = g x + g y" for x y
by(simp add: g_def exp_add h_eq[OF exp_gt_zero exp_gt_zero] ln_mult_pos[OF h_pos h_pos])
have "g = (λx. x * g 1)"
using g_meas g_eq Cauchy_equation_measurable' by blast
hence "x * g 1 = ln (h (exp x))" for x
by (metis g_def)
hence "x > 0 ⟹ ln x * g 1 = ln (h x)" for x
by simp
thus hx:"x > 0 ⟹ h x = x powr ln (h (exp 1))" for x
by (simp add: h_pos powr_def g_def mult.commute)
show "regularly_varying U (ln (h (exp 1)))"
using assms by(auto intro!: regularly_varyingI simp: hx[symmetric])
thus "∃ρ. regularly_varying U ρ"
by blast
qed
lemma
assumes mono:"mono_on {0<..} U" and U_pos: "⋀x. 0 < x ⟹ 0 < U x"
and b_pos:"∀⇩F n in sequentially. 0 < b n"
and l_pos:"∀⇩F n in sequentially. 0 < l n"
and lim_b:"filterlim b at_top sequentially"
and l_equiv:"l ∼[sequentially] (λn. l (Suc n))"
and lim:"⋀x. 0 < x ⟹ (λn. l n * U (b n * x)) ⇢ h x"
and h_pos: "⋀x. 0 < x ⟹ 0 < h x"
shows regularly_varying_sequentialy_lim:
"⋀x. 0 < x ⟹ ((λt. U (t * x) / U t) ⤏ h x / h 1) at_top"
and regularly_varying_sequentialy:"regularly_varying U (ln (h (exp 1) / h 1))"
and regularly_varying_sequentialy_ex:"∃ρ. regularly_varying U ρ"
proof -
have l_Spos:"∀⇩F n in sequentially. 0 < l (Suc n)"
using l_pos le_Suc_eq by(auto simp: eventually_sequentially)
have lim_l:"(λn. l n / l (Suc n)) ⇢ 1"
using l_pos eventually_mono
by(fastforce intro!: asymp_equivD_strong[OF l_equiv])
have lim_S:"⋀x. 0 < x ⟹ (λn. l (Suc n) * U (b (Suc n) * x)) ⇢ h x"
using lim by(auto intro!: LIMSEQ_Suc)
define n where "n ≡ (λt. LEAST m. t < b (m + 1))"
have n_less_b:"t < b (n t + 1)" for t
unfolding n_def
by(rule LeastI_ex)
(metis lim_b eventually_sequentially filterlim_at_top_dense nat_le_iff_add)
have b_le_n:"b (n t) ≤ t" if t:"b 0 ≤ t" for t
by(rule ccontr)
(metis Least_le Suc_n_not_le_n n_def not0_implies_Suc not_le Suc_eq_plus1 t)
have lim_n:"filterlim n sequentially at_top"
proof(rule ccontr)
assume "¬ filterlim n sequentially at_top"
then obtain M where M':"⋀T. ∃t≥T. n t + 1 ≤ M + 1"
unfolding filterlim_at_top eventually_at_top_linorder
by (meson add_right_mono linear)
define bM where "bM ≡ Max (b ` {..M + 1})"
have "⋀T. ∃t≥T. b (n t + 1) ≤ bM"
using M' unfolding bM_def
by (meson Max.coboundedI atMost_iff finite_atMost finite_imageI image_eqI)
then obtain t where "bM ≤ t" "b (n t + 1) ≤ bM"
by blast
thus False
using n_less_b[of t] by linarith
qed
have b_pos':"∀⇩F t in at_top. 0 < b (n t)"
and l_pos':"∀⇩F t in at_top. 0 < l (n t)"
and l_Spos':"∀⇩F t in at_top. 0 < l (Suc (n t))"
and lim_b':"filterlim (λt. b (n t)) at_top at_top"
and lim_l':"((λt. l (n t) / l (Suc (n t))) ⤏ 1) at_top"
and lim':"⋀x. 0 < x ⟹ ((λt. l (n t) * U (b (n t) * x)) ⤏ h x) at_top"
and lim_S':"⋀x. 0 < x ⟹ ((λt. l (Suc (n t)) * U (b (Suc (n t)) * x)) ⤏ h x) at_top"
by(auto intro!: b_pos l_pos lim_b lim_l eventually_compose_filterlim[OF _ lim_n]
filterlim_compose[OF _ lim_n] l_Spos lim lim_S)
show *:"((λt. U (t * x) / U t) ⤏ h x / h 1) at_top" if x:"0 < x" for x
proof(rule tendsto_sandwich)
show "∀⇩F t in at_top. (l (Suc (n t)) / l (n t))
* (l (n t) * U (b (n t) * x) / (l (Suc (n t)) * U (b (Suc (n t)))))
≤ U (t * x) / U t" (is "∀⇩F t in at_top. ?lhs t ≤ _")
proof(intro impI eventually_mp[OF eventually_at_top_linorderI[where c="max (b 0) 1"]
eventually_conj[OF b_pos' eventually_conj[OF l_pos' l_Spos']]])
fix t
assume t: "max (b 0) 1 ≤ t" and h:"0 < b (n t) ∧ 0 < l (n t) ∧ 0 < l (Suc (n t))"
have "?lhs t = U (b (n t) * x) / U (b (Suc (n t)))"
using h by simp
also have "... ≤ U (t * x) / U t"
by(rule frac_le)
(use U_pos x h t n_less_b[of t] mono_onD[OF mono] b_le_n[of t]
in "auto intro!: order.strict_implies_order[of 0]")
finally show "?lhs t ≤ U (t * x) / U t" .
qed
next
show "∀⇩F t in at_top. U (t * x) / U t
≤ (l (n t) / l (Suc (n t)))
* (l (Suc (n t)) * U (b (Suc (n t)) * x) / (l (n t) * U (b (n t))))
" (is "∀⇩F t in at_top. _ ≤ ?rhs t")
proof(intro impI eventually_mp[OF eventually_at_top_linorderI[where c="max (b 0) 1"]
eventually_conj[OF b_pos' eventually_conj[OF l_pos' l_Spos']]])
fix t
assume t: "max (b 0) 1 ≤ t" and h:"0 < b (n t) ∧ 0 < l (n t) ∧ 0 < l (Suc (n t))"
have "U (t * x) / U t ≤ U (b (Suc (n t)) * x) / U (b (n t))"
by(rule frac_le)
(use U_pos x h t n_less_b[of t] mono_onD[OF mono] b_le_n[of t]
in "auto intro!: order.strict_implies_order[of 0]")
also have "... ≤ ?rhs t"
using h by simp
finally show "U (t * x) / U t ≤ ?rhs t" .
qed
next
have 1:"((λt. l (Suc (n t)) / l (n t)) ⤏ 1) at_top"
using tendsto_divide[OF tendsto_const[of 1] lim_l'] by simp
have 2:"((λt. l (n t) * U (b (n t) * x)) ⤏ h x) at_top"
using x lim' by simp
have 3:"((λt. l (Suc (n t)) * U (b (Suc (n t)))) ⤏ h 1) at_top"
using lim_S'[of 1] by simp
show "((λt. l (Suc (n t)) / l (n t) *
(l (n t) * U (b (n t) * x) / (l (Suc (n t)) * U (b (Suc (n t))))))
⤏ h x / h 1) at_top"
using tendsto_mult[OF 1 tendsto_divide[OF 2 3]] h_pos[of 1] by argo
next
thm lim_l'
have 2:"((λt. l (Suc (n t)) * U (b (Suc (n t)) * x)) ⤏ h x) at_top"
using x lim_S' by simp
have 3:"((λt. l (n t) * U (b (n t))) ⤏ h 1) at_top"
using lim'[of 1] by simp
show "((λt. l (n t) / l (Suc (n t)) *
(l (Suc (n t)) * U (b (Suc (n t)) * x) / (l (n t) * U (b (n t)))))
⤏ h x / h 1) at_top"
using tendsto_mult[OF lim_l' tendsto_divide[OF 2 3]] h_pos[of 1] by argo
qed
show "regularly_varying U (ln (h (exp 1) / h 1))"
by(auto intro!: divide_limit_imp_regularly_varying
borel_measurable_mono_on_fnc mono U_pos *)
thus "∃ρ. regularly_varying U ρ"
by blast
qed
lemma regularly_varying_integral_infinity:
assumes rv:"regularly_varying U ρ"
assumes rho:"- 1 < ρ"
shows "(∫⇧+ t∈{a<..}. ennreal (U t) ∂lborel) = ⊤"
proof -
have [measurable]:"⋀n. (λx. ennreal (U x) * indicator {2^n<..2 * 2^n} x)
∈ borel_measurable borel"
"(λx. ennreal (U x) * indicator {0<..} x) ∈ borel_measurable borel"
by(auto intro!: regularly_varying_meas_Ioc_ennreal
regularly_varying_meas_o_ennreal rv)
have "2 powr ρ > 1 / 2"
by (metis rho powr_less_cancel_iff powr_neg_one rel_simps(49,51) semiring_norm(76))
with regularly_varying_lim[where x=2,OF rv]
obtain s' where s':"⋀t. s' ≤ t ⟹ 1 / 2 < U (t * 2) / U t"
by (metis (lifting) eventually_at_top_linorder rel_simps(51) order_tendstoD(1))
obtain s'' where s'': "⋀t k. s'' ≤ t ⟹ set_integrable lborel {t..k} U"
using regularly_varying_eventually_locally_integrable[OF rv]
by (metis (lifting) eventually_at_top_linorder)
define s where "s ≡ max (max 1 a) (max s' s'')"
have s_pos:"0 < s" and s:"⋀t. s ≤ t ⟹ U t < 2 * U (t * 2)"
and s2:"⋀t k. s ≤ t ⟹ set_integrable lborel {t..k} U"
using s' s'' regularly_varying_pos[OF rv] by(fastforce simp: s_def)+
have as:"a ≤ s"
by(simp add: s_def)
obtain N where N:"s ≤ 2 ^ N"
using power_of_nat_log_ge [of 2 s] by auto
hence N':"⋀n. N ≤ n ⟹ 2 ^ n ≤ t ⟹ U t < 2 * U (t * 2)" for t
using s[of t] s_pos order.trans less_num_simps
by (metis power_increasing power_one_right two_realpow_ge_one)
have integrable:"N ≤ n ⟹ set_integrable lborel {2^n<..2 * 2^n} U" for n
using s2[OF order.trans[OF N]]
by(auto intro!: set_integrable_subset[where A="{2^n..2 * 2^n}" and B="{2^n<..2 * 2^n}"])
have less':"(∫⇧+ t∈{2^n<..2 * 2^n}. U t ∂lborel) < (∫⇧+ t∈{2*2^n<..4 * 2^n}. U t ∂lborel)"
if n:"N ≤ n" for n
proof -
have "(∫⇧+ t∈{2^n<..2 * 2^n}. ennreal (U t) ∂lborel)
< (∫⇧+ t∈{2^n<..2 * 2^n}. ennreal (2 * U (t * 2)) ∂lborel)"
proof(rule set_nn_integral_less)
have "(∫⇧+x∈{2 ^ n<..2 * 2 ^ n}. ennreal (U x) ∂lborel)
≤ (∫⇧+x. ennreal ¦indicat_real {2 ^ n<..2 * 2 ^ n} x * U x¦ ∂lborel)"
by(auto intro!: nn_integral_mono arg_cong[where f=ennreal]
simp: ennreal_indicator[symmetric] ennreal_mult''[OF indicator_pos_le,symmetric]
mult.commute)
also have "... < ∞"
using integrable[OF n] by(auto simp: set_integrable_def integrable_iff_bounded)
finally show "(∫⇧+x∈{2 ^ n<..2 * 2 ^ n}. ennreal (U x) ∂lborel) ≠ ∞"
by order
next
show "AE x∈{2 ^ n<..2 * 2 ^ n} in lborel. ennreal (U x)
< ennreal (2 * U (x * 2)) "
by(fastforce intro!: ennreal_lessI N'[OF n] regularly_varying_pos[OF rv])
show "(λx. ennreal (2 * U (x * 2)) * indicator {2 ^ n<..2 * 2 ^ n} x)
∈ borel_measurable lborel"
by(auto intro!: regularly_varying_meas_Ioc_ennreal
regularly_varying_comp_multc regularly_varying_cmult rv)
qed auto
also have "... = (∫⇧+x∈{2 ^ n<..2 * 2 ^ n}. ennreal (¦2¦ * U (x * 2)) ∂lborel)"
by simp
also have "... = (∫⇧+x∈(λx. x * 2) ` {2 ^ n<..2 * 2 ^ n}. ennreal (U x) ∂lborel)"
by(rule nn_integral_change_of_variables_real1'[symmetric])
(use integrable[of "n + 1"] n in
"auto intro!: measurable_restrict_space1 inj_on_mult less_imp_le
regularly_varying_pos[OF rv] simp: mult_commute_abs")
also have "... = (∫⇧+ t∈{2*2^n<..4 * 2^n}. U t ∂lborel)"
by simp
finally show ?thesis .
qed
have less:"(∫⇧+ t∈{2^N<..2 * 2^N}. U t ∂lborel) < (∫⇧+ t∈{2*2^n<..4 * 2^n}. U t ∂lborel)"
if n:"N ≤ n" for n
proof(rule nat_induct_at_least[OF n])
fix m
assume m:"N ≤ m"
and "(∫⇧+x∈{2 ^ N<..2 * 2 ^ N}. ennreal (U x) ∂lborel)
< (∫⇧+x∈{2 * 2 ^ m<..4 * 2 ^ m}. ennreal (U x) ∂lborel)"
hence "(∫⇧+x∈{2 ^ N<..2 * 2 ^ N}. ennreal (U x) ∂lborel)
< (∫⇧+x∈{2 * 2 ^ m<..4 * 2 ^ m}. ennreal (U x) ∂lborel)"
by simp
also have "... = (∫⇧+x∈{2 ^ Suc m<..2 * 2 ^ Suc m}. ennreal (U x) ∂lborel)"
by simp
also have "... < (∫⇧+x∈{2 * 2 ^ Suc m<..4 * 2 ^ Suc m}. ennreal (U x) ∂lborel)"
by(intro less') (use m in auto)
finally show "(∫⇧+x∈{2 ^ N<..2 * 2 ^ N}. ennreal (U x) ∂lborel)
< (∫⇧+x∈{2 * 2 ^ Suc m<..4 * 2 ^ Suc m}. ennreal (U x) ∂lborel)" .
qed(use less' in auto)
have disj:"disjoint_family (λn. {2 * 2 ^ (n + N) <..4 * 2 ^ (n + N)::real})"
unfolding disjoint_family_on_def
proof safe
fix m n x
assume mn:"m ≠ n"
and x:"x ∈ {2 * 2 ^ (m + N)<..4 * 2 ^ (m + N)::real}"
"x ∈ {2 * 2 ^ (n + N)<..4 * 2 ^ (n + N)}"
have 1:"m < n ⟹ (2 :: real) ^ (m + 1 + (N + 1)) ≤ 2 ^ (n + N + 1)"
by(intro power_increasing) (auto simp: less_eq_Suc_le)
have 2:"n < m ⟹ (2 :: real) ^ (n + 1 + (N + 1)) ≤ 2 ^ (m + N + 1)"
by(intro power_increasing) (auto simp: less_eq_Suc_le)
consider "m < n" | "n < m"
using mn by linarith
thus "x ∈ {}"
by cases (use 1 2 x in auto)
qed
have subst:"(⋃m. {2*2^(m + N)<..4 * 2^(m + N)}) ⊆ {a<..}"
proof safe
fix x m
assume x: "x ∈ {2 * 2 ^ (m + N)<..4 * 2 ^ (m + N) :: real}"
have "(2 :: real) ^ N ≤ 2 * 2 ^ (m + N)"
by(auto simp del: power_Suc simp: power_Suc[symmetric])
thus "a < x"
using as N x by simp
qed
have "⊤ = (∑m. (∫⇧+ t∈{2 ^ N<..2 * 2 ^ N}. ennreal (U t) ∂lborel))"
by(intro suminf_const_infinity[symmetric] set_nn_integral_zero_less AE_I2)
(use regularly_varying_pos[OF rv] in auto)
also have "... ≤ (∑m. (∫⇧+ t∈{2*2^(m + N)<..4 * 2^(m + N)}. U t ∂lborel))"
by(auto intro!: suminf_le less_imp_le[OF less])
also have "... =
(∑m. (∫⇧+ t∈{2*2^(m + N)<..4 * 2^(m + N)}. ennreal (U t) * indicator {0<..} t ∂lborel))"
by(auto intro!: suminf_cong nn_integral_cong ennreal_mult_right_cong
simp: indicator_eq_0_iff)
also have "... =
(∫⇧+ t∈⋃m. {2*2^(m + N)<..4 * 2^(m + N)}. ennreal (U t) * indicator {0<..} t ∂lborel)"
by(rule nn_integral_disjoint_family[symmetric]) (auto simp: disj)
also have "... ≤ (∫⇧+t∈{a<..}. ennreal (U t) ∂lborel)"
using subst by(intro nn_integral_mono) (fastforce simp: indicator_def)
finally show ?thesis
using neq_top_trans by blast
qed
subsection ‹Karamata's Representation Theorem›
text ‹Lemma 1.3.1 in \cite{BGT}.›
lemma Karamata_representation_ln_exp_slowly_varying:
fixes L
defines "h ≡ (λx. ln (L (exp x)))"
assumes sv:"slowly_varying L"
and A: "0 < A"
and bdd:"⋀a b. A ≤ a ⟹ ∃X>0. ∃Y. L ` {a..b} ⊆ {X..Y}"
shows "∃c e C.
(∀x ≥ ln A. h x = c x + (∫u∈{ln A<..x}. e u ∂lborel))
∧ (∀x ≥ ln A. set_integrable lborel {ln A<..x} e)
∧ e ∈ borel_measurable borel
∧ (e ⤏ 0) at_top
∧ bounded (e ` {ln A..})
∧ c ∈ borel_measurable borel
∧ (c ⤏ C) at_top"
proof -
have [measurable]:"h ∈ borel_measurable borel"
using regularly_varying_meas_log_exp sv by(simp add: h_def)
have bddh:"bounded (h ` {a..b})" if a:"ln A ≤ a" for a b
proof(cases "a ≤ b")
assume b:"a ≤ b"
then obtain A' B where A': "A ≤ A'" "a = ln A'" and B:"A' ≤ B" "b = ln B"
by (metis a exp_gt_zero landau_omega.R_trans ln_exp ln_mono nle_le)
hence A'_pos:"0 < A'" and B_pos:"0 < B"
using A by auto
obtain X Y where XY:"X > 0" "X ≤ Y" "L ` {A'..B} ⊆ {X..Y}"
using bdd A' B by (meson A'_pos atLeastatMost_subset_iff order.trans)
have "exp ` {a..b} = {A'..B}"
unfolding A' B
by(subst image_mono_on_continuous_on_Icc)
(use A' B A'_pos B_pos in
"auto intro!: mono_on_subset[OF Multiseries_Expansion_Bounds.mono_exp_real]
continuous_on_exp")
hence "h ` {a..b} = (λx. ln (L x)) ` {A'..B}"
by (metis (no_types, lifting) ext h_def image_image)
also have "... = ln ` (L ` {A'..B})"
by blast
also have "... ⊆ ln ` {X..Y}"
using XY by blast
also have "... = {ln X..ln Y}"
using XY
by(intro image_mono_on_continuous_on_Icc XY continuous_on_ln mono_onI ln_mono)
auto
finally show ?thesis
by (metis bounded_closed_interval bounded_subset)
qed simp
have integrableh:"set_integrable lborel {a<..b} h" if a:"ln A ≤ a" for a b
unfolding set_integrable_def
proof(safe intro!: integrableI_bounded)
obtain K where K:"⋀x. a ≤ x ⟹ x ≤ b ⟹ ¦h x¦ ≤ K"
using bddh[OF a] by (metis atLeastAtMost_iff bounded_real image_eqI)
have "(∫⇧+ x. ennreal (norm (indicat_real {a<..b} x *⇩R h x)) ∂lborel)
= (∫⇧+ x∈{a<..b}. ennreal ¦h x¦ ∂lborel)"
by(auto intro!: nn_integral_cong simp: indicator_times_eq_if)
also have "... ≤ (∫⇧+ x∈{a..b}. ennreal K ∂lborel)"
using K by(auto intro!: nn_integral_mono simp: indicator_def ennreal_leI)
also have "... = ennreal K * (∫⇧+ x. indicator {a..b} x ∂lborel)"
by(subst nn_integral_cmult) simp_all
also have "... < ∞"
by (simp add: emeasure_lborel_Icc_eq ennreal_mult_less_top)
finally show "(∫⇧+ x. ennreal (norm (indicat_real {a<..b} x *⇩R h x)) ∂lborel) < ∞" .
qed simp
define C where "C ≡ (∫t∈{ln A<..ln A + 1}. h t ∂lborel)"
define c where "c ≡ (λx. C + (∫t∈{x<..x+ 1}. h x - h t ∂lborel))"
define e where "e ≡ (λx. h (x + 1) - h x)"
have integrableh':"set_integrable lborel {ln A<..x} (λt. h (t + 1))" for x
proof -
have "(λt. indicat_real {ln A + 1<..x + 1} (1 + t) * h (1 + t))
= (λt. indicat_real {ln A<..x} t * h (t + 1))"
by standard (auto simp: indicator_def add.commute)
thus ?thesis
using integrableh[of "ln A + 1" "x + 1"]
by(auto simp:
lborel_integrable_real_affine_iff[symmetric,
where f="λt. indicat_real {ln A+1<..x+1} t * h t" and t=1 and c=1]
set_integrable_def)
qed
have *:"∀x ≥ ln A. h x = c x + (∫u∈{ln A<..x}. e u ∂lborel)"
proof safe
fix x
assume x:"ln A ≤ x"
have "h x = h x + (∫t∈{ln A<..ln A + 1} ∪ {ln A + 1<.. x+ 1}. h t ∂lborel)
- (∫t∈{ln A<..x} ∪ {x<..x+ 1}. h t ∂lborel)"
using x by(auto intro!: arg_cong[where f="λA. set_lebesgue_integral lborel A h"])
also have "... = h x + (∫t∈{ln A<..ln A + 1}. h t ∂lborel)
+ (∫t∈{ln A + 1<.. x+ 1}. h t ∂lborel)
- (∫t∈{ln A<..x} ∪ {x<..x+ 1}. h t ∂lborel)"
by(subst set_integral_Un) (auto intro!: integrableh)
also have "... = h x + (∫t∈{ln A<..ln A + 1}. h t ∂lborel)
+ (∫t∈{ln A + 1<.. x+ 1}. h t ∂lborel)
- ((∫t∈{ln A<..x}. h t ∂lborel)
+ (∫t∈{x<..x+ 1}. h t ∂lborel))"
by(subst set_integral_Un) (auto intro!: integrableh x)
also have "... = h x + (∫t∈{ln A<..ln A + 1}. h t ∂lborel)
+ (∫t∈{ln A<.. x}. h (t + 1) ∂lborel)
- ((∫t∈{ln A<..x}. h t ∂lborel)
+ (∫t∈{x<..x+ 1}. h t ∂lborel))"
unfolding set_lebesgue_integral_def real_scaleR_def
by(subst lborel_integral_real_affine
[where f="λt. indicat_real {ln A+1<..x+1} t * h t" and t=1 and c=1])
(auto intro!: Bochner_Integration.integral_cong simp: indicator_def add.commute)
also have "... = C + (h x + (∫t∈{x<..x+ 1}. - h t ∂lborel))
+ ((∫t∈{ln A<.. x}. h (t + 1) ∂lborel)
+ (∫t∈{ln A<..x}. - h t ∂lborel))"
by(simp add: set_integral_uminus[OF integrableh] x C_def)
also have "... = C + ((∫t∈{x<..x+ 1}. h x ∂lborel) + (∫t∈{x<..x+ 1}. - h t ∂lborel))
+ ((∫t∈{ln A<.. x}. h (t + 1) ∂lborel)
+ (∫t∈{ln A<..x}. - h t ∂lborel))"
by(auto simp: set_lebesgue_integral_def)
also have "... = C + ((∫t∈{x<..x+ 1}. h x + (- h t) ∂lborel))
+ ((∫t∈{ln A<.. x}. h (t + 1) ∂lborel)
+ (∫t∈{ln A<..x}. - h t ∂lborel))"
by(subst set_integral_add)
(auto intro!: integrableh x set_integrable_const simp: set_integrable_uminus)
also have "... = c x + ((∫t∈{ln A<.. x}. h (t + 1) + (- h t) ∂lborel))"
by(subst set_integral_add[where f="λt. h (t + 1)"])
(auto intro!: integrableh x integrableh' simp: set_integrable_uminus c_def)
finally show "h x = c x + (∫u∈{ln A<..x}. e u ∂lborel)"
by(simp add: e_def)
qed
have **:"∀x≥ln A. set_integrable lborel {ln A<..x} e"
by(auto simp: e_def intro!: integrableh' integrableh)
have *****:"e ∈ borel_measurable borel"
by(simp add: e_def)
have ***:"(e ⤏ 0) at_top"
using slowly_varying_ln_exp[OF sv] by(simp add: e_def h_def)
have ******:"bounded (e ` {ln A..})"
proof -
obtain X where X:"⋀x. X < x ⟹ ¦e x¦ < 1"
using tendstoD[OF ***,of 1] unfolding eventually_at_top_dense
by auto
have 1:"bounded (e ` {ln A..X})"
unfolding e_def
by(intro bounded_minus_comp bounded_subset[where T="h ` {ln A..X}" and S="h ` {ln A<..X}"]
bounded_subset[where T="(λx. h (x + 1)) ` {ln A..X}"
and S="(λx. h (x + 1)) ` {ln A<..X}"])
(auto simp: image_image[symmetric,where g="λx. x + 1"] intro!: bddh)
have 2:"bounded (e ` {X<..})"
using X by(fastforce intro!: boundedI[where B=2])
show ?thesis
by(rule bounded_subset[where T="e ` {ln A..X} ∪ e ` {X<..}"])
(use 1 2 in fastforce)+
qed
have ****:"c ∈ borel_measurable borel"
proof -
have "Measurable.pred (borel ⨂⇩M borel) (λx::real × real. snd x ∈ {fst x<..fst x + 1})"
by simp
thus ?thesis
unfolding c_def set_lebesgue_integral_def
by measurable
qed
have "(c ⤏ C) at_top"
proof -
have "∀⇩F x in at_top. (∫t∈{x<..x+ 1}. h x - h t ∂lborel)
= (∫t∈{0<..1}. h x - h (x + t) ∂lborel)"
proof(safe intro!: eventually_at_top_linorderI[where c="ln A"])
fix x
assume x:"ln A ≤ x"
thus "(∫t∈{x<..x+ 1}. h x - h t ∂lborel) = (∫t∈{0<..1}. h x - h (x + t) ∂lborel)"
unfolding set_lebesgue_integral_def
by(subst lborel_integral_real_affine[where c=1 and t=x])
(auto intro!: Bochner_Integration.integral_cong simp: indicator_def)
qed
moreover have "((λx. (∫t∈{0<..1}. h x - h (x + t) ∂lborel)) ⤏ 0) at_top"
proof(rule tendstoI)
fix e :: real
assume e:"0 < e"
define e' where "e' ≡ e / 2"
have e':"0 < e'"
using e by(simp add: e'_def)
obtain X where X:"⋀x t. X ≤ x ⟹ 0 ≤ t ⟹ t ≤ 1 ⟹ ¦h x - h (x + t)¦ < e'"
using uniform_limitD[OF slowly_varying_UCT_interval_ln_exp[OF sv,of 0 1] e']
by(fastforce simp: h_def dist_real_def eventually_at_top_linorder abs_minus_commute)
show "∀⇩F x in at_top. dist (∫t∈{0<..1}. h x - h (x + t) ∂lborel) 0 < e"
proof(safe intro!: eventually_at_top_linorderI[where c=X])
fix x
assume x:"X ≤ x"
then have [simp]:"set_integrable lborel {0<..1} (λt. ¦h x - h (x + t)¦)"
using less_imp_le[OF X]
by(auto intro!: integrableI_bounded_set[where A="{0<..1}" and B=e']
simp: set_integrable_def)
have "dist (∫t∈{0<..1}. h x - h (x + t) ∂lborel) 0
≤ (∫t∈{0<..1}. ¦h x - h (x + t)¦ ∂lborel)"
by(auto simp: set_lebesgue_integral_def abs_mult_pos')
also have "... ≤ (∫t∈{0::real<..1}. e' ∂lborel)"
by(auto intro!: set_integral_mono less_imp_le[OF X] x integrableh set_integrable_const)
also have "... < e"
by(simp add: set_lebesgue_integral_def e'_def e)
finally show "dist (∫t∈{0<..1}. h x - h (x + t) ∂lborel) 0 < e" .
qed
qed
ultimately have "((λx. (∫t∈{x<..x+ 1}. h x - h t ∂lborel)) ⤏ 0) at_top"
by(simp cong: tendsto_cong)
thus ?thesis
by (metis (lifting) ext c_def group_cancel.rule0 tendsto_add_const_iff)
qed
thus ?thesis
using * ** *** **** ***** ****** by blast
qed
lemma Karamata_representation_ln_exp2:
fixes U
defines "h ≡ (λx. ln (U (exp x)))"
assumes rv:"regularly_varying U ρ"
and A: "0 < A"
and bdd:"⋀a b. A ≤ a ⟹ ∃X>0. ∃Y. U ` {a..b} ⊆ {X..Y}"
shows "∃c e C.
(∀x ≥ ln A. h x = c x + ρ * ln A + (∫u∈{ln A<..x}. ρ + e u ∂lborel))
∧ (∀x ≥ ln A. set_integrable lborel {ln A<..x} e)
∧ e ∈ borel_measurable borel
∧ (e ⤏ 0) at_top
∧ bounded (e ` {ln A..})
∧ c ∈ borel_measurable borel
∧ (c ⤏ C) at_top"
proof -
define L where "L ≡ λx. U x / x powr ρ"
define h' where "h' ≡ λx. ln (L (exp x))"
have sv:"slowly_varying L"
by(simp add: regularly_varying_iff_slowly_varying_divide_powr[of U,symmetric] L_def rv)
have U_L:"⋀x. 0 < x ⟹ U x = x powr ρ * L x"
by(auto simp: L_def)
have h_h':"h = (λx. ρ * x + h' x)"
using regularly_varying_pos[OF sv exp_gt_zero]
by(auto simp add: h'_def h_def U_L ln_mult less_le)
have "∃X>0. ∃Y. L ` {a..b} ⊆ {X..Y}" if Aa:"A ≤ a" for a b
proof -
obtain X' Y' where X'_pos:"X' > 0"
and X': "⋀x. a ≤ x ⟹ x ≤ b ⟹ X' ≤ U x"
and Y':"⋀x. a ≤ x ⟹ x ≤ b ⟹ U x ≤ Y'"
using bdd[OF Aa,of b] by fastforce
consider "ρ ≤ 0" "a ≤ b" | "0 ≤ ρ" "a ≤ b" | "b < a"
by linarith
thus ?thesis
proof cases
assume h: "ρ ≤ 0" "a ≤ b"
have "X' / a powr ρ ≤ U x / x powr ρ"
and "U x / x powr ρ ≤ Y' / b powr ρ" if "a ≤ x" "x ≤ b" for x
using X'[OF that] Y'[OF that] Aa A X'_pos h that
by(auto intro!: frac_le powr_mono2')
thus ?thesis
using X'_pos h Aa A
by(intro exI[where x="X' / a powr ρ",OF conjI[OF _ exI[where x="Y' / b powr ρ"]]])
(auto simp: L_def)
next
assume h: "ρ ≥ 0" "a ≤ b"
have "X' / b powr ρ ≤ U x / x powr ρ"
and "U x / x powr ρ ≤ Y' / a powr ρ" if "a ≤ x" "x ≤ b" for x
using X'[OF that] Y'[OF that] Aa A X'_pos h that
by(auto intro!: frac_le powr_mono2)
thus ?thesis
using X'_pos h Aa A
by(intro exI[where x="X' / b powr ρ",OF conjI[OF _ exI[where x="Y' / a powr ρ"]]])
(auto simp: L_def)
qed (auto intro!: exI[where x=1])
qed
from Karamata_representation_ln_exp_slowly_varying[OF sv A this]
obtain c e C where
h'_eq:"⋀x. ln A ≤ x ⟹ h' x = c x + (∫u∈{ln A<..x}. e u ∂lborel)"
and e_integrable:"⋀x. ln A ≤ x ⟹ set_integrable lborel {ln A<..x} e"
and e_meas[measurable]:"e ∈ borel_measurable borel"
and e_lim:"(e ⤏ 0) at_top"
and e_bdd:"bounded (e ` {ln A..})"
and c_meas[measurable]:"c ∈ borel_measurable borel"
and c_lim:"(c ⤏ C) at_top"
by(auto simp: h'_def)
have h_eq:"h x = c x + ρ * ln A + (∫u∈{ln A<..x}. ρ + e u ∂lborel)" if x:"ln A ≤ x" for x
proof -
have "h x = h' x + ρ * x"
by(simp add: h_h')
also have "... = c x + (∫u∈{ln A<..x}. e u ∂lborel) + ρ * x"
by(simp add: x h'_eq)
also have "... = c x + (∫u∈{ln A<..x}. ρ ∂lborel) + (∫u∈{ln A<..x}. e u ∂lborel) + ρ * ln A"
by(simp add: interval_integral_Ioc[OF x,symmetric] right_diff_distrib')
also have "... = c x + ρ * ln A + (∫u∈{ln A<..x}. ρ + e u ∂lborel)"
by (rule sym) (auto intro!: e_integrable set_integrable_const simp: x)
finally show ?thesis .
qed
thus ?thesis
using e_integrable e_lim c_lim c_meas e_meas e_bdd by blast
qed
lemma Karamata_representation_ln_exp:
fixes U
defines "h ≡ (λx. ln (U (exp x)))"
assumes rv:"regularly_varying U ρ"
shows "∃A>0. ∃c e C.
(∀x ≥ ln A. h x = c x + ρ * ln A + (∫u∈{ln A<..x}. ρ + e u ∂lborel))
∧ (∀x ≥ ln A. set_integrable lborel {ln A<..x} e)
∧ e ∈ borel_measurable borel
∧ (e ⤏ 0) at_top
∧ bounded (e ` {ln A..})
∧ c ∈ borel_measurable borel
∧ (c ⤏ C) at_top"
proof -
obtain A where "0 < A" "⋀a b. A ≤ a ⟹ ∃X>0. ∃Y. U ` {a..b} ⊆ {X..Y}"
using regularly_varying_eventually_bounded_interval_strong[OF rv]
unfolding eventually_at_top_linorder
by (meson exp_gt_self exp_gt_zero less_eq_real_def)
from Karamata_representation_ln_exp2[OF rv this] this
show ?thesis
unfolding h_def by blast
qed
text ‹This equation for @{term ln} is useful for transforming equations in proofs.›
lemma Karamata_representation_ex1:
assumes rv:"regularly_varying U ρ"
and A:"0 < A"
and bdd:"⋀a b. A ≤ a ⟹ ∃X>0. ∃Y. U ` {a..b} ⊆ {X..Y}"
shows "∃c r C.
(∀x ≥ A. U x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel))
∧ (∀x ≥ A. set_integrable lborel {A<..x} (λt. r t / t))
∧ r ∈ borel_measurable borel
∧ (r ⤏ ρ) at_top
∧ bounded (r ` {A..})
∧ c ∈ borel_measurable borel
∧ (∀x. 0 < c x)
∧ (c ⤏ C) at_top
∧ 0 < C"
proof -
define h where "h ≡ λx. ln (U (exp x))"
from Karamata_representation_ln_exp2[OF assms]
obtain c' e C' where
h_eq:"⋀x. ln A ≤ x ⟹ h x = c' x + ρ * ln A + (∫u∈{ln A<..x}. ρ + e u ∂lborel)"
and e_integrable:"⋀x. ln A ≤ x ⟹ set_integrable lborel {ln A<..x} e"
and e_meas[measurable]:"e ∈ borel_measurable borel"
and e_lim:"(e ⤏ 0) at_top"
and e_bdd:"bounded (e ` {ln A..})"
and c_meas[measurable]:"c' ∈ borel_measurable borel"
and c_lim:"(c' ⤏ C') at_top"
unfolding h_def by blast
define C where "C ≡ exp C' * (A powr ρ)"
define c where "c ≡ λx. exp (c' (ln x)) * A powr ρ"
define r where "r ≡ λx. ρ + e (ln x)"
have im_ln:"A ≤ x ⟹ ln ` {A<..x} = {ln A<..ln x}" for x
using A
by(intro image_mono_on_continuous_on_Ioc continuous_on_ln strict_mono_onI ln_strict_mono)
auto
have im_ln2:"ln ` {A..} = {ln A..}"
using A
by(intro image_mono_on_continuous_on_Ic continuous_on_ln mono_onI ln_mono ln_at_top)
auto
have *:"∀x ≥ A. set_integrable lborel {A<..x} (λt. r t / t)
∧ U x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel)"
proof safe
fix x
assume x:"A ≤ x"
have [simp]:"set_integrable lborel ({ln A<..ln x}) e"
unfolding im_ln[OF x]
by(auto intro!: e_integrable ln_mono x A)
have 1:"set_integrable lborel {A<..x} (λx. ¦1 / x¦ * e (ln x))"
using A x
by(intro lebesgue_integrable_change_of_variables_real
[where g'="λx. 1 / x" and f=e,THEN iffD1]
strict_mono_on_imp_inj_on)
(auto simp: set_borel_measurable_def im_ln[OF x] DERIV_ln_divide
has_field_derivative_at_within
intro!: measurable_restrict_space1 strict_mono_onI ln_strict_mono)
have integ1:"set_integrable lborel {A<..x} (λt. e (ln t) / t)"
by(rule set_integrable_cong[THEN iffD1,OF _ _ _ 1]) (use A in auto)
have integ2:"set_integrable lborel {A<..x} (λt. ρ / t)"
unfolding set_integrable_def
using x A by(auto intro!: integrableI_bounded_set[where A="{A<..x}" and B="¦ρ¦ / A"]
simp: divide_mono)
show "set_integrable lborel {A<..x} (λt. r t / t)"
by(auto simp: r_def add_divide_distrib integ1 integ2)
have "(∫u∈{ln A<..ln x}. ρ + e u ∂lborel) = (∫u∈ln ` {A<..x}. ρ + e u ∂lborel)"
by(simp add: im_ln x)
also have "... = (∫x∈{A<..x}. ¦1 / x¦ * (ρ + e (ln x)) ∂lborel)"
using A x
by(intro lebesgue_integral_change_of_variables_real1
[where g'="λx. 1 / x" and f="λx. ρ + e x"] strict_mono_on_imp_inj_on)
(auto simp: set_borel_measurable_def im_ln[OF x] DERIV_ln_divide
has_field_derivative_at_within
intro!: set_integrable_const measurable_restrict_space1 strict_mono_onI ln_strict_mono)
finally have eq:"(∫u∈{ln A<..ln x}. ρ + e u ∂lborel) = (∫t∈{A<..x}. r t / t ∂lborel)"
using A by(auto simp: r_def intro!: set_lebesgue_integral_cong)
have "U x = exp (h (ln x))"
using A x regularly_varying_pos[OF rv] by(simp add: h_def)
also have "... = exp (c' (ln x) + ρ * ln A + (∫u∈{ln A<..ln x}. ρ + e u ∂lborel))"
using A x by(simp add: h_eq)
also have "... = c x * exp (∫u∈{ln A<..ln x}. ρ + e u ∂lborel)"
using A by(simp add: c_def exp_add ln_powr[symmetric] del: ln_powr)
also have "... = c x * exp (∫t∈{A<..x}. r t / t ∂lborel)"
by(simp add: eq)
finally show "U x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel)" .
qed
have **:"r ∈ borel_measurable borel"
by(simp add: r_def)
have ***:"(r ⤏ ρ) at_top"
unfolding r_def
by(rule filterlim_compose[OF _ ln_at_top])
(use tendsto_add[OF tendsto_const e_lim] in simp)
have ****:"bounded (r ` {A..})"
unfolding r_def image_image[symmetric,where g=ln and f="λx. ρ + e x"] im_ln2
by(auto intro!: bounded_plus_comp[OF boundedI e_bdd])
have *****:"c ∈ borel_measurable borel"
by (simp add: c_def)
have ******:"∀x. 0 < c x"
using A by(simp add: c_def)
have cC:"(c ⤏ C) at_top"
unfolding c_def C_def
by(rule filterlim_compose[OF _ ln_at_top])
(auto intro!: tendsto_mult_right tendsto_exp c_lim)
have C:"0 < C"
using A by(simp add: C_def)
show ?thesis
using * ** *** **** ***** ****** C cC by blast
qed
lemma Karamata_representation_ex:
assumes rv:"regularly_varying U ρ"
shows "∃A>0. ∃c r C.
(∀x ≥ A. U x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel))
∧ (∀x ≥ A. set_integrable lborel {A<..x} (λt. r t / t))
∧ r ∈ borel_measurable borel
∧ (r ⤏ ρ) at_top
∧ bounded (r ` {A..})
∧ c ∈ borel_measurable borel
∧ (∀x. 0 < c x)
∧ (c ⤏ C) at_top
∧ 0 < C"
proof -
obtain A where "0 < A" "⋀a b. A ≤ a ⟹ ∃X>0. ∃Y. U ` {a..b} ⊆ {X..Y}"
using regularly_varying_eventually_bounded_interval_strong[OF rv]
unfolding eventually_at_top_linorder
by (meson exp_gt_self exp_gt_zero less_eq_real_def)
from Karamata_representation_ex1[OF rv this] this
show ?thesis
by blast
qed
corollary Karamata_representation_ex_total:
assumes rv:"regularly_varying U ρ"
shows "∃c r C.
(∀x. U x = c x * exp (∫t∈{0<..x}. r t / t ∂lborel))
∧ (∀x y. set_integrable lborel {..y} (λt. r t / t))
∧ r ∈ borel_measurable borel
∧ (r ⤏ ρ) at_top
∧ bounded (range r)
∧ c ∈ borel_measurable (restrict_space borel {0<..})
∧ (∀x>0. 0 < c x)
∧ (c ⤏ C) at_top
∧ 0 < C"
proof -
from Karamata_representation_ex[OF rv]
obtain A c' r' C where A_pos:"0 < A"
and eq': "⋀x. A ≤ x ⟹ U x = c' x * exp (∫t∈{A<..x}. r' t / t ∂lborel)"
and integ':"⋀x. A ≤ x ⟹ set_integrable lborel {A<..x} (λt. r' t / t)"
and r'[measurable]:"r' ∈ borel_measurable borel"
and lim_r':"(r' ⤏ ρ) at_top"
and bdd:"bounded (r' ` {A..})"
and c'[measurable]:"c' ∈ borel_measurable borel"
and c'_pos:"⋀x. 0 < c' x"
and lim_c':"(c' ⤏ C) at_top"
and C_pos:"0 < C"
by blast
define c where "c ≡ λx. if A < x then c' x else U x"
define r where "r ≡ λx. if A < x then r' x else 0"
have r_integral:"(∫t∈{0<..x}. r t / t ∂lborel) = 0" if Ax:"x ≤ A" for x
proof -
have "(∫t∈{0<..x}. r t / t ∂lborel) = (∫t∈{0<..x}. 0 ∂lborel)"
unfolding set_lebesgue_integral_def using Ax
by(intro Bochner_Integration.integral_cong)
(auto simp: r_def indicator_def)
thus ?thesis
by simp
qed
have r_integrable1:"x ≤ A ⟹ set_integrable lborel {..x} (λt. r t / t)" for x
by(subst set_integrable_cong[where f'="λx. 0",OF refl refl])
(auto simp: r_def)
hence r_integrable1'[simp]:"x ≤ A ⟹ set_integrable lborel {0<..x} (λt. r t / t)" for x
using set_integrable_subset[where A="{..x}" and B="{0<..x}"]
by fastforce
have r_integrabl2[simp]: "A ≤ x ⟹ set_integrable lborel {A<..x} (λt. r t / t)" for x
by(subst set_integrable_cong[where f'="λt. r' t / t",OF refl refl])
(auto simp: r_def integ')
have 1:"U x = c x * exp (∫t∈{0<..x}. r t / t ∂lborel)" for x
proof(cases "A ≤ x")
assume Ax:"A ≤ x"
have "(∫t∈{0<..x}. r t / t ∂lborel) = (∫t∈{0<..A}∪{A<..x}. r t / t ∂lborel)"
using Ax A_pos by(intro arg_cong[where f="λB. (∫t∈B. r t / t ∂lborel)"]) auto
also have "... = (∫t∈{0<..A}. r t / t ∂lborel) + (∫t∈{A<..x}. r t / t ∂lborel)"
by(subst set_integral_Un) (auto simp: Ax)
also have "... = (∫t∈{A<..x}. r t / t ∂lborel)"
by(simp add: r_integral)
also have "... = (∫t∈{A<..x}. r' t / t ∂lborel)"
by(auto intro!: Bochner_Integration.integral_cong simp: set_lebesgue_integral_def r_def)
finally show ?thesis
using Ax by(simp add: c_def eq')
qed(auto simp: c_def r_integral)
have 2:"set_integrable lborel {..x} (λt. r t / t)" for x
proof -
consider "A ≤ x" | "x ≤ A"
by fastforce
then show ?thesis
proof cases
assume Ax:"A ≤ x"
then have [simp]:"{..A} ∪ {A<..x} = {..x}"
by auto
with set_integrable_Un[OF r_integrable1[OF order.refl] r_integrabl2[OF Ax]]
show ?thesis
by simp
qed fact
qed
have 3:"r ∈ borel_measurable borel"
by(simp add: r_def)
have 4:"(r ⤏ ρ) at_top"
by(rule tendsto_cong[THEN iffD1,OF eventually_at_top_linorderI[where c="A + 1"] lim_r'])
(simp add: r_def)
have 5:"bounded (range r)"
proof -
have eq:"r ` {A..} ∪ r ` {..<A} = range r"
by fastforce
have *:"bounded (r ` {A..})"
using bdd bounded_iff by(auto simp: r_def bounded_subset image_mono)
have **:"bounded (r ` {..<A})"
by(auto simp: bounded_iff r_def)
have "bounded (r ` {A..} ∪ r ` {..<A})"
by(simp add: * **)
thus ?thesis
by(simp add: eq)
qed
have 6:"c ∈ borel_measurable (restrict_space borel {0<..})"
unfolding c_def
proof(subst measurable_If)
show "c' ∈ borel_measurable (restrict_space borel {0<..})"
by(auto intro!: measurable_restrict_space1)
show "{x ∈ space (restrict_space borel {0<..}). A < x} ∈ sets (restrict_space borel {0<..})"
using borel_measurable_const measurable_id measurable_inequality_set_flipped
measurable_restrict_space1 by blast
qed(use regularly_varying_meas[OF rv] in auto)
have 7:"∀x>0. 0 < c x"
using c'_pos regularly_varying_pos[OF rv] by(simp add: c_def)
have 8:"(c ⤏ C) at_top"
by(rule tendsto_cong[THEN iffD1,OF eventually_at_top_linorderI[where c="A + 1"] lim_c'])
(simp add: c_def)
show ?thesis
using 1 2 3 4 5 6 7 8 C_pos by blast
qed
lemma Karamata_representation_iff:
assumes U_meas:"U ∈ borel_measurable (restrict_space borel {0<..})"
and U_pos:"⋀x. 0 < x ⟹ 0 < U x"
shows "regularly_varying U ρ ⟷
(∃A>0. ∃c r C.
(∀x ≥ A. U x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel))
∧ (∀x ≥ A. set_integrable lborel {A<..x} (λt. r t / t))
∧ (r ⤏ ρ) at_top
∧ (c ⤏ C) at_top
∧ 0 < C)"
proof(safe intro!: regularly_varyingI)
fix A c r C x
assume A:"0 < A" and x_pos:"(0 :: real) < x"
and eq_U:"∀x≥A. U x =
c x * exp (∫t∈{A<..x}. r t / t ∂lborel)"
and integ:"∀x≥A. set_integrable lborel {A<..x}
(λt. r t / t)"
and lim_r:"(r ⤏ ρ) at_top"
and C_pos:"0 < C"
and lim_c:"(c ⤏ C) at_top"
have lim_powr1:"((λs. x powr s) ⤏ 1) (at_right 0)"
using tendsto_powr[OF tendsto_const[of x] tendsto_ident_at[of 0]] x_pos by simp
have lim_powr2:"((λs. x powr (- s)) ⤏ 1) (at_right 0)"
using tendsto_powr[OF tendsto_const[of x] tendsto_minus[OF tendsto_ident_at[of 0]]] x_pos
by simp
have *:"∀⇩F t in at_top. U (t * x) / U t
= (c (t * x) / c t)
* exp ((∫s∈{A<..t * x}. r s / s ∂lborel) - (∫s∈{A<..t}. r s / s ∂lborel))"
using x_pos A eq_U
by(auto intro!: eventually_at_top_linorderI[where c="max (A / x) A"]
simp: divide_le_eq exp_diff)
have **:"((λt. c (t * x) / c t) ⤏ C / C) at_top"
using C_pos
by(intro tendsto_divide filterlim_ident lim_c tendsto_const
filterlim_compose[OF lim_c filterlim_at_top_mult_tendsto_pos[OF _ x_pos]]) simp
have ***:"((λt. exp ((∫s∈{A<..t * x}. r s / s ∂lborel) - (∫s∈{A<..t}. r s / s ∂lborel)))
⤏ x powr ρ) at_top"
proof -
consider "x < 1" | "x = 1" | "1 < x"
by linarith
then show ?thesis
proof cases
assume x:"x < 1"
show ?thesis
proof(rule tendsto_sandwich_mult_const[OF _ lim_powr1 lim_powr2])
fix e :: real
assume e:"0 < e"
obtain T1 where T1:"⋀t. T1 ≤ t ⟹ r t ≤ ρ + e" "⋀t. T1 ≤ t ⟹ ρ - e ≤ r t"
using tendstoD[OF lim_r e] unfolding eventually_at_top_linorder dist_real_def
by (metis abs_diff_le_iff less_eq_real_def)
define T where "T ≡ max (A / x) (T1 / x)"
show "∀⇩F t in at_top.
x powr e ≤ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ
∧ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ
≤ x powr - e"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
then have t_pos:"0 < t" and tx:"t * x ≤ t"
using A x_pos x
by(auto simp: T_def order.strict_trans2[OF divide_pos_pos[OF A x_pos]])
hence Atx:"A ≤ t * x" and At:"A ≤ t"
using A t x_pos x
by(auto simp: T_def divide_le_eq intro!: order.trans[of A "t * x" t] mult_left_le)
have t_le:"⋀s. t * x ≤ s ⟹ r s ≤ ρ + e" and le_t:"⋀s. t * x ≤ s ⟹ ρ - e ≤ r s"
using t x_pos x by(auto simp: T_def divide_le_eq intro!: T1)
have "exp ((∫s∈{A<..t * x}. r s / s ∂lborel) - (∫s∈{A<..t}. r s / s ∂lborel))
= exp ((∫s∈{t * x<..t}. - r s / s ∂lborel))"
unfolding set_lebesgue_integral_def
using integ At Atx tx
by(subst Bochner_Integration.integral_diff[symmetric])
(auto simp: set_lebesgue_integral_def set_integrable_def indicator_def
simp del: integral_minus Bochner_Integration.integral_diff
intro!: Bochner_Integration.integral_cong)
also have "... ≤ exp ((∫s∈{t * x<..t}. - (ρ - e) / s ∂lborel))"
using integ At Atx A
by(auto simp: set_integrable_uminus simp del: minus_diff_eq
intro!: le_t set_integral_mono divide_right_mono set_integrable_inverse'
set_integrable_subset[where A="{A<..t}" and B="{t * x<..t}"])
also have "... = exp ((ρ - e) * ln x)"
using A Atx x_pos t_pos x
by(subst set_integral_inverse) (auto simp: left_diff_distrib' ln_mult)
also have "... = x powr (ρ - e)"
by (metis nless_le powr_def x_pos)
finally have "exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) ≤ x powr (ρ - e)" .
from divide_right_mono[OF this,of "x powr ρ"]
show "exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ ≤ x powr - e"
using x_pos by(auto simp: powr_diff[symmetric])
have "x powr (ρ + e) = exp ((ρ + e) * ln x)"
using x_pos by(simp add: powr_def)
also have "... = exp ((∫s∈{t* x<..t}. - (ρ + e) / s ∂lborel))"
using t_pos A Atx tx
by(subst set_integral_inverse) (auto simp: ln_mult left_diff_distrib' distrib_right)
also have "... ≤ exp ((∫s∈{t * x<..t}. - r s / s ∂lborel))"
using integ At Atx A
by(auto simp: set_integrable_uminus simp del: minus_add_distrib
intro!: t_le set_integral_mono divide_right_mono set_integrable_inverse'
set_integrable_subset[where A="{A<..t}" and B="{t * x<..t}"])
also have "... = exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel))"
unfolding set_lebesgue_integral_def
using integ At Atx tx
by(subst Bochner_Integration.integral_diff[symmetric])
(auto simp: set_lebesgue_integral_def set_integrable_def indicator_def
simp del: integral_minus Bochner_Integration.integral_diff
intro!: Bochner_Integration.integral_cong)
finally have "x powr (ρ + e) ≤ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel))" .
from divide_right_mono[OF this,of "x powr ρ"]
show "x powr e ≤ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ"
using x_pos by(auto simp: powr_diff[symmetric])
qed
qed
next
assume x:"1 < x"
show ?thesis
proof(rule tendsto_sandwich_mult_const[OF _ lim_powr2 lim_powr1])
fix e :: real
assume e:"0 < e"
obtain T1 where T1:"⋀t. T1 ≤ t ⟹ r t ≤ ρ + e" "⋀t. T1 ≤ t ⟹ ρ - e ≤ r t"
using tendstoD[OF lim_r e] unfolding eventually_at_top_linorder dist_real_def
by (metis abs_diff_le_iff less_eq_real_def)
define T where "T ≡ max A T1"
show "∀⇩F t in at_top.
x powr (- e) ≤ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ
∧ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ
≤ x powr e"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
then have t_pos:"0 < t" and tx:"t ≤ t * x"
using A x_pos x
by(auto simp: T_def order.strict_trans2[OF divide_pos_pos[OF A x_pos]])
hence Atx:"A ≤ t * x" and At:"A ≤ t"
using t tx by(auto simp: T_def order.trans)
have t_le:"⋀s. t ≤ s ⟹ r s ≤ ρ + e" and le_t:"⋀s. t ≤ s ⟹ ρ - e ≤ r s"
using t by(auto simp: T_def intro!:T1)
have "exp ((∫s∈{A<..t * x}. r s / s ∂lborel) - (∫s∈{A<..t}. r s / s ∂lborel))
= exp ((∫s∈{t<..t * x}. r s / s ∂lborel))"
unfolding set_lebesgue_integral_def
using integ At Atx tx
by(subst Bochner_Integration.integral_diff[symmetric])
(auto simp: set_lebesgue_integral_def set_integrable_def indicator_def
simp del: integral_minus Bochner_Integration.integral_diff
intro!: Bochner_Integration.integral_cong)
also have "... ≤ exp ((∫s∈{t<..t * x}. (ρ + e) / s ∂lborel))"
using integ At Atx A tx
by(fastforce simp:
intro!: t_le set_integral_mono divide_right_mono set_integrable_inverse'
set_integrable_subset[where A="{A<..t*x}" and B="{t<..t * x}"])
also have "... = exp ((ρ + e) * ln x)"
using A Atx x_pos t_pos x
by(subst set_integral_inverse) (auto simp: left_diff_distrib' ln_mult)
also have "... = x powr (ρ + e)"
by (metis nless_le powr_def x_pos)
finally have "exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) ≤ x powr (ρ + e)" .
from divide_right_mono[OF this,of "x powr ρ"]
show "exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ ≤ x powr e"
using x_pos by(auto simp: powr_diff[symmetric])
have "x powr (ρ - e) = exp ((ρ - e) * ln x)"
using x_pos by(simp add: powr_def)
also have "... = exp ((∫s∈{t<..t*x}. (ρ - e) / s ∂lborel))"
using t_pos A Atx tx
by(subst set_integral_inverse) (auto simp: ln_mult left_diff_distrib' distrib_right)
also have "... ≤ exp ((∫s∈{t<..t * x}. r s / s ∂lborel))"
using integ At Atx A tx
by(fastforce simp:
intro!: le_t set_integral_mono divide_right_mono set_integrable_inverse'
set_integrable_subset[where A="{A<..t*x}" and B="{t<..t * x}"])
also have "... = exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel))"
unfolding set_lebesgue_integral_def
using integ At Atx tx
by(subst Bochner_Integration.integral_diff[symmetric])
(auto simp: set_lebesgue_integral_def set_integrable_def indicator_def
simp del: integral_minus Bochner_Integration.integral_diff
intro!: Bochner_Integration.integral_cong)
finally have "x powr (ρ - e) ≤ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel))" .
from divide_right_mono[OF this,of "x powr ρ"]
show "x powr (- e) ≤ exp ((∫s∈{A<..t * x}. r s / s ∂lborel)
- (∫s∈{A<..t}. r s / s ∂lborel)) / x powr ρ"
using x_pos by(auto simp: powr_diff[symmetric])
qed
qed
qed simp
qed
have "((λt. (c (t * x) / c t)
* exp ((∫s∈{A<..t * x}. r s / s ∂lborel) - (∫s∈{A<..t}. r s / s ∂lborel)))
⤏ x powr ρ) at_top"
using tendsto_mult[OF ** ***] C_pos by simp
thus "((λt. U (t * x) / U t) ⤏ x powr ρ) at_top"
using tendsto_cong * by fast
qed(use assms Karamata_representation_ex in blast)+
subsubsection ‹Theorems Obtained from Karamata's Representation Theorem›
lemma
assumes rv:"regularly_varying U ρ"
shows regularly_varying_pos_at_top:"0 < ρ ⟹ filterlim U at_top at_top"
and regularly_varying_neg_at_top:"ρ < 0 ⟹ (U ⤏ 0) at_top"
proof -
let ?h = "λx. ln (U (exp x))"
from Karamata_representation_ln_exp[OF rv]
obtain A c e C where A:"0 < A"
and eq_h: "⋀x. ln A ≤ x ⟹ ?h x = c x + ρ * ln A + (∫u∈{ln A<..x}. ρ + e u ∂lborel)"
and integrable: "⋀x. ln A ≤ x ⟹ set_integrable lborel {ln A<..x} e"
and lim_e: "(e ⤏ 0) at_top"
and lim_c: "(c ⤏ C) at_top"
by blast
obtain X1 where X1:"⋀x. X1 ≤ x ⟹ C - 1 < c x" "⋀x. X1 ≤ x ⟹ c x < C + 1"
using tendstoD[OF lim_c,of 1]
unfolding eventually_at_top_linorder dist_real_def abs_less_iff
by fastforce
have lim_h_pos: "0 < ρ ⟹ filterlim ?h at_top at_top"
proof -
assume rho:"0 < ρ"
obtain X2 where X2:"⋀x. X2 ≤ x ⟹ ¦e x¦ < ρ / 2"
using tendstoD[OF lim_e half_gt_zero[OF rho]]
by (metis (no_types, lifting) eventually_at_top_linorder norm_conv_dist real_norm_def)
define X where "X ≡ max (ln A) (max X1 X2)"
have le_X:"ln A ≤ X" "X1 ≤ X" "X2 ≤ X"
by(simp_all add: X_def)
have X:"⋀x. X ≤ x ⟹ - ρ / 2 ≤ e x" "⋀x. X ≤ x ⟹ C - 1 ≤ c x"
using X2 X1 X_def by force+
have "∀⇩F x in at_top. ?h x ≥ C - 1 + ρ * ln A + (∫u∈{ln A<..X}. ρ + e u ∂lborel)
+ (- ρ / 2) * X + (ρ / 2) * x" (is "∀⇩F x in at_top. ?h x ≥ ?f x")
proof(rule eventually_at_top_linorderI[where c=X])
fix x
assume x:"X ≤ x"
have "?f x = C - 1 + ρ * ln A + (∫u∈{ln A<..X}. ρ + e u ∂lborel) + (ρ / 2) * (x - X)"
by argo
also have "... = C - 1 + ρ * ln A
+ ((∫u∈{ln A<..X}. ρ + e u ∂lborel) + (∫u∈{X<..x}. ρ / 2 ∂lborel))"
by(simp add: interval_integral_Ioc[OF x,symmetric])
also have "... ≤ C - 1 + ρ * ln A
+ ((∫u∈{ln A<..X}. ρ + e u ∂lborel) + (∫u∈{X<..x}. ρ + e u ∂lborel))"
using X x le_X by(auto simp del: set_integral_divide_zero
simp: real_0_le_add_iff minus_divide_le_eq
intro!: set_integral_mono_banach set_integrable_subset[OF integrable[of x]]
set_integrable_const)
also have "... = C - 1 + ρ * ln A + ((∫u∈{ln A<..X} ∪ {X<..x}. ρ + e u ∂lborel))"
using le_X x by(auto intro!: set_integral_Un[symmetric]
set_integrable_subset[OF integrable[of x]] set_integrable_const)
also have "... = C - 1 + ρ * ln A + ((∫u∈{ln A<..x}. ρ + e u ∂lborel))"
using x le_X by(subst ivl_disj_un_two) auto
also have "... ≤ ?h x"
using le_X x X by(simp add: eq_h[of x])
finally show "?f x ≤ ?h x" .
qed
moreover have "filterlim ?f at_top at_top"
by(intro filterlim_tendsto_add_at_top
filterlim_tendsto_pos_mult_at_top[OF _ half_gt_zero[OF rho]] filterlim_ident)
blast+
ultimately show ?thesis
using filterlim_at_top_mono by fast
qed
show "filterlim U at_top at_top" if rho:"0 < ρ"
proof -
note filterlim_compose[OF exp_at_top filterlim_compose[OF lim_h_pos[OF rho] ln_at_top]]
moreover have "∀⇩F x in at_top. exp (?h (ln x)) = U x"
using regularly_varying_pos[OF rv] by(auto intro!: eventually_at_top_linorderI[where c=1])
ultimately show ?thesis
by(simp cong: filterlim_cong)
qed
have lim_h_neg: "ρ < 0 ⟹ filterlim ?h at_bot at_top"
proof -
assume rho:"ρ < 0"
obtain X2 where X2:"⋀x. X2 ≤ x ⟹ ¦e x¦ < - ρ / 2"
using tendstoD[OF lim_e half_gt_zero[OF neg_0_less_iff_less[THEN iffD2,OF rho]]]
by (metis (no_types, lifting) eventually_at_top_linorder norm_conv_dist real_norm_def)
define X where "X ≡ max (ln A) (max X1 X2)"
have le_X:"ln A ≤ X" "X1 ≤ X" "X2 ≤ X"
by(simp_all add: X_def)
have X:"⋀x. X ≤ x ⟹ e x ≤ - ρ / 2" "⋀x. X ≤ x ⟹ c x ≤ C + 1"
using X2 X1 X_def by force+
have "∀⇩F x in at_top. ?h x ≤ C + 1 + ρ * ln A + (∫u∈{ln A<..X}. ρ + e u ∂lborel)
+ (- ρ / 2) * X + (ρ / 2) * x"
(is "∀⇩F x in at_top. ?h x ≤ ?g x")
proof(rule eventually_at_top_linorderI[where c=X])
fix x
assume x:"X ≤ x"
have "?h x ≤ C + 1 + ρ * ln A + ((∫u∈{ln A<..x}. ρ + e u ∂lborel))"
using le_X x X by(simp add: eq_h[of x])
also have "... = C + 1 + ρ * ln A + ((∫u∈{ln A<..X} ∪ {X<..x}. ρ + e u ∂lborel))"
using x le_X by(subst ivl_disj_un_two) auto
also have "... = C + 1 + ρ * ln A
+ ((∫u∈{ln A<..X}. ρ + e u ∂lborel) + (∫u∈{X<..x}. ρ + e u ∂lborel))"
using le_X x by(auto intro!: set_integral_Un
set_integrable_subset[OF integrable[of x]] set_integrable_const)
also have "... ≤ C + 1 + ρ * ln A
+ ((∫u∈{ln A<..X}. ρ + e u ∂lborel) + (∫u∈{X<..x}. ρ / 2 ∂lborel))"
using X x le_X by(auto simp del: set_integral_divide_zero
simp: real_add_le_0_iff le_minus_divide_eq
intro!: set_integral_mono_banach set_integrable_subset[OF integrable[of x]]
set_integrable_const)
also have "... = ?g x"
by(simp add: interval_integral_Ioc[OF x,symmetric] right_diff_distrib)
finally show "?h x ≤ ?g x" .
qed
moreover have "filterlim ?g at_bot at_top"
using rho
by (intro filterlim_tendsto_add_at_bot_iff[THEN iffD2]
filterlim_tendsto_neg_mult_at_bot[where c="ρ / 2"] filterlim_ident)
fastforce+
ultimately show ?thesis
using filterlim_at_bot_mono by fast
qed
show "(U ⤏ 0) at_top" if rho:"ρ < 0"
proof -
note filterlim_compose[OF exp_at_bot filterlim_compose[OF lim_h_neg[OF rho] ln_at_top]]
moreover have "∀⇩F x in at_top. exp (?h (ln x)) = U x"
using regularly_varying_pos[OF rv] by(auto intro!: eventually_at_top_linorderI[where c=1])
ultimately show ?thesis
by(simp cong: filterlim_cong)
qed
qed
subsubsection ‹Uniform Convergence Theorem for $\rho \neq 0$›
corollary regularly_varying_pos_UCT:
assumes rv:"regularly_varying U ρ"
and bdd:"⋀x. 0 < x ⟹ bounded (U ` {0<..x})"
and rho:"0 < ρ"
and a: "0 < a"
shows "uniform_limit {0<..a} (λt x. U (t * x) / U t) (λx. x powr ρ) at_top"
unfolding uniform_limit_iff dist_real_def
proof safe
fix e :: real
assume e:"0 < e"
define e' where "e' ≡ min e (1 / 2)"
have e'_pos:"0 < e'" and e'_le_1:"e' < 1"
using e by(simp_all add: e'_def)
obtain i where i_pos:"0 < i" and i:"ρ - i > 0"
using rho dense by auto
from Karamata_representation_ex[OF rv]
obtain A c r C where A_pos:"0 < A"
and eq_U:"⋀x. A ≤ x ⟹ U x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel)"
and integ:"⋀x. A ≤ x ⟹ set_integrable lborel {A<..x} (λt. r t / t)"
and lim_r:"(r ⤏ ρ) at_top"
and r_meas[measurable]: "r ∈ borel_measurable borel"
and lim_c:"(c ⤏ C) at_top"
and C_pos:"0 < C"
by blast
define X where "X ≡ min (min (1 / 2) ((e' / 4) powr (1 / ρ))) ((e' / 16) powr (1 / (ρ - i)))"
have X_pos:"0 < X" and X_le_1:"X < 1"
and X_e':"X powr ρ < e' / 2"
using e'_pos rho by(auto simp: X_def powr_powr simp del: less_divide_eq_numeral1
intro!: order.strict_trans1[OF powr_mono2[OF _ _ min.coboundedI2[THEN min.coboundedI1]]])
have X_e2':"X powr (ρ - i) < e' / 8"
using e'_pos e'_le_1 i by(auto simp: X_def powr_powr simp del: less_divide_eq_numeral1
intro!: order.strict_trans1[OF powr_mono2[OF _ _ min.coboundedI2]]
order.strict_trans2[OF powr_less_mono'[where x="e' / 8" and a = i]])
have X_e:"⋀x. 0 < x ⟹ x ≤ X ⟹ x powr ρ < e / 2"
using X_e' by (smt (verit, del_insts) rho e'_def field_sum_of_halves powr_mono2)
have X_e2:"x powr (ρ - i) < e / 8" if xX:"x ≤ X" and x:"0 < x" for x
using i
by(intro order.strict_trans2[OF order.strict_trans1
[OF powr_mono2[OF _ less_imp_le[OF x] xX,of "ρ - i"] X_e2']])
(simp_all add: e'_def)
obtain T1 where T1:"⋀x. T1 ≤ x ⟹ ρ - i ≤ r x" "⋀x. T1 ≤ x ⟹ 0 < r x"
using tendstoD[OF lim_r i_pos] tendstoD[OF lim_r rho] rho i_pos i
unfolding eventually_at_top_linorder dist_real_def abs_less_iff
by fastforce
obtain T2 where T2':"⋀x. T2 ≤ x ⟹ ¦c x - C¦ ≤ C / 2"
using tendstoD[OF lim_c half_gt_zero[OF C_pos]]
unfolding eventually_at_top_linorder dist_real_def
by fastforce
have T2:"C / 2 ≤ c x" "c x ≤ 2 * C" if x:"T2 ≤ x" for x
using T2'[OF x] by argo+
define L where "L ≡ λx. U x / x powr ρ"
have sv:"slowly_varying L"
by(simp add: regularly_varying_iff_slowly_varying_divide_powr[of U,symmetric] L_def rv)
have "0 < e / a powr ρ"
using e a by auto
from uniform_limitD[OF slowly_varying_UCT[OF sv X_pos,of a] this]
obtain T3 where T3:"⋀t x. T3 ≤ t ⟹ X ≤ x ⟹ x ≤ a
⟹ ¦L (t * x) / L t - 1¦ < e / a powr ρ"
unfolding dist_real_def eventually_at_top_linorder
by (meson atLeastAtMost_iff)
define T' where "T' ≡ max (max (max (A / X) A) T3) (max T1 T2)"
have T':"A ≤ T'" "0 < T'" "A / X≤ T'"
and T'_le1:"⋀x. T' ≤ x ⟹ ρ - i ≤ r x" "⋀x. T' ≤ x ⟹ 0 < r x"
and T'_le2:"⋀x. T' ≤ x ⟹ C / 2 ≤ c x"
and T'_le2': "⋀x. T' ≤ x ⟹ c x ≤ 2 * C"
and T'_le3:"⋀t x. T' ≤ t ⟹ X ≤ x ⟹ x ≤ a ⟹ ¦L (t * x) / L t - 1¦ < e / a powr ρ"
using T1 T2 T3 A_pos by(auto simp: T'_def)
from bdd[of T'] regularly_varying_pos[OF rv] T'
obtain K where K:"⋀x. 0 < x ⟹ x ≤ T' ⟹ ¦U x¦ ≤ K"
unfolding bounded_iff by fastforce
have "((λx. K / U x) ⤏ 0) at_top"
by(intro real_tendsto_divide_at_top regularly_varying_pos_at_top[OF rv rho]) auto
then obtain T'' where T'':"⋀t. T'' ≤ t ⟹ ¦K / U t¦ < e / 2"
by (metis (mono_tags, lifting) divide_pos_pos e eventually_at_top_linorder
less_le norm_conv_dist real_norm_def tendstoD zero_le_numeral zero_neq_numeral)
define T where "T ≡ max T' T''"
have T:"T' ≤ T" "T'' ≤ T"
by(simp_all add: T_def)
show "∀⇩F t in at_top. ∀x∈{0<..a}. ¦U (t * x) / U t - x powr ρ¦ < e"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t x
assume t:"T ≤ t" and "x ∈ {0<..a}"
then have x_pos:"0 < x" and x_a: "x ≤ a"
and T't:"T' ≤ t" and t_pos:"0 < t" and T''t:"T'' ≤ t"
using T A_pos by (auto simp: T'_def)
then consider "x ≤ X" "T' ≤ t * x" | "x ≤ X" "t * x ≤ T'" | "X ≤ x"
by fastforce
thus "¦U (t * x) / U t - x powr ρ¦ < e"
proof cases
assume x:"X ≤ x"
have "¦U (t * x) / U t - x powr ρ¦ = x powr ρ * ¦L (t * x) / L t - 1¦"
using T T' t x_pos by(simp add: L_def powr_mult abs_mult_pos' right_diff_distrib)
also have "... ≤ a powr ρ * ¦L (t * x) / L t - 1¦"
using x_pos x_a rho by(intro mult_mono powr_mono2) auto
also have "... < e"
using a mult_le_less_imp_less[OF order.refl[of "a powr ρ"] T'_le3[OF T't x x_a]] by force
finally show ?thesis .
next
assume x:"x ≤ X" and txT:"t * x ≤ T'"
have "¦U (t * x) / U t¦ ≤ ¦K / U t¦"
using K[OF _ txT] x_pos t_pos by (simp add: divide_right_mono)
also have "... < e / 2"
by(intro T'' T''t)
finally have *:"¦U (t * x) / U t¦ < e / 2" .
have "¦U (t * x) / U t - x powr ρ¦ ≤ ¦U (t * x) / U t¦ + ¦x powr ρ¦"
by argo
also have "... < e / 2 + e / 2"
unfolding abs_of_nonneg[OF powr_ge_zero]
by(intro add_strict_mono * X_e x_pos x)
finally show ?thesis
by simp
next
assume x:"x ≤ X" and Ttx:"T' ≤ t * x"
have Atx:"A ≤ t * x" and At:"A ≤ t" and ttx:"t * x ≤ t" and tx_pos:"0 < t * x"
using x T' t T Ttx X_pos A_pos x_pos X_le_1 by auto
have im_ln:"ln ` {t * x<..t} = {ln (t * x) <..ln t}"
using ttx tx_pos
by(intro image_mono_on_continuous_on_Ioc ttx monotone_onI continuous_on_ln ln_strict_mono)
auto
have "U (t * x) / U t = c (t * x) * exp (∫u∈{A<..t * x}. r u / u ∂lborel)
/ (c t * exp (∫u∈{A<..t}. r u / u ∂lborel))"
by(simp add: eq_U Atx At)
also have "... = (c (t * x) / c t) * exp ((∫u∈{A<..t * x}. r u / u ∂lborel)
- (∫u∈{A<..t}. r u / u ∂lborel))"
by (simp add: exp_diff)
also have "... ≤ (2 * C / (C / 2)) * exp ((∫u∈{A<..t * x}. r u / u ∂lborel)
- (∫u∈{A<..t}. r u / u ∂lborel))"
using frac_le[OF _ T'_le2'[OF Ttx] _ T'_le2[OF T't]] C_pos by(intro mult_mono) auto
also have "... = 4 * exp ((∫u. indicat_real {A<..t * x} u * r u / u
- indicat_real {A<..t} u * r u / u ∂lborel))"
using integ[OF Atx] integ[OF At] C_pos
by(auto simp: set_lebesgue_integral_def set_integrable_def)
also have "... = 4 * exp (∫u∈{t*x<..t}. - (r u / u) ∂lborel)"
using ttx Atx At
by(auto intro!: Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def simp del: integral_minus)
also have "... ≤ 4 * exp (∫u∈{t*x<..t}. - (ρ - i) / u ∂lborel)"
unfolding divide_minus_left
using Atx ttx tx_pos Ttx rho i T'_le1
by(intro mult_mono exp_mono set_integral_mono
set_integrable_subset[THEN set_integrable_uminus[THEN iffD2],OF integ,of t])
(fastforce simp: set_integrable_def
intro!: integrableI_bounded_set[where A="{t * x<..t}" and B="¦ρ - i¦ / (t * x)"]
divide_mono)+
also have "... = 4 * exp (- (ρ - i) * (ln t - ln (t * x)))"
by(subst set_integral_inverse) (use ttx tx_pos in auto)
also have "... = 4 * exp (- (ρ - i) * ln (1 / x))"
using A_pos At Atx
by(subst ln_divide_pos[symmetric]) auto
also have "... = 4 * exp ((ρ - i) * ln x)"
by(simp add: x_pos ln_divide_pos[of 1 x] minus_mult_right mult.commute)
also have "... = 4 * x powr (ρ - i)"
using x_pos i by(simp add: powr_def X_def)
also have "... < e / 2"
using x X_e2 x_pos by force
finally have *:"¦U (t * x) / U t¦ < e / 2"
by (simp add: regularly_varying_pos[OF rv] abs_of_pos t_pos tx_pos)
have "¦U (t * x) / U t - x powr ρ¦ ≤ ¦U (t * x) / U t¦ + ¦x powr ρ¦"
by linarith
also have "... < e / 2 + e / 2"
using * X_e[OF x_pos x] by(intro add_strict_mono) auto
finally show ?thesis
by fastforce
qed
qed
qed
corollary regularly_varying_neg_UCT:
assumes rv:"regularly_varying U ρ"
and rho:"ρ < 0"
and a: "0 < a"
shows "uniform_limit {a..} (λt x. U (t * x) / U t) (λx. x powr ρ) at_top"
unfolding uniform_limit_iff dist_real_def
proof safe
fix e :: real
assume e:"0 < e"
obtain i where i_pos:"0 < i" and i:"ρ + i < 0"
by (metis rho neg_0_less_iff_less real_add_less_0_iff real_arch_inverse)
from Karamata_representation_ex[OF rv]
obtain A c r C where A_pos:"0 < A"
and eq_U:"⋀x. A ≤ x ⟹ U x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel)"
and integ:"⋀x. A ≤ x ⟹ set_integrable lborel {A<..x} (λt. r t / t)"
and lim_r:"(r ⤏ ρ) at_top"
and lim_c:"(c ⤏ C) at_top"
and C_pos:"0 < C"
by blast
from tendstoD[OF tendsto_neg_powr[OF rho filterlim_ident] half_gt_zero[OF e]]
obtain X1 where X1:"⋀x. X1 ≤ x ⟹ x powr ρ < e / 2"
unfolding eventually_at_top_linorder dist_real_def by auto
from tendstoD[OF tendsto_mult_right_zero[OF tendsto_neg_powr[OF i filterlim_ident],of 4]
half_gt_zero[OF e]]
obtain X2 where X2:"⋀x. X2 ≤ x ⟹ 4 * x powr (ρ + i) < e / 2"
unfolding eventually_at_top_linorder dist_real_def by auto
define X where "X ≡ max (max 1 a) (max X1 X2)"
have X:"⋀x. X ≤ x ⟹ x powr ρ < e / 2" "⋀x. X ≤ x ⟹ 4 * x powr (ρ + i) < e / 2"
"⋀x. X ≤ x ⟹ 0 < x powr ρ" "⋀x. X ≤ x ⟹ 0 < 4 * x powr ρ"
using X1 X2 by(auto simp: X_def)
obtain T1 where T1:"⋀x. T1 ≤ x ⟹ r x ≤ ρ + i"
using tendstoD[OF lim_r i_pos] unfolding eventually_at_top_linorder dist_real_def abs_less_iff
by fastforce
obtain T2 where T2':"⋀x. T2 ≤ x ⟹ ¦c x - C¦ ≤ C / 2"
using tendstoD[OF lim_c half_gt_zero[OF C_pos]]
unfolding eventually_at_top_linorder dist_real_def
by fastforce
have T2:"C / 2 ≤ c x" "c x ≤ 2 * C" if x:"T2 ≤ x" for x
using T2'[OF x] by argo+
define L where "L ≡ λx. U x / x powr ρ"
have sv:"slowly_varying L"
by(simp add: regularly_varying_iff_slowly_varying_divide_powr[of U,symmetric] L_def rv)
have "0 < e / a powr ρ"
using e a by auto
from uniform_limitD[OF slowly_varying_UCT[OF sv a,of X] this]
obtain T3 where T3:"⋀t x. T3 ≤ t ⟹ a ≤ x ⟹ x ≤ X ⟹ ¦L (t * x) / L t - 1¦ < e / a powr ρ"
unfolding dist_real_def eventually_at_top_linorder
by (meson atLeastAtMost_iff)
define T where "T ≡ max (max A T3) (max T1 T2)"
have T:"A ≤ T" "0 < T"
and T_le1:"⋀x. T ≤ x ⟹ r x ≤ ρ + i"
and T_le2:"⋀x. T ≤ x ⟹ C / 2 ≤ c x" and T_le2': "⋀x. T ≤ x ⟹c x ≤ 2 * C"
and T_le3:"⋀t x. T ≤ t ⟹ a ≤ x ⟹ x ≤ X ⟹ ¦L (t * x) / L t - 1¦ < e / a powr ρ"
using T1 T2 T3 A_pos by(auto simp: T_def)
show "∀⇩F t in at_top. ∀x∈{a..}. ¦U (t * x) / U t - x powr ρ¦ < e"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t x
assume t:"T ≤ t" and "a ≤ x"
then consider "a ≤ x" "x ≤ X" | "X ≤ x"
by fastforce
thus "¦U (t * x) / U t - x powr ρ¦ < e"
proof cases
assume x:"a ≤ x" "x ≤ X"
have "¦U (t * x) / U t - x powr ρ¦ = x powr ρ * ¦L (t * x) / L t - 1¦"
using T t x a by(simp add: L_def powr_mult abs_mult_pos' right_diff_distrib)
also have "... ≤ a powr ρ * ¦L (t * x) / L t - 1¦"
using x a rho by(intro mult_mono powr_mono2') auto
also have "... < e"
using a mult_le_less_imp_less[OF order.refl[of "a powr ρ"] T_le3[OF t x]] by force
finally show ?thesis .
next
assume x:"X ≤ x"
have Atx:"A ≤ t * x" and At:"A ≤ t" and ttx:"t ≤ t * x"
using x t mult_mono[of A t 1 x] A_pos by(auto simp: X_def T_def)
hence Ttx:"T ≤ t * x"
using t by linarith
have im_ln:"ln ` {t<..t * x} = {ln t <..ln (t * x)}"
using At A_pos
by(intro image_mono_on_continuous_on_Ioc ttx monotone_onI continuous_on_ln ln_strict_mono)
auto
have "U (t * x) / U t = c (t * x) * exp (∫u∈{A<..t * x}. r u / u ∂lborel)
/ (c t * exp (∫u∈{A<..t}. r u / u ∂lborel))"
by(simp add: eq_U Atx At)
also have "... = (c (t * x) / c t) * exp ((∫u∈{A<..t * x}. r u / u ∂lborel)
- (∫u∈{A<..t}. r u / u ∂lborel))"
by (simp add: exp_diff)
also have "... ≤ (2 * C / (C / 2)) * exp ((∫u∈{A<..t * x}. r u / u ∂lborel)
- (∫u∈{A<..t}. r u / u ∂lborel))"
using frac_le[OF _ T_le2'[OF Ttx] _ T_le2[OF t]] C_pos by(intro mult_mono) auto
also have "... = 4 * exp ((∫u. indicat_real {A<..t * x} u * r u / u
- indicat_real {A<..t} u * r u / u ∂lborel))"
using integ[OF Atx] integ[OF At] C_pos
by(auto simp: set_lebesgue_integral_def set_integrable_def)
also have "... = 4 * exp (∫u∈{t<..t * x}. r u / u ∂lborel)"
using ttx Atx At by(auto intro!: Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def)
also have "... ≤ 4 * exp (∫u∈{t<..t * x}. (ρ + i) / u ∂lborel)"
using ttx At T_le1 T t Atx
by(fastforce intro!: set_integral_mono set_integrable_subset[OF integ,of "t * x"]
divide_right_mono integrableI_bounded_set[where A="{t<..t * x}" and B="¦ρ + i¦ / t"]
divide_mono simp: set_borel_measurable_def set_integrable_def)
also have "... = 4 * exp ((ρ + i) * (ln (t * x) - ln t))"
by(subst set_integral_inverse) (use A_pos At ttx in auto)
also have "... = 4 * exp ((ρ + i) * ln x)"
using A_pos At Atx
by(subst ln_divide_pos[symmetric]) auto
also have "... = 4 * x powr (ρ + i)"
using x a by(simp add: powr_def X_def)
also have "... < e / 2"
using X x by blast
finally have *:"¦U (t * x) / U t¦ < e / 2"
by (smt (verit, best) A_pos At rv divide_pos_pos regularly_varying_pos ttx)
have "¦U (t * x) / U t - x powr ρ¦ ≤ ¦U (t * x) / U t¦ + ¦x powr ρ¦"
by linarith
also have "... < e / 2 + e / 2"
using * X[OF x] by(intro add_strict_mono) auto
finally show ?thesis
by fastforce
qed
qed
qed
subsubsection ‹Potter Bounds›
corollary
assumes rv:"regularly_varying U ρ"
and A:"1 < A" and d:"0 < d"
shows Potter_bounds1:
"∃T>0. ∀x≥T. ∀y≥x. U y / U x ≤ A * (y / x) powr (ρ + d)" (is ?g1)
and Potter_bounds2:
"∃T>0. ∀y≥T. ∀x≥y. U y / U x ≤ A * (y / x) powr (ρ - d)" (is ?g2)
and Potter_bounds:
"∃T>0. ∀x≥T. ∀y≥T. U y / U x ≤ A * max ((y / x) powr (ρ + d)) ((y / x) powr (ρ - d))"
(is ?g3)
proof -
from Karamata_representation_ex[OF rv]
obtain B c r C where A_pos:"0 < B"
and eq_U:"⋀x. B ≤ x ⟹ U x = c x * exp (∫t∈{B<..x}. r t / t ∂lborel)"
and integ:"⋀x. B ≤ x ⟹ set_integrable lborel {B<..x} (λt. r t / t)"
and lim_r:"(r ⤏ ρ) at_top"
and lim_c:"(c ⤏ C) at_top"
and C_pos:"0 < C"
by blast
obtain T1 where T1:"⋀t. T1 ≤ t ⟹ r t ≤ ρ + d" "⋀t. T1 ≤ t ⟹ ρ - d ≤ r t"
using tendstoD[OF lim_r d] unfolding eventually_at_top_linorder dist_real_def
by (metis abs_diff_le_iff less_eq_real_def)
have pos:"C * (A - 1) / (A + 1) > 0"
using A C_pos by fastforce
obtain T2 where "⋀t. T2 ≤ t ⟹ ¦c t - C¦ ≤ C * (A - 1) / (A + 1)"
using tendstoD[OF lim_c pos] unfolding eventually_at_top_linorder dist_real_def
by fastforce
hence T2':"C - C * (A - 1) / (A + 1) ≤ c t" "c t ≤ C + C * (A - 1) / (A + 1)"
if t:"T2 ≤ t" for t
using t by(auto simp: abs_diff_le_iff)
have ct_pos:"0 < c t" if t:"T2 ≤ t" for t
using T2'[OF t] C_pos A
by (smt (verit, ccfv_threshold) mult.commute le_divide_eq le_divide_eq_1
nonzero_mult_divide_mult_cancel_left2)
have T2:"c y / c x ≤ A" if x:"T2 ≤ x" and y:"T2 ≤ y" for x y
proof -
have "c y / c x ≤ (C + C * (A - 1) / (A + 1)) / (C - C * (A - 1) / (A + 1))"
using T2'[OF x] T2'[OF y] ct_pos[OF y] C_pos A
by(auto intro!: divide_mono simp del: times_divide_eq_right
simp: times_divide_eq_right[symmetric])
also have "... = (C * (1 + (A - 1) / (A + 1))) / (C * (1 - (A - 1) / (A + 1)))"
by (simp add: distrib_left right_diff_distrib')
also have "... = (C * ((A + 1) / (A + 1) + (A - 1) / (A + 1)))
/ (C * ((A + 1) / (A + 1) - (A - 1) / (A + 1)))"
using A by simp
also have "... = A"
unfolding add_divide_distrib[symmetric] diff_divide_distrib[symmetric]
using C_pos A by simp
finally show ?thesis .
qed
define T where "T ≡ max (max 1 B) (max T1 T2)"
have T_pos: "0 < T" and TB:"B ≤ T"
and Tr1:"⋀t. T ≤ t ⟹ r t ≤ ρ + d" and Tr2:"⋀t. T ≤ t ⟹ ρ - d ≤ r t"
and Tc:"⋀x y. T ≤ x ⟹ T ≤ y ⟹ c y / c x ≤ A"
using T1 T2 by(auto simp: T_def)
have 1:"U y / U x ≤ A * (y / x) powr (ρ + d)" if x:"T ≤ x" and xy:"x ≤ y" for x y
proof -
have y:"T ≤ y"
using x xy by simp
have "U y / U x = c y * exp (∫t∈{B<..y}. r t / t ∂lborel)
/ (c x * exp (∫t∈{B<..x}. r t / t ∂lborel))"
using x y eq_U TB by simp
also have "... = (c y / c x)
* exp ((∫t∈{B<..y}. r t / t ∂lborel) - (∫t∈{B<..x}. r t / t ∂lborel))"
by (simp add: exp_diff)
also have "... ≤ A * exp ((∫t∈{B<..y}. r t / t ∂lborel) - (∫t∈{B<..x}. r t / t ∂lborel))"
using Tc[OF x y] A by(intro mult_mono) auto
also have "... = A * exp ((∫t. indicat_real {B<..y} t * r t / t
- indicat_real {B<..x} t * r t / t ∂lborel))"
using integ[of x] integ[of y] TB x y A
by(auto simp: set_lebesgue_integral_def set_integrable_def)
also have "... = A * exp ((∫t∈{x<..y}. r t / t ∂lborel))"
using x y TB xy by(auto intro!: Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def)
also have "... ≤ A * exp ((∫t∈{x<..y}. (ρ + d) / t ∂lborel))"
using A x TB T_pos Tr1 y
by(auto intro!: set_integral_mono set_integrable_subset[OF integ[of y]]
set_integrable_inverse' divide_right_mono)
also have "... = A * exp ((ρ + d) * ln (y / x))"
using x y xy T_pos
by(subst set_integral_inverse) (auto simp: ln_divide_pos)
also have "... = A * (y / x) powr (ρ + d)"
using x y T_pos by(simp add: powr_def)
finally show ?thesis .
qed
have 2:"U y / U x ≤ A * (y / x) powr (ρ - d)" if yx:"y ≤ x" and y:"T ≤ y" for x y
proof -
have x:"T ≤ x"
using yx y by simp
have "U y / U x = c y * exp (∫t∈{B<..y}. r t / t ∂lborel)
/ (c x * exp (∫t∈{B<..x}. r t / t ∂lborel))"
using x y eq_U TB by simp
also have "... = (c y / c x)
* exp ((∫t∈{B<..y}. r t / t ∂lborel) - (∫t∈{B<..x}. r t / t ∂lborel))"
by (simp add: exp_diff)
also have "... ≤ A * exp ((∫t∈{B<..y}. r t / t ∂lborel) - (∫t∈{B<..x}. r t / t ∂lborel))"
using Tc[OF x y] A by(intro mult_mono) auto
also have "... = A * exp ((∫t. indicat_real {B<..y} t * r t / t
- indicat_real {B<..x} t * r t / t ∂lborel))"
using integ[of x] integ[of y] TB x y A
by(auto simp: set_lebesgue_integral_def set_integrable_def)
also have "... = A * exp ((∫t∈{y<..x}. - r t / t ∂lborel))"
using x y TB yx A by(auto intro!: Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def simp del: integral_minus)
also have "... ≤ A * exp ((∫t∈{y<..x}. - (ρ - d) / t ∂lborel))"
using A x TB T_pos Tr2 y yx
by(auto intro!: set_integral_mono set_integrable_subset[OF integ[of x]]
set_integrable_inverse' divide_right_mono simp: set_integrable_uminus
simp del: minus_diff_eq)
also have "... = A * exp((ρ - d) * ln (y / x))"
using x y yx T_pos
by(subst set_integral_inverse)
(auto simp: ln_divide_pos left_diff_distrib right_diff_distrib)
also have "... = A * (y / x) powr (ρ - d)"
using x y T_pos by(simp add: powr_def)
finally show ?thesis .
qed
have 3:"U y / U x ≤ A * max ((y / x) powr (ρ + d)) ((y / x) powr (ρ - d))"
if x:"T ≤ x" and y:"T ≤ y" for x y
proof(cases "x ≤ y")
assume xy:"x ≤ y"
then have "U y / U x ≤ A * (y / x) powr (ρ + d)"
using 1 x by blast
thus ?thesis
using T_pos xy d powr_mono x by force
next
assume yx:"¬ x ≤ y"
then have "U y / U x ≤ A * (y / x) powr (ρ - d)"
using 2 y by simp
thus ?thesis
by (smt (verit, best) A mult_mono powr_ge_zero)
qed
show ?g1 ?g2 ?g3
using 1 2 3 T_pos by blast+
qed
corollary
assumes rv:"regularly_varying U ρ"
and A:"A < 1" and d:"0 < d"
shows Potter_bounds_lower1:
"∃T>0. ∀x≥T. ∀y≥x. A * (y / x) powr (ρ - d) ≤ U y / U x" (is ?g1)
and Potter_bounds_lower2:
"∃T>0. ∀y≥T. ∀x≥y. A * (y / x) powr (ρ + d) ≤ U y / U x" (is ?g2)
and Potter_bounds_lower:
"∃T>0. ∀x≥T. ∀y≥T. A * min ((y / x) powr (ρ + d)) ((y / x) powr (ρ - d)) ≤ U y / U x"
(is ?g3)
proof -
show g1:?g1
proof(cases "A ≤ 0")
assume "A ≤ 0"
thus ?thesis
by (smt (verit, best) divide_pos_pos mult_cancel_right2 mult_less_cancel_left
powr_non_neg regularly_varying_pos rv)
next
assume A_pos:"¬ A ≤ 0"
then have invA:"1 < 1 / A"
using A by force
from Potter_bounds2[OF rv this d]
obtain T where T_pos:"T > 0" and T:"⋀x y. y ≥ T ⟹ x ≥ y ⟹
U y / U x ≤ 1 / A * (y / x) powr (ρ - d)"
by fast
have "A * (y / x) powr (ρ - d) ≤ U y / U x" if x:"T ≤ x" and xy:"x ≤ y" for x y
proof -
have "1 / (1 / A * (x / y) powr (ρ - d)) ≤ 1 / (U x / U y)"
using A_pos regularly_varying_pos[OF rv] T_pos x xy
by(intro divide_left_mono T[OF x xy] T[OF x xy]) auto
thus ?thesis
by (simp add: powr_divide)
qed
thus ?thesis
using T_pos by blast
qed
show g2:?g2
proof(cases "A ≤ 0")
assume "A ≤ 0"
thus ?thesis
by (smt (verit, best) divide_pos_pos mult_cancel_right2 mult_less_cancel_left
powr_non_neg regularly_varying_pos rv)
next
assume A_pos:"¬ A ≤ 0"
then have invA:"1 < 1 / A"
using A by force
from Potter_bounds1[OF rv this d]
obtain T where T_pos:"T > 0" and T:"⋀x y. x ≥ T ⟹ y ≥ x ⟹
U y / U x ≤ 1 / A * (y / x) powr (ρ + d)"
by fast
have "A * (y / x) powr (ρ + d) ≤ U y / U x" if y:"T ≤ y" and yx:"y ≤ x" for x y
proof -
have "1 / (1 / A * (x / y) powr (ρ + d)) ≤ 1 / (U x / U y)"
using A_pos regularly_varying_pos[OF rv] T_pos y yx
by(intro divide_left_mono T[OF y yx]) auto
thus ?thesis
by (simp add: powr_divide)
qed
thus ?thesis
using T_pos by blast
qed
from g1 g2 obtain T1 T2 where
T1:"T1 > 0" "∀x≥T1. ∀y≥x. A * (y / x) powr (ρ - d) ≤ U y / U x"
and T2:"T2 > 0" "∀y≥T2. ∀x≥y. A * (y / x) powr (ρ + d) ≤ U y / U x"
by auto
thus ?g3
by(safe intro!: exI[where x="max T1 T2"] max.strict_coboundedI1)
(smt (verit, best) assms(3) divide_pos_pos less_divide_eq_1_pos powr_less_mono powr_mono')
qed
subsection ‹Karamata's Theorem›
subsubsection ‹Direct Half›
lemma Karamata_theorem_half1:
assumes rv: "regularly_varying U ρ"
and a: "0 ≤ a" and rho:"- 1 < ρ"
and integrable:"⋀c d. a ≤ c ⟹ set_integrable lborel {c<..d} U"
shows "((λt. (∫x∈{a<..t}. U x ∂lborel) / (t * U t)) ⤏ 1 / (ρ + 1)) at_top"
proof -
obtain d where d_pos:"0 < d" and d:"d < ρ + 1"
by (metis rho minus_less_iff real_0_less_add_iff real_arch_inverse)
with Potter_bounds2[OF rv,of 2 d]
obtain T' where T':"T' > 0" "⋀x y. T' ≤ y ⟹ y ≤ x ⟹ U y / U x ≤ 2 * (y / x) powr (ρ - d)"
by auto
define T where "T ≡ max T' a"
have T_pos:"0 < T" and aT:"a ≤ T"
and T:"⋀x y. T ≤ y ⟹ y ≤ x ⟹ U y / U x ≤ 2 * (y / x) powr (ρ - d)"
using T' by(auto simp: T_def)
have eq:"(∫x∈{T<..t}. U x ∂lborel) / (t * U t) = (∫s∈{T/t<..1}. U (t * s) / U t ∂lborel)"
if t:"T ≤ t" for t
proof -
have "(∫x∈{T<..t}. U x ∂lborel) = t * (∫s. indicat_real {T<..t} (t * s) *⇩R U (t * s) ∂lborel)"
using lborel_integral_real_affine[of t "λx. indicat_real {T<..t} x * U x" 0] T_pos t
by(auto simp: set_lebesgue_integral_def)
also have "... = t * (∫s∈{T/t<..1}. U (t * s) ∂lborel)"
unfolding set_lebesgue_integral_def using T_pos t
by(intro arg_cong[where f="(*) t"]
Bochner_Integration.integral_cong arg_cong[where f="λy. y *⇩R U (t * _)"])
(auto simp: mult.commute indicator_def pos_divide_less_eq)
finally show ?thesis
using T_pos t by simp
qed
have "set_integrable lborel {T/t<..1} (λs. U (t * s) / U t)"
if t:"T < t" for t
proof -
have *:"indicat_real {T<..t} (t * x) = indicat_real {T/t<..1} x" for x
using T_pos t by(auto simp: indicator_def divide_less_eq mult.commute)
have "integrable lborel (λx. indicat_real {T<..t} (t * x) * U (t * x))"
using lborel_integrable_real_affine[of "λx. indicat_real {T<..t} x * U x" t 0]
T_pos aT integrable[of T t] t
by(auto simp: set_integrable_def)
thus ?thesis
unfolding * by(simp add: set_integrable_def)
qed
hence *:"(λs. indicat_real {T/t<..1} s * U (t * s) / U t) ∈ borel_measurable lborel"
if t:"T + 1 ≤ t" for t
using t T_pos by(auto simp: set_integrable_def)
have **:"integrable lborel (λs. indicator {0<..1} s * 2 * s powr (ρ - d))"
using d set_integrable_mult_right_iff[THEN iffD2,OF _ set_integrable_powr_from_0[of "ρ - d"]]
by(auto simp: set_integrable_def mult.assoc)
have ***:"AE s in lborel.
((λt. indicat_real {T/t<..1} s * U (t * s) / U t)
⤏ indicat_real {0<..1} s * s powr ρ) at_top"
proof(rule AE_I2)
fix s :: real
consider "0 < s" "s ≤ 1" | "s ≤ 0" | "1 < s"
by linarith
then show "((λt. indicat_real {T / t<..1} s * U (t * s) / U t)
⤏ indicat_real {0<..1} s * s powr ρ) at_top"
proof cases
assume s:"0 < s" "s ≤ 1"
then obtain X where X:"0 < X" "T / X < s"
by (metis linordered_field_no_ub mult.commute not_less_iff_gr_or_eq order.strict_trans
pos_divide_less_eq)
hence "⋀t. X ≤ t ⟹ T / t < s"
by (metis T_pos order.strict_trans frac_less2 less_eq_real_def)
hence "∀⇩F t in at_top. indicat_real {T / t<..1} s * U (t * s) / U t = U (t * s) / U t"
using s by(auto intro!: eventually_at_top_linorderI[where c=X])
moreover have "((λt. U (t * s) / U t) ⤏ indicat_real {0<..1} s * s powr ρ) at_top"
using regularly_varying_lim[OF rv] s
by(simp add: indicator_def)
ultimately show ?thesis
by(simp only: tendsto_cong)
next
assume s:"s ≤ 0"
hence "∀⇩F t in at_top. indicat_real {T / t<..1} s * U (t * s) / U t = 0"
by(intro eventually_at_top_linorderI[where c=1])
(simp add: linorder_class.not_less[of "T / _" s]
T_pos dual_order.trans[of "0" "T / _" s]
less_eq_real_def[of "0"])
thus ?thesis
using s by (simp add: tendsto_eventually)
qed simp
qed
have ****:"AE x in lborel. norm (indicat_real {T / t<..1} x * U (t * x) / U t)
≤ indicat_real {0<..1} x * 2 * x powr (ρ - d)"
if t:"T + 1 ≤ t" for t
proof(rule AE_I2)
fix s::real
consider "T / t < s" "s ≤ 1" | "s ≤ T / t" | "1 < s"
by linarith
then show "norm (indicat_real {T / t<..1} s * U (t * s) / U t)
≤ indicat_real {0<..1} s * 2 * s powr (ρ - d)"
proof cases
assume s:"T / t < s" "s ≤ 1"
then have Tts:"T ≤ t * s" "t * s ≤ t" and s_pos:"s > 0"
using t T_pos by(auto simp: mult.commute pos_divide_less_eq
order.strict_trans[of 0 "T / t" s])
have "norm (indicat_real {T / t<..1} s * U (t * s) / U t)
= U (t * s) / U t"
using s T_pos t s_pos
by(auto simp del: abs_divide intro!: abs_of_pos
regularly_varying_pos[OF rv] divide_pos_pos)
also have "... ≤ indicat_real {0<..1} s * 2 * s powr (ρ - d)"
using s_pos T[OF Tts] t s T_pos by auto
finally show ?thesis .
qed auto
qed
have lim:"((λt. (∫s∈{T/t<..1}. U (t * s) / U t ∂lborel))
⤏ (∫s∈{0<..1}. s powr ρ ∂lborel)) at_top"
using integral_dominated_convergence_real[OF _ * ** *** ****]
by(auto simp: set_lebesgue_integral_def)
have cong:"∀⇩F t in at_top.
(∫x∈{a<..t}. U x ∂lborel) / (t * U t)
= (∫x∈{a<..T}. U x ∂lborel)/ (t * U t) + (∫s∈{T/t<..1}. U (t * s) / U t ∂lborel)"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
with aT have "(∫x∈{a<..t}. U x ∂lborel) = (∫x∈{a<..T} ∪ {T<..t}. U x ∂lborel)"
by(intro arg_cong[where f="λB. set_lebesgue_integral lborel B _"]) auto
also have "... = (∫x∈{a<..T}. U x ∂lborel) + (∫x∈{T<..t}. U x ∂lborel)"
by(intro set_integral_Un integrable aT) auto
finally show "(∫x∈{a<..t}. U x ∂lborel) / (t * U t)
= (∫x∈{a<..T}. U x ∂lborel)/ (t * U t) + (∫s∈{T/t<..1}. U (t * s) / U t ∂lborel)"
by(simp add: add_divide_distrib eq[OF t])
qed
have lim2:"((λt. (∫x∈{a<..T}. U x ∂lborel)/ (t * U t)
+ (∫s∈{T/t<..1}. U (t * s) / U t ∂lborel))
⤏ 0 + 1 / (ρ + 1)) at_top"
using rho lim set_integral_powr_from_0
by(intro tendsto_add real_tendsto_divide_at_top
regularly_varying_pos_at_top[where ρ="1 + ρ"] regularly_varying_mult rv)
auto
show ?thesis
using lim2 cong tendsto_cong
by fastforce
qed
lemma Karamata_theorem_half_uminus1:
assumes rv:"regularly_varying U (- 1)"
and a: "0 ≤ a"
and integrable:"⋀c d. a ≤ c ⟹ set_integrable lborel {c<..d} U"
shows "filterlim (λt. (∫x∈{a<..t}. U x ∂lborel) / (t * U t)) at_top at_top"
unfolding filterlim_at_top
proof safe
fix Z :: real
define Z' where "Z' ≡ max (Z + 1) 2"
define c where "c ≡ exp (- Z')"
have c_pos:"0 < c" and c_1:"c < 1"
by (simp_all add: c_def Z'_def)
obtain T1 where T1:"⋀t. T1 ≤ t ⟹ a ≤ c * t"
by (metis mult.commute c_pos pos_divide_le_eq)
obtain T2 where T2:"⋀t x. T2 ≤ t ⟹ c ≤ x ⟹ x ≤ 1
⟹ ¦U (t * x) / U t - x powr (- 1)¦ < 1"
using uniform_limitD[OF regularly_varying_UCT_interval[OF rv c_pos,of 1],of 1]
by(fastforce simp: eventually_at_top_linorder dist_real_def )
define T where "T ≡ max 1 (max T1 T2)"
have Tact:"⋀t. T ≤ t ⟹ a ≤ c * t"
by(auto simp: T_def intro!: T1)
have Tle:"⋀t x. T ≤ t ⟹ c ≤ x ⟹ x ≤ 1 ⟹ 1 / x - 1 ≤ U (t * x) / U t"
using T2 T_def c_pos by fastforce
show "∀⇩F t in at_top. Z ≤ (∫x∈{a<..t}. U x ∂lborel) / (t * U t)"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
then have t_pos:"0 < t"
by(simp add: T_def)
have integ1[simp]:"set_integrable lborel {c * t<..t} U"
by(auto intro!: assms Tact[OF t])
have integ2[simp]:"set_integrable lborel {c<..1} (λx. U (t * x) / U t)"
proof -
have *:"indicat_real {c * t<..t} (t * x) = indicat_real {c<..1} x" for x
using t_pos by(auto simp: indicator_def divide_less_eq mult.commute)
have "integrable lborel (λx. indicat_real {c * t<..t} (t * x) * U (t * x))"
using lborel_integrable_real_affine[of "λx. indicat_real {c * t<..t} x * U x" t 0]
integ1 t_pos
unfolding set_integrable_def
by simp
thus ?thesis
unfolding * by(simp add: set_integrable_def)
qed
note [simp] = set_integral_diff[OF set_integrable_inverse'[OF c_pos]
set_integrable_const[of lborel "{c<..1}"]]
have "Z ≤ Z' - 1"
by(simp add: Z'_def)
also have "... = - ln c - 1"
by(simp add: c_def)
also have "... ≤ - ln c - (1 - c)"
using c_1 c_pos by argo
also have "... = (∫x∈{c<..1}. 1 / x ∂lborel) - (1 - c)"
using c_pos c_1 by(subst set_integral_inverse) auto
also have "... = (∫x∈{c<..1}. 1 / x ∂lborel) - (∫x∈{c<..1}. 1 ∂lborel)"
using c_1 by(subst set_integral_const) auto
also have "... = (∫x∈{c<..1}. 1 / x - 1 ∂lborel)"
using c_1 by auto
also have "... ≤ (∫x∈{c<..1}. U (t * x) / U t ∂lborel)"
using t c_1 by(intro set_integral_mono Tle) auto
also have "... = (∫x∈{c * t<..t}. U x ∂lborel) / (t * U t)"
proof -
have "(∫x∈{c * t<..t}. U x ∂lborel)
= t * (∫s. indicat_real {c * t<..t} (t * s) *⇩R U (t * s) ∂lborel)"
using lborel_integral_real_affine[of t "λx. indicat_real {c*t<..t} x * U x" 0] t_pos
by(auto simp: set_lebesgue_integral_def)
also have "... = t * (∫s∈{c<..1}. U (t * s) ∂lborel)"
unfolding set_lebesgue_integral_def using t_pos
by(intro arg_cong[where f="(*) t"]
Bochner_Integration.integral_cong arg_cong[where f="λy. y *⇩R U (t * _)"])
(auto simp: mult.commute indicator_def pos_divide_less_eq)
finally show ?thesis
using t_pos by simp
qed
also have "... ≤ (∫x∈{a<..t}. U x ∂lborel) / (t * U t)"
using t_pos less_imp_le[OF regularly_varying_pos[OF rv]]
integrable[OF order.refl] Tact[OF t] a
by(intro divide_right_mono set_integral_subset) auto
finally show "Z ≤ (∫x∈{a<..t}. U x ∂lborel) / (t * U t)" .
qed
qed
corollary Karamata_theorem_half1_inverse:
assumes rv: "regularly_varying U ρ"
and rho:"- 1 ≤ ρ" and a: "0 ≤ a"
and integrable:"⋀c d. a ≤ c ⟹ set_integrable lborel {c<..d} U"
shows "((λt. (t * U t) / (∫x∈{a<..t}. U x ∂lborel)) ⤏ ρ + 1) at_top"
proof(cases "ρ = -1")
show "ρ = -1 ⟹ ?thesis"
using tendsto_inverse_0_at_top[OF Karamata_theorem_half_uminus1[OF _ a integrable]] rv
by simp
qed(use assms tendsto_inverse[OF Karamata_theorem_half1] in auto)
lemma Karamata_theorem_half1_ex:
assumes rv: "regularly_varying U ρ"
and rho:"- 1 ≤ ρ"
shows "∃a. ((λt. (t * U t) / (∫x∈{a<..t}. U x ∂lborel)) ⤏ ρ + 1) at_top"
proof -
from regularly_varying_eventually_locally_integrable[OF rv]
obtain x' where x':"⋀a b. x' ≤ a ⟹ set_integrable lborel {a..b} U"
by (metis (lifting) eventually_at_top_linorder)
define x where "x ≡ max 0 x'"
have x:"0 ≤ x" "⋀c d. x ≤ c ⟹ set_integrable lborel {c<..d} U"
by(auto intro!: set_integrable_subset[where A="{_.._}" and B="{_<.._}"] x' simp: x_def)
from Karamata_theorem_half1_inverse[OF rv rho this]
show ?thesis
by fast
qed
lemma regularly_varying_integral_limit:
assumes rv: "regularly_varying U ρ"
and rho:"- 1 ≤ ρ" and a: "0 ≤ a"
and integrable:"⋀c d. a ≤ c ⟹ set_integrable lborel {c<..d} U"
and x: "0 < x"
shows "((λt. (∫s∈{a<..t * x}. U s ∂lborel) / (∫s∈{a<..t}. U s ∂lborel))
⤏ x powr (ρ + 1)) at_top"
(is "(?g ⤏ x powr (ρ + 1)) at_top")
proof(cases "ρ = -1")
assume "ρ ≠ - 1"
then have rho':"- 1 < ρ"
using rho by force
have "(λt. (∫s∈{a<..t * x}. U s ∂lborel) / (∫s∈{a<..t}. U s ∂lborel)) ∼[at_top]
(λt. (t * x * U (t * x)) / (t * U t))"
using asymp_equiv_divide[OF asymp_equivI'_const[OF
filterlim_compose[OF Karamata_theorem_half1[OF rv a rho' integrable]
filterlim_tendsto_pos_mult_at_top[OF tendsto_const x filterlim_ident]]]
asymp_equivI'_const[OF Karamata_theorem_half1[OF rv a rho' integrable]]] rho'
by(simp add: mult.commute)
moreover have "(λt. (t * x * U (t * x)) / (t * U t))
∼[at_top] (λt. (x * (U (t * x)) / U t))"
using x regularly_varying_pos[OF rv] regularly_varying_pos[OF rv mult_pos_pos[OF _ x]]
by(intro asymp_equivI' tendstoI eventually_at_top_linorderI[where c=1])
(smt (verit, ccfv_threshold) dist_real_def divide_divide_eq_right
divide_divide_times_eq divide_eq_1_iff nonzero_mult_div_cancel_left)
ultimately have "(λt. (∫s∈{a<..t * x}. U s ∂lborel) / (∫s∈{a<..t}. U s ∂lborel))
∼[at_top] (λt. (x * (U (t * x)) / U t))"
using asymp_equiv_trans by blast
moreover have "((λt. (x * (U (t * x)) / U t)) ⤏ x powr (ρ + 1)) at_top"
using tendsto_mult[OF tendsto_const[of x] regularly_varying_lim[OF rv x]]
powr_mult_base' x
by (simp add: add.commute powr_mult_base)
ultimately show ?thesis
using tendsto_asymp_equiv_cong by blast
next
assume rho':"ρ = - 1"
show ?thesis
proof(cases "set_integrable lborel {a<..} U")
assume h:"set_integrable lborel {a<..} U"
then have *:"((λt. (∫s∈{a<..t}. U s ∂lborel)) ⤏ (∫s∈{a<..}. U s ∂lborel)) at_top"
using a
by(intro interval_integral_inf2 less_imp_le[OF regularly_varying_pos[OF rv]]
set_integrable_subset[OF h])
auto
have "0 < (∫s∈{a<..}. U s ∂lborel)"
using a
by(auto intro!: set_integral_zero_less h regularly_varying_pos[OF rv]
order.strict_trans2[where b="emeasure lborel {a<..a+1}" and c="emeasure lborel {a<..}",
OF _ emeasure_mono])
thus ?thesis
using tendsto_divide[OF filterlim_compose[OF
* filterlim_tendsto_pos_mult_at_top[OF tendsto_const x filterlim_ident]]
*] x
by(simp add: mult.commute rho')
next
assume h:"¬ set_integrable lborel {a<..} U"
have integ_infa:"(∫⇧+s∈{a<..}. ennreal (U s) ∂lborel) = ⊤"
proof -
have "¬ (∫⇧+ x. ennreal ¦indicat_real {a<..} x * U x¦ ∂lborel) < ∞"
using h regularly_varying_meas_o[OF rv a]
by(auto simp: set_integrable_def integrable_iff_bounded)
moreover have "(∫⇧+ x. ennreal ¦indicat_real {a<..} x * U x¦ ∂lborel)
= (∫⇧+s∈{a<..}. U s ∂lborel)"
using a regularly_varying_pos[OF rv]
by(auto intro!: nn_integral_cong simp: indicator_def abs_of_pos)
ultimately show ?thesis
using top.not_eq_extremum by fastforce
qed
have filterlim1:"filterlim (λt. (∫s∈{a<..t}. U s ∂lborel)) at_top at_top"
proof -
have 1:"∀⇩F t in at_top.
ennreal (∫s∈{a<..t}. U s ∂lborel) = (∫⇧+s∈{a<..t}. ennreal (U s) ∂lborel)"
using integrable[OF order.refl] a
unfolding nn_integral_set_ennreal set_lebesgue_integral_def
apply(intro eventually_at_top_linorderI[where c="a + 1"])
by(subst nn_integral_eq_integral)
(auto simp: set_integrable_def mult.commute indicator_def
less_imp_le[OF regularly_varying_pos[OF rv]])
have 2:"((λt. (∫⇧+s∈{a<..t}. ennreal (U s) ∂lborel))
⤏ (∫⇧+s∈{a<..}. ennreal (U s) ∂lborel)) at_top"
proof(rule nn_integral_at_top_real[where K="0"])
show "mono_on {0..} (λr x. ennreal (U x) * indicator {a<..r} x)"
by(auto intro!: mono_onI le_funI simp: indicator_def)
next
show "⋀t. (λx. ennreal (U x) * indicator {a<..t} x) ∈ borel_measurable lborel"
using regularly_varying_meas_Ioc_ennreal[OF rv a] by simp
next
fix y
show "((λt. ennreal (U y) * indicator {a<..t} y) ⤏
ennreal (U y) * indicator {a<..} y) at_top"
proof(cases "a < y")
assume "a < y"
then obtain T where "⋀t. T ≤ t ⟹ y ≤ t"
by simp
thus ?thesis
unfolding mult.commute[where a="ennreal (U y)"] indicator_mult_ennreal
by(intro tendsto_ennrealI tendstoI eventually_at_top_linorderI[where c=T])
(auto simp: dist_real_def indicator_def)
qed simp
qed
show ?thesis
unfolding ennreal_tendsto_top_eq_at_top[symmetric]
using 1 2 integ_infa
by (simp add: tendsto_cong)
qed
have filterlim2:"filterlim (λt. (∫s∈{X<..t}. U s ∂lborel)) at_top at_top"
if X:"a ≤ X" for X
proof -
have "∀⇩F t in at_top. (∫s∈{a<..t}. U s ∂lborel)
= (∫s∈{a<..X}. U s ∂lborel) + (∫s∈{X<..t}. U s ∂lborel)"
using X unfolding eventually_at_top_linorder
by(subst set_integral_Un[symmetric])
(auto intro!: integrable arg_cong[where f="λB. (∫s∈B. U s ∂lborel)"] exI[where x=X])
hence "∀⇩F t in at_top. (∫s∈{X<..t}. U s ∂lborel)
= - (∫s∈{a<..X}. U s ∂lborel) + (∫s∈{a<..t}. U s ∂lborel)"
by (rule eventually_mono) simp
moreover have "filterlim (λt. - (∫s∈{a<..X}. U s ∂lborel) + (∫s∈{a<..t}. U s ∂lborel))
at_top at_top"
by(subst filterlim_tendsto_add_at_top_iff)
(auto simp: filterlim1)
ultimately show ?thesis
by(simp add: filterlim_cong)
qed
have integ_pos:"⋀b c. a ≤ b ⟹ b < c ⟹ 0 < (∫s∈{b<..c}. U s ∂lborel)"
using a
by(intro set_integral_zero_less set_integrable_subset[OF integrable])
(auto intro!: regularly_varying_pos[OF rv])
have integ_le_0:"∀⇩F t in at_top. 0 < (∫s∈{X<..t}. U s ∂lborel)" if X:"a ≤ X" for X
using filterlim_at_top_dense[THEN iffD1,OF filterlim2[OF X]]
by fast
have asymp_eq:"(λt. (∫s∈{a<..t}. U s ∂lborel)) ∼[at_top] (λt. ∫s∈{X<..t}. U s ∂lborel)"
if X:"a ≤ X" for X
proof -
have "∀⇩F t in at_top. (∫s∈{a<..t}. U s ∂lborel)
= (∫s∈{a<..X}. U s ∂lborel) + (∫s∈{X<..t}. U s ∂lborel)"
using X unfolding eventually_at_top_linorder
by(subst set_integral_Un[symmetric])
(auto intro!: integrable arg_cong[where f="λB. (∫s∈B. U s ∂lborel)"] exI[where x=X])
hence "∀⇩F t in at_top. (∫s∈{a<..t}. U s ∂lborel) / (∫s∈{X<..t}. U s ∂lborel)
= (∫s∈{a<..X}. U s ∂lborel) / (∫s∈{X<..t}. U s ∂lborel) + 1"
by(rule eventually_mono[OF eventually_conj[OF integ_le_0[OF X]]])
(use filterlim_at_top[THEN iffD1,OF filterlim2[OF X]]
in "simp add: add_divide_distrib")
moreover have "((λt. (∫s∈{a<..X}. U s ∂lborel) / (∫s∈{X<..t}. U s ∂lborel) + 1)
⤏ 0 + 1) at_top"
by(intro tendsto_add real_tendsto_divide_at_top filterlim2 X) auto
ultimately show ?thesis
by(auto intro!: asymp_equivI' simp: tendsto_cong)
qed
have asymp_eq':"(λt. (∫s∈{a<..t * x}. U s ∂lborel))
∼[at_top] (λt. ∫s∈{X<..t * x}. U s ∂lborel)"
if X:"a ≤ X" for X
using filterlim_tendsto_pos_mult_at_top[OF tendsto_const x filterlim_ident]
by(intro asymp_equiv_compose'[OF asymp_eq] X)
(simp add: mult.commute)
have le1:"1
≤ Liminf at_top (λt. ereal (?g t))
+ ereal e"
and le2:"Limsup at_top (λt. ereal (?g t))
≤ 1 + ereal e"
if e:"0 < e" for e
proof -
define e' where "e' ≡ e / x"
have e':"0 < e'"
using e x by(simp add: e'_def)
obtain T' where T':"⋀t. T' ≤ t ⟹ ¦U (t * x) / U t - 1 / x¦ < e'"
using tendstoD[OF regularly_varying_lim[OF rv x] e'] x
by(auto simp: rho' eventually_at_top_linorder dist_real_def)
define T where "T ≡ max 1 (max (a + 1) (max (a / x) T'))"
have T_pos:"0 < T" and aT2:"a + 1 ≤ T" and TT':"T' ≤ T" and "a / x ≤ T"
using x by(auto simp: T_def)
hence aTx:"a ≤ T * x" and aT1:"a ≤ T"
using x a pos_divide_le_eq by auto
have T1:"T ≤ t ⟹ U (t * x) ≤ U t * (1 / x + e')" for t
using T'[OF order.trans[OF TT'],of t] T_pos regularly_varying_pos[OF rv,of t]
by(auto simp: abs_less_iff diff_less_eq add.commute mult.commute pos_divide_less_eq)
have T2:"T ≤ t ⟹ U t * (1 / x - e') ≤ U (t * x)" for t
using T'[OF order.trans[OF TT'],of t] T_pos regularly_varying_pos[OF rv,of t]
by (metis (no_types, lifting) linorder_not_le abs_diff_less_iff dual_order.trans
mult.commute mult_imp_div_pos_less not_less_iff_gr_or_eq)
have integT:"set_integrable lborel {T<..y} (λt. U (t * x))" for y
proof -
have 1:"indicat_real {T * x<..y * x} (s * x) * U (s * x)
= indicat_real {T<..y} s * U (s * x)" for s
using x by(auto simp: indicator_def)
have "integrable lborel (λt. indicat_real {T * x<..y * x} t * U t)"
using integrable[OF aTx] unfolding set_integrable_def by simp
from lborel_integrable_real_affine[where c=x and t=0,OF this] x
have "integrable lborel (λs. indicat_real {T * x<..y * x} (s * x) * U (s * x))"
by(simp add: mult.commute)
thus ?thesis
unfolding 1 by(simp add: set_integrable_def)
qed
have "Limsup at_top (λt. ereal (?g t))
= Limsup at_top (λt. ereal ((∫s∈{T * x<..t * x}. U s ∂lborel)
/ (∫s∈{T<..t}. U s ∂lborel)))"
using aTx aT2 aT1 a T_pos x
by(intro asymp_equiv_Limsup_cong_ereal[OF asymp_equiv_divide[OF asymp_eq'[OF aTx]
asymp_eq[OF aT1]]]
eventually_at_top_linorderI[where c="max (T * x + 1) (T + 1)"]
less_imp_le divide_pos_pos )
(auto intro!: integ_pos order.strict_trans1
[OF aTx mult_less_cancel_right_pos[THEN iffD2,OF x]])
also have "... = Limsup at_top
(λt. ereal (x * (∫s∈{T<..t}. U (s * x) ∂lborel)
/ (∫s∈{T<..t}. U s ∂lborel)))"
proof(intro Limsup_eq eventually_at_top_linorderI[where c="T * x + 1"])
fix y
assume y:"T * x + 1 ≤ y"
have "(∫s∈{T * x<..y * x}. U s ∂lborel)
= x * (∫s. indicat_real {T * x<..y * x} (s * x) * U (s * x) ∂lborel)"
using x unfolding set_lebesgue_integral_def
by(subst lborel_integral_real_affine[of x "λt. indicat_real {T*x<..y*x} t *⇩R U t" 0])
(auto simp: mult.commute)
also have "... = x * (∫s∈{T<..y}. U (s * x) ∂lborel)"
using x
by(auto simp: set_lebesgue_integral_def indicator_def
intro!: Bochner_Integration.integral_cong)
finally show "ereal ((∫s∈{T * x<..y * x}. U s ∂lborel) / (∫s∈{T<..y}. U s ∂lborel))
= ereal (x * (∫s∈{T<..y}. U (s * x) ∂lborel) / (∫s∈{T<..y}. U s ∂lborel))"
by presburger
qed
also have "... ≤ Limsup at_top (λt. ereal (x * (∫s∈{T<..t}. U s * (1 / x + e') ∂lborel)
/ (∫s∈{T<..t}. U s ∂lborel)))"
using x
by(auto intro!: Limsup_mono eventually_at_top_linorderI[where c="T + 1"]
T1 mult_left_mono divide_right_mono set_integral_mono integrable[OF aT1]
less_imp_le[OF integ_pos[OF aT1]] integT
simp del: set_integral_mult_left)
also have "... = Limsup at_top (λt::real. ereal (1 + x * e'))"
using x
by(intro Limsup_eq eventually_mono[OF integ_le_0[OF aT1]])
(simp add: distrib_left[of x])
also have "... = ereal (1 + e)"
using x by(simp add: e'_def Limsup_const)
also have "... = 1 + ereal e"
by simp
finally show "Limsup at_top (λt. ereal (?g t)) ≤ 1 + ereal e" .
have "1 - ereal e = ereal (1 - e)"
by (simp add: one_ereal_def)
also have "... = Liminf at_top (λt::real. ereal (1 - x * e'))"
using x by(simp add: e'_def Liminf_const)
also have "... = Liminf at_top (λt. ereal (x * (∫s∈{T<..t}. U s * (1 / x - e') ∂lborel)
/ (∫s∈{T<..t}. U s ∂lborel)))"
using x e'
by(intro Liminf_eq eventually_mono[OF integ_le_0[OF aT1]])
(simp add: right_diff_distrib[of x])
also have "... ≤ Liminf at_top (λt. ereal (x * (∫s∈{T<..t}. U (s * x) ∂lborel)
/ (∫s∈{T<..t}. U s ∂lborel)))"
using x
by(auto intro!: Liminf_mono eventually_at_top_linorderI[where c="T + 1"]
T2 mult_left_mono divide_right_mono set_integral_mono integrable[OF aT1]
less_imp_le[OF integ_pos[OF aT1]] integT
simp del: set_integral_mult_left)
also have "... = Liminf at_top (λt. ereal ((∫s∈{T * x<..t * x}. U s ∂lborel)
/ (∫s∈{T<..t}. U s ∂lborel)))"
proof(intro Liminf_eq eventually_at_top_linorderI[where c="T * x + 1"])
fix y
assume y:"T * x + 1 ≤ y"
have "(∫s∈{T * x<..y * x}. U s ∂lborel)
= x * (∫s. indicat_real {T * x<..y * x} (s * x) * U (s * x) ∂lborel)"
using x unfolding set_lebesgue_integral_def
by(subst lborel_integral_real_affine
[of x "λt. indicat_real {T*x<..y*x} t *⇩R U t" 0])
(auto simp: mult.commute)
also have "... = x * (∫s∈{T<..y}. U (s * x) ∂lborel)"
using x
by(auto simp: set_lebesgue_integral_def indicator_def
intro!: Bochner_Integration.integral_cong)
finally show "ereal (x * (∫s∈{T<..y}. U (s * x) ∂lborel) / (∫s∈{T<..y}. U s ∂lborel))
= ereal ((∫s∈{T * x<..y * x}. U s ∂lborel) / (∫s∈{T<..y}. U s ∂lborel))"
by presburger
qed
also have "... = Liminf at_top (λt. ereal (?g t))"
using aTx aT2 aT1 a T_pos x
by(intro asymp_equiv_Liminf_cong_ereal[OF asymp_equiv_divide[OF asymp_eq'[OF aTx]
asymp_eq[OF aT1]],symmetric]
eventually_at_top_linorderI[where c="max (T * x + 1) (T + 1)"]
less_imp_le divide_pos_pos)
(auto intro!: integ_pos order.strict_trans1[OF aTx
mult_less_cancel_right_pos[THEN iffD2,OF x]] )
finally
show "1
≤ Liminf at_top (λt. ereal (?g t)) + ereal e"
by (smt (verit, best) ‹1 - ereal e = ereal (1 - e)› add_mono one_ereal_def order.refl
plus_ereal.simps(1))
qed
have le3:"1 ≤ Liminf at_top (λt. ereal (?g t))"
by(rule ereal_le_epsilon2) (intro le1)
moreover have le4:"Limsup at_top (λt. ereal (?g t)) ≤ 1"
by(rule ereal_le_epsilon2) (intro le2)
ultimately
have "Liminf at_top (λt. ereal (?g t)) = ereal 1"
and "Limsup at_top (λt. ereal (?g t)) = ereal 1"
using Liminf_le_Limsup[of at_top]
by (metis (no_types, lifting) one_ereal_def order.antisym order_trans
trivial_limit_at_top_linorder)+
hence "((λt. ereal (?g t)) ⤏ ereal 1) at_top"
by(intro Liminf_eq_Limsup) auto
thus ?thesis
using x by(simp add: rho')
qed
qed
lemma
assumes rv: "regularly_varying U ρ"
and rho:"ρ < - 1"
shows Karamata_theorem_half2:"((λt. (∫x∈{t<..}. U x ∂lborel) / (t * U t))
⤏ - 1 / (ρ + 1)) at_top"
and regularly_varying_tail_integrable:"∃T>0. set_integrable lborel {T<..} U"
proof -
obtain i where i_pos:"0 < i" and i:"ρ + i < -1"
by (metis add_minus_cancel rho dense less_add_same_cancel1)
from Potter_bounds1[OF rv _ i_pos,of 2]
obtain T where T_pos:"0 < T"
and T:"⋀x y. T ≤ x ⟹ x ≤ y
⟹ U y / U x ≤ 2 * (y / x) powr (ρ + i)"
by auto
have *:"(λs. indicat_real {1<..} s * U (t * s) / U t) ∈ borel_measurable lborel"
if t:"T ≤ t" for t
proof -
have [measurable]:"(*) t ∈ restrict_space borel {0<..} →⇩M restrict_space borel {0<..}"
using t T_pos
by(auto intro!: measurable_restrict_space3)
note [measurable] = regularly_varying_meas[OF rv]
have [measurable]:"(λs. U (t * s)) ∈ borel_measurable (restrict_space borel {1<..})"
by(rule measurable_restrict_mono[where A="{0<..}"]) measurable
have "(λs. indicat_real {1<..} s * U (t * s) / U t) =
(λs. if s ∈ {1<..} then U (t * s) / U t else 0)"
by fastforce
also have "... ∈ borel_measurable lborel"
by(intro measurable_restrict_space_iff[THEN iffD1]) auto
finally show ?thesis .
qed
have **: "integrable lborel (λx. indicat_real {1<..} x * 2 * x powr (ρ + i))"
using set_integrable_mult_right_iff[THEN iffD2,OF _ set_integrable_powr_inf[OF i]]
by(simp add: set_integrable_def mult.assoc)
have ***:"AE s in lborel. ((λt. indicat_real {1<..} s * U (t * s) / U t)
⤏ indicat_real {1<..} s * s powr ρ) at_top"
by(auto simp: indicator_def regularly_varying_lim[OF rv])
have ****:"AE s in lborel.
norm (indicat_real {1<..} s * U (t * s) / U t)
≤ indicat_real {1<..} s * 2 * s powr (ρ + i)"
if t:"T ≤ t" for t
proof(rule AE_I2)
fix s
show "norm (indicat_real {1<..} s * U (t * s) / U t)
≤ indicat_real {1<..} s * 2 * s powr (ρ + i)"
proof(cases "1 < s")
assume s:"1 < s"
then have "norm (indicat_real {1<..} s * U (t * s) / U t)
= U (t * s) / U t"
using regularly_varying_pos[OF rv] t T_pos
by(fastforce simp del: abs_divide
intro!: abs_of_pos regularly_varying_pos[OF rv] divide_pos_pos)
also have "... ≤ indicat_real {1<..} s * 2 * s powr (ρ + i)"
using T[OF t,of "t * s"] s T_pos t by auto
finally show ?thesis .
qed simp
qed
have lim:"((λt. (∫x∈{1<..}. U (t * x) / U t ∂lborel)) ⤏ - 1 / (ρ + 1)) at_top"
using integral_dominated_convergence_real[OF _ * ** *** ****]
set_integral_powr_inf[OF rho]
by(auto simp: set_lebesgue_integral_def)
have eq:"∀⇩F t in at_top. (∫x∈{t<..}. U x ∂lborel) / (t * U t)
= (∫x∈{1<..}. U (t * x) / U t ∂lborel)"
proof(rule eventually_at_top_linorderI[where c=1])
fix t :: real
assume t:"1 ≤ t"
have "(∫x∈{t<..}. U x ∂lborel) = t * (∫s. indicat_real {t<..} (t * s) *⇩R U (t * s) ∂lborel)"
using lborel_integral_real_affine[of t "λx. indicat_real {t<..} x * U x" 0] t
by(simp add: set_lebesgue_integral_def)
also have "... = t * (∫x∈{1<..}. U (t * x) ∂lborel)"
using t
by(auto intro!: Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def mult.commute indicator_def pos_divide_less_eq)
finally show "(∫x∈{t<..}. U x ∂lborel) / (t * U t) = (∫x∈{1<..}. U (t * x) / U t ∂lborel)"
using t by simp
qed
show "((λt. (∫x∈{t<..}. U x ∂lborel) / (t * U t)) ⤏ - 1 / (ρ + 1)) at_top"
using lim eq tendsto_cong by fast
have "set_integrable lborel {1<..} (λx. U (t * x) / U t)" if t:"T ≤ t" for t
using ** ****[OF t] t
by(auto intro!: Bochner_Integration.integrable_bound
[where f="λs. indicat_real {1<..} s * 2 * s powr (ρ + i)",OF _ * ]
simp: set_integrable_def)
from this[OF order.refl]
have "integrable lborel (λx. indicat_real {1<..} (x / T) * U x / U T)"
using lborel_integrable_real_affine
[of "λx. indicat_real {1<..} x * U (T * x) / U T" "1 / T" 0]
T_pos by(auto simp: set_integrable_def)
from this[THEN integrable_divide[where y="1 / U T"]] regularly_varying_pos[OF rv T_pos]
have "integrable lborel (λx. indicat_real {1<..} (x / T) * U x)"
by simp
moreover have "indicat_real {1<..} (x / T) * U x = indicat_real {T<..} x * U x" for x
using T_pos regularly_varying_pos[OF rv] by(auto simp: indicator_def)
ultimately have "set_integrable lborel {T<..} U"
by (simp add: set_integrable_def cong: Bochner_Integration.integrable_cong)
thus "∃T>0. set_integrable lborel {T<..} U"
using T_pos by fast
qed
lemma Karamata_theorem_half_uminus2_at_top:
assumes rv: "regularly_varying U (- 1)"
and a:"0 ≤ a"
and integ:"set_integrable lborel {a<..} U"
shows "filterlim (λt. (∫x∈{t<..}. U x ∂lborel) / (t * U t)) at_top at_top"
unfolding filterlim_at_top
proof safe
fix Z :: real
define Z' where "Z' ≡ max (Z + 1) 2"
define A where "A ≡ exp Z'"
have A1:"1 ≤ A"
by(simp add: A_def Z'_def)
obtain T1 where T1:"⋀x t. T1 ≤ t ⟹ 1 ≤ x ⟹ ¦U (t * x) / U t - x powr (- 1)¦ < 1 / A"
using uniform_limitD[OF regularly_varying_neg_UCT[OF rv,of 1],of "1 / A"] A1
by(fastforce simp: eventually_at_top_linorder dist_real_def)
define T where "T ≡ max (max 1 a) T1"
have Tle:"⋀t x. T ≤ t ⟹ 1 ≤ x ⟹ 1 / x - 1 / A ≤ U (t * x) / U t"
using T1 T_def by fastforce
show "∀⇩F t in at_top. Z ≤ (∫x∈{t<..}. U x ∂lborel) / (t * U t)"
proof(rule eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
hence t_pos:"0 < t"
by(simp add: T_def)
have integ1[simp]: "set_integrable lborel {t<..} U"
using t by(auto intro!: set_integrable_subset[OF integ] simp: T_def)
have integ2[simp]:"set_integrable lborel {1<..} (λx. U (t * x) / U t)"
proof -
have *:"indicat_real {t<..} (t * x) = indicat_real {1<..} x" for x
using t_pos by(auto simp: indicator_def divide_less_eq mult.commute)
have "integrable lborel (λx. indicat_real {t<..} (t * x) * U (t * x))"
using lborel_integrable_real_affine[of "λx. indicat_real {t<..} x * U x" t 0]
integ1 t_pos unfolding set_integrable_def
by simp
thus ?thesis
unfolding * by(simp add: set_integrable_def)
qed
have integ3[simp]:"set_integrable lborel {1<..A} (λx. U (t * x) / U t)"
by(auto intro!: set_integrable_subset[OF integ2])
note [simp] = set_integral_diff[OF set_integrable_inverse'[of 1]
set_integrable_const[of lborel "{1<..A}" "1 / A"]]
have "Z ≤ ln A - 1"
by(simp add: A_def Z'_def)
also have "... ≤ ln A - (1 - 1 / A)"
using A1 by simp
also have "... = (∫x∈{1<..A}. 1 / x ∂lborel) - (1 - 1 / A)"
using A1 by(subst set_integral_inverse) auto
also have "... = (∫x∈{1<..A}. 1 / x ∂lborel) - (∫x∈{1<..A}. 1 / A ∂lborel)"
using A1 by(subst set_integral_const) (auto simp: diff_divide_distrib)
also have "... = (∫x∈{1<..A}. 1 / x - 1 / A ∂lborel)"
using A1 by simp
also have "... ≤ (∫x∈{1<..A}. U (t * x) / U t ∂lborel)"
using A1 by(intro set_integral_mono Tle t) auto
also have "... ≤ (∫x∈{1<..}. U (t * x) / U t ∂lborel)"
using t_pos
by(intro set_integral_subset)
(auto intro!: divide_pos_pos less_imp_le[of 0] regularly_varying_pos[OF rv])
also have "... = (∫x∈{t<..}. U x ∂lborel) / (t * U t)"
proof -
have "(∫x∈{t<..}. U x ∂lborel)
= t * (∫s. indicat_real {t<..} (t * s) *⇩R U (t * s) ∂lborel)"
using lborel_integral_real_affine[of t "λx. indicat_real {t<..} x * U x" 0] t_pos
by(simp add: set_lebesgue_integral_def)
also have "... = t * (∫x∈{1<..}. U (t * x) ∂lborel)"
using t_pos
by(auto intro!: Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def mult.commute indicator_def pos_divide_less_eq)
finally show ?thesis
using t_pos by simp
qed
finally show "Z ≤ (∫x∈{t<..}. U x ∂lborel) / (t * U t)" .
qed
qed
corollary Karamata_theorem_half_uminus2:
assumes rv: "regularly_varying U (- 1)"
and a:"0 ≤ a"
and integ:"set_integrable lborel {a<..} U"
shows "((λt. (t * U t) / (∫x∈{t<..}. U x ∂lborel)) ⤏ 0) at_top"
using real_tendsto_divide_at_top[OF tendsto_const[of 1]
Karamata_theorem_half_uminus2_at_top[OF assms]]
by simp
lemma regularly_varying_integral_tail_limit:
assumes rv: "regularly_varying U ρ"
and rho:"ρ < - 1"
and x: "0 < x"
shows "((λt. (∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel))
⤏ x powr (ρ + 1)) at_top"
proof -
have "(λt. (∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel)) ∼[at_top]
(λt. (t * x * U (t * x)) / (t * U t))"
using asymp_equiv_divide[OF asymp_equivI'_const[OF
filterlim_compose[OF Karamata_theorem_half2[OF rv rho]
filterlim_tendsto_pos_mult_at_top[OF tendsto_const x filterlim_ident]]]
asymp_equivI'_const[OF Karamata_theorem_half2[OF rv rho]]] rho
by(simp add: mult.commute)
moreover have "(λt. (t * x * U (t * x)) / (t * U t))
∼[at_top] (λt. (x * (U (t * x)) / U t))"
using x regularly_varying_pos[OF rv] regularly_varying_pos[OF rv mult_pos_pos[OF _ x]]
by(intro asymp_equivI' tendstoI eventually_at_top_linorderI[where c=1])
(smt (verit, ccfv_threshold) dist_real_def divide_divide_eq_right
divide_divide_times_eq divide_eq_1_iff nonzero_mult_div_cancel_left)
ultimately have "(λt. (∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel))
∼[at_top] (λt. (x * (U (t * x)) / U t))"
using asymp_equiv_trans by blast
moreover have "((λt. (x * (U (t * x)) / U t)) ⤏ x powr (ρ + 1)) at_top"
using tendsto_mult[OF tendsto_const[of x] regularly_varying_lim[OF rv x]]
powr_mult_base' x
by (simp add: add.commute powr_mult_base)
ultimately show ?thesis
using tendsto_asymp_equiv_cong by blast
qed
lemma regularly_varying_integral_tail_limit2:
assumes rv: "regularly_varying U (- 1)"
and integ:"set_integrable lborel {a<..} U"
and x:"0 < x"
shows "((λt. (∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel)) ⤏ 1) at_top"
unfolding tendsto_iff eventually_at_top_linorder dist_real_def
proof safe
define a' where "a' ≡ max 1 a"
have a':"0 < a'"
by(simp add: a'_def)
have integ':"⋀t. a' ≤ t ⟹ set_integrable lborel {t<..} U"
by(auto intro!: set_integrable_subset[OF integ] simp: a'_def)
fix e :: real
assume e:"0 < e"
define e' where "e' ≡ e / (2 * x)"
have e':"0 < e'"
using x e by(simp add: e'_def)
obtain T' where T':"⋀t. T' ≤ t ⟹ ¦U (t * x) / U t - 1 / x¦ < e'"
using tendstoD[OF regularly_varying_lim[OF rv x] e'] x
by(auto simp: eventually_at_top_linorder dist_real_def)
define T where "T ≡ max a' (max (a' / x) T')"
have T_pos:"0 < T" and aT2:"a' ≤ T" and TT':"T' ≤ T" and "a' / x ≤ T"
using a' x by(auto simp: T_def)
hence aTx:"a' ≤ T * x" and aT1:"a' ≤ T"
using x a' pos_divide_le_eq by auto
have T1:"T ≤ t ⟹ U (t * x) ≤ U t * (1 / x + e')" for t
using T'[OF order.trans[OF TT'],of t] T_pos regularly_varying_pos[OF rv,of t]
by(auto simp: abs_less_iff diff_less_eq add.commute mult.commute pos_divide_less_eq)
have T2:"T ≤ t ⟹ U t * (1 / x - e') ≤ U (t * x)" for t
using T'[OF order.trans[OF TT'],of t] T_pos regularly_varying_pos[OF rv,of t]
by (metis (no_types, lifting) linorder_not_le abs_diff_less_iff dual_order.trans
mult.commute mult_imp_div_pos_less not_less_iff_gr_or_eq)
have integT:"set_integrable lborel {T<..} (λt. U (t * x))"
proof -
have 1:"indicat_real {T * x<..} (s * x) * U (s * x)
= indicat_real {T<..} s * U (s * x)" for s
using x by(auto simp: indicator_def)
have "integrable lborel (λt. indicat_real {T * x<..} t * U t)"
using integ'[OF aTx] unfolding set_integrable_def by simp
from lborel_integrable_real_affine[where c=x and t=0,OF this] x
have "integrable lborel (λs. indicat_real {T * x<..} (s * x) * U (s * x))"
by(simp add: mult.commute)
thus ?thesis
unfolding 1 by(simp add: set_integrable_def)
qed
show "∃T. ∀t≥T. ¦(∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel) - 1¦ < e"
proof(safe intro!: exI[where x=T])
fix t
assume t:"T ≤ t"
then have t_pos:"0 < t"
using T_pos by simp
have integ_pos[arith]:"0 < (∫s∈{t<..}. U s ∂lborel)"
using t_pos
by(intro set_integral_zero_less integ' order.trans[OF aT1 t] emeasure_mono
order.strict_trans2[of 0 "emeasure lborel {t<..t+1}" "emeasure lborel {t<..}"])
(auto intro!: regularly_varying_pos[OF rv])
have eq:"(∫s∈{t * x<..}. U s ∂lborel) = x * (∫s∈{t<..}. U (s * x) ∂lborel)"
proof -
have "(∫s∈{t * x<..}. U s ∂lborel)
= x * (∫s. indicat_real {t * x<..} (s * x) * U (s * x) ∂lborel)"
using lborel_integral_real_affine[of x "λs. indicat_real {t*x<..} s * U s" 0] x
by(simp add: set_lebesgue_integral_def mult.commute)
also have "... = x * (∫s∈{t<..}. U (s * x) ∂lborel)"
using x t_pos regularly_varying_pos[OF rv]
by(auto simp: set_lebesgue_integral_def indicator_def
intro!: Bochner_Integration.integral_cong)
finally show ?thesis .
qed
have "(∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel)
= x * (∫s∈{t<..}. U (s * x) ∂lborel) / (∫s∈{t<..}. U s ∂lborel)"
by(simp add: eq)
also have "... ≤ x * (∫s∈{t<..}. U s * (1 / x + e') ∂lborel) / (∫s∈{t<..}. U s ∂lborel)"
using x t aT1
by(auto simp del: set_integral_mult_left
intro!: divide_right_mono set_integral_mono set_integrable_subset[OF integT]
set_integrable_mult_left[OF integ'] T1)
also have "... < 1 + e"
using x e by(simp add: distrib_left[of x] e'_def)
finally have *:"(∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel)
< 1 + e" .
have "1 - e < x * (∫s∈{t<..}. U s * (1 / x - e') ∂lborel) / (∫s∈{t<..}. U s ∂lborel)"
using x e by(simp add: right_diff_distrib'[of x] e'_def)
also have "... ≤ x * (∫s∈{t<..}. U (s * x) ∂lborel) / (∫s∈{t<..}. U s ∂lborel)"
using x t aT1
by(auto simp del: set_integral_mult_left
intro!: divide_right_mono set_integral_mono set_integrable_subset[OF integT]
set_integrable_mult_left[OF integ'] T2)
also have "... = (∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel)"
by(simp add: eq)
finally show "¦(∫s∈{t * x<..}. U s ∂lborel) / (∫s∈{t<..}. U s ∂lborel) - 1¦ < e"
using * by linarith
qed
qed
lemma regularly_varying_integral_measurable:
assumes rv: "regularly_varying U ρ"
and a:"0 ≤ a"
shows "(λx. (∫s∈{a<..x}. U s ∂lborel)) ∈ borel_measurable borel"
proof -
define U' where "U' ≡ λx. if x ≤ a then 0 else U x"
have [measurable]:"U' ∈ borel_measurable borel"
unfolding U'_def using regularly_varying_meas[OF rv] a
by(subst measurable_If_restrict_space_iff)
(auto intro!: measurable_restrict_mono[where A="{0<..}" and B="{x. ¬ x ≤ a}"])
have *:"(λx. (∫s∈{a<..x}. U' s ∂lborel)) = (λx. (∫s∈{a<..x}. U s ∂lborel))"
by (auto intro!: set_lebesgue_integral_cong simp: U'_def)
have "(λx. (∫s∈{a<..x}. U' s ∂lborel)) ∈ borel_measurable borel"
unfolding set_lebesgue_integral_def
by measurable auto
thus ?thesis
unfolding * by simp
qed
lemma regularly_varying_tail_integral_measurable:
assumes rv: "regularly_varying U ρ"
shows "(λx. (∫s∈{x<..}. U s ∂lborel)) ∈ borel_measurable (restrict_space borel {0<..})"
proof -
define U' where "U' ≡ λx. if 0 < x then U x else 0"
have [measurable]:"U' ∈ borel_measurable borel"
unfolding U'_def using regularly_varying_meas[OF rv]
by(subst measurable_If_restrict_space_iff)
(auto intro!: measurable_restrict_mono[where A="{0<..}" and B="{x. 0 < x}"])
have "(λx. (∫s∈{x<..}. U' s ∂lborel)) ∈ borel_measurable borel"
unfolding set_lebesgue_integral_def
by measurable auto
hence *:"(λx. (∫s∈{x<..}. U' s ∂lborel)) ∈ borel_measurable (restrict_space borel {0<..})"
using measurable_restrict_space1 by blast
have "⋀x. x ∈ space (restrict_space borel {0<..})
⟹ (∫s∈{x<..}. U' s ∂lborel) = (∫s∈{x<..}. U s ∂lborel)"
by(auto intro!: set_lebesgue_integral_cong simp: U'_def)
from measurable_cong[OF this] *
show ?thesis
by fast
qed
lemma regularly_varying_integral:
assumes rv:"regularly_varying U ρ"
and rho:"- 1 ≤ ρ"
and integrable:"⋀x. set_integrable lborel {0<..x} U"
shows "regularly_varying (λx. (∫t∈{0<..x}. U t ∂lborel)) (ρ + 1)"
using regularly_varying_pos[OF rv]
by(intro regularly_varyingI[OF _ _ regularly_varying_integral_limit] rho
measurable_restrict_space1[OF regularly_varying_integral_measurable[OF rv]]
rv set_integral_zero_less integrable set_integrable_subset[OF integrable])
fastforce+
lemma regularly_varying_tail_integral:
assumes rv:"regularly_varying U ρ"
and rho:"ρ ≤ - 1"
and integrable:"set_integrable lborel {0<..} U"
shows "regularly_varying (λx. (∫t∈{x<..}. U t ∂lborel)) (ρ + 1)"
proof -
have 1:"0 < x ⟹ 0 < (∫t∈{x<..}. U t ∂lborel)" for x
by(intro set_integral_zero_less set_integrable_subset[OF integrable]
order.strict_trans2[of 0 "emeasure lborel {x<..x+1}"
"emeasure lborel {x<..}"] emeasure_mono)
(auto intro!: regularly_varying_pos[OF rv])
consider "ρ < - 1" | "ρ = - 1"
using rho by argo
thus ?thesis
proof cases
assume rho:"ρ = - 1"
show "regularly_varying (λx. set_lebesgue_integral lborel {x<..} U) (ρ + 1)"
using rv 1
by(auto intro!: slowly_varyingI
[OF _ _ regularly_varying_integral_tail_limit2[OF _ integrable]]
regularly_varying_tail_integral_measurable[OF rv] rv simp: rho)
qed(intro regularly_varyingI[OF _ _ regularly_varying_integral_tail_limit]
regularly_varying_tail_integral_measurable[OF rv] rv 1)
qed
subsubsection ‹Converse Half›
lemma
assumes U_pos:"⋀r. 0 < r ⟹ 0 < U r"
and U_meas:"U ∈ borel_measurable (restrict_space borel {0<..})"
and rho:"- 1 < ρ" and a[arith]:"0 ≤ a"
and lim: "((λt. (t * U t) / (∫x∈{a<..t}. U x ∂lborel)) ⤏ ρ + 1) at_top"
shows Karamata_theorem_converse1:"regularly_varying U ρ"
and Karamata_theorem_converse1_integrable:
"⋀c d. a ≤ c ⟹ set_integrable lborel {c..d} U"
proof -
show integrable:"set_integrable lborel {c..d} U" if le:"a ≤ c" for c d
proof -
obtain T where T:"⋀t. T ≤ t ⟹ 0 < t * U t / (∫x∈{a<..t}. U x ∂lborel)"
using order_tendstoD[where a=0,OF lim] rho
by(auto simp: eventually_at_top_linorder)
have [arith]:"a < T"
by(rule ccontr) (use T[of T] in simp)
have "T ≤ t ⟹ 0 < (∫x∈{a<..t}. U x ∂lborel)" for t
using T[of t] U_pos[of t]
by(auto simp: zero_less_divide_iff mult_less_0_iff)
hence "T ≤ t ⟹ set_integrable lborel {a<..t} U" for t
using not_set_integrable_integral_eq by fastforce
hence "T ≤ t ⟹ set_integrable lborel {a..t} U" for t
using set_integrable_Ioc_eq_Icc by blast
thus "set_integrable lborel {c..d} U"
by (metis (mono_tags, opaque_lifting) atLeastAtMost_borel atLeastatMost_subset_iff
le le_cases set_integrable_subset sets_lborel)
qed
let ?F = "λx. (∫t∈{a<..x}. U t ∂lborel)"
define g where "g ≡ λt. (t * U t) / ?F t"
have F_pos[simp]:"a < x ⟹ 0 < ?F x" for x
using U_pos
by(intro set_integral_zero_less set_integrable_subset[OF integrable[of a x]]) auto
obtain b where b[arith]:"a < b"
using linordered_field_no_ub by blast
have lnF_eq: "ln (?F b) + (∫t∈{b<..x}. g t / t ∂lborel) = ln (?F x)"
if x[arith]:"b ≤ x" for x
proof -
have "(∫t∈{b<..x}. g t / t ∂lborel) = (∫t∈{b<..x}. 1 / ?F t * U t ∂lborel)"
using U_pos
by(intro set_integral_cong) (auto simp: g_def)
also have "... = (∫t∈{?F b<..?F x}. 1 / t ∂lborel)"
by(intro set_integral_compose_integral_Ioc U_pos integrable measurable_restrict_space1)
auto
also have "... = ln (?F x) - ln (?F b)"
by(subst set_integral_inverse)
(auto intro!: set_integral_subset set_integrable_subset
[OF integrable[of a x]] less_imp_le[OF U_pos])
finally show ?thesis
by simp
qed
have g_integ:"set_integrable lborel {b<..x} (λt. g t / t)"
if x[arith]:"b ≤ x" for x
proof -
have 1:"set_integrable lborel {b<..x} (λt. 1 / ?F t * U t)"
by(intro set_integrable_compose_integral_Ioc U_pos integrable set_integrable_inverse')
auto
have 2:"⋀t. t ∈ {b<..x} ⟹ 1 / ?F t * U t = g t / t"
by(simp add: g_def)
show ?thesis
using set_integrable_cong[THEN iffD1,OF refl refl 2 1]
by fastforce
qed
define r where "r ≡ λx. g x - 1"
define c where "c ≡ λx. g x * ?F b / b"
define C where "C ≡ (ρ + 1) * ?F b / b"
have 1:"∀x≥b. U x = c x * exp (∫t∈{b<..x}. r t / t ∂lborel)"
proof safe
fix x
assume x[arith]:"b ≤ x"
have [arith]:"0 < ?F x"
by simp
have "U x = g x * ?F x / x"
by(simp add: g_def)
also have "... = g x * exp (- ln x) * exp (ln (?F x))"
by(simp add: ln_inverse[symmetric] divide_real_def)
also have "... = g x * exp (ln (1 / b) - (∫t∈{b<..x}. 1 / t ∂lborel))
* exp (ln (?F b) + (∫t∈{b<..x}. g t / t ∂lborel))"
by(simp add: set_integral_inverse lnF_eq ln_divide_pos)
also have "... = c x * exp ((∫t∈{b<..x}. g t / t ∂lborel) - (∫t∈{b<..x}. 1 / t ∂lborel))"
by(simp add: c_def exp_diff exp_add)
also have "... = c x * exp (∫t∈{b<..x}. r t / t ∂lborel)"
using g_integ[OF x] set_integrable_inverse'
by(auto simp: r_def diff_divide_distrib)
finally show "U x = c x * exp (∫t∈{b<..x}. r t / t ∂lborel)" .
qed
have 2:"∀x≥b. set_integrable lborel {b<..x} (λt. r t / t)"
unfolding r_def diff_divide_distrib
by(intro allI impI set_integral_diff set_integrable_inverse' g_integ) auto
have 3:"(r ⤏ ρ) at_top"
using tendsto_diff[OF lim tendsto_const[where k=1]]
by(simp add: r_def g_def)
have 4:"(c ⤏ C) at_top"
unfolding c_def C_def times_divide_eq_right[symmetric]
by(intro tendsto_mult) (auto simp: g_def lim)
have 5:"0 < C"
using rho by(simp add: C_def)
show "regularly_varying U ρ"
using 1 2 3 4 5
by(subst Karamata_representation_iff[OF U_meas U_pos])
(auto intro!: exI[where x=b,OF conjI
[OF _ exI[where x=c,OF exI[where x=r,OF exI[where x=C]]]]]
simp del: ex_simps)
qed
lemma
assumes U_pos:"⋀r. 0 < r ⟹ 0 < U r"
and U_meas:"U ∈ borel_measurable (restrict_space borel {0<..})"
and rho:"- 1 > ρ"
and lim: "((λt. t * U t / (∫x∈{t<..}. U x ∂lborel)) ⤏ - (ρ + 1)) at_top"
shows Karamata_theorem_converse2:"regularly_varying U ρ"
and Karamata_theorem_converse2_itegrable: "∃a>0. set_integrable lborel {a..} U"
proof -
show "∃a>0. set_integrable lborel {a..} U"
proof -
obtain T' where T':"⋀t. T' ≤ t ⟹ 0 < (t * U t) / (∫x∈{t<..}. U x ∂lborel)"
using order_tendstoD[where a=0,OF lim] rho
by(auto simp: eventually_at_top_linorder)
define a where "a ≡ max T' 1"
have [arith]:"0 < a"
by(simp add: a_def)
have "0 < (∫x∈{a<..}. U x ∂lborel)"
using T'[of a] U_pos[of a]
by(auto simp: a_def zero_less_divide_iff mult_less_0_iff)
thus ?thesis
using not_set_integrable_integral_eq
by(fastforce intro!: exI[where x=a] simp: set_integrable_atLeast_eq[symmetric])
qed
then obtain a where a_pos[arith]:"0 < a"
and integrable:"set_integrable lborel {a..} U"
by blast
let ?F = "λx. (∫t∈{x<..}. U t ∂lborel)"
define g where "g ≡ λx. - x * U x / ?F x"
have F_pos[simp]:"a ≤ x ⟹ 0 < ?F x" for x
using U_pos
by(intro set_integral_zero_less set_integrable_subset[OF integrable]
order.strict_trans2[of 0 "emeasure lborel {x<..x+1}"
"emeasure lborel {x<..}",OF _ emeasure_mono])
auto
have g_integ[simp]:"set_integrable lborel {a<..x} (λt. g t / t)"
if x[arith]:"a ≤ x" for x
proof -
have 1:"set_integrable lborel {a<..x} (λt. - 1 / ?F t * U t)"
by(intro set_integrable_compose_integral_tail[where a=a]
U_pos integrable set_integrable_inverse')
auto
have 2:"⋀t. t ∈ {a<..x} ⟹ - 1 / ?F t * U t = g t / t"
by(simp add: g_def)
show ?thesis
using set_integrable_cong[THEN iffD1,OF refl refl 2 1]
by fastforce
qed
have lnF_eq: "ln (?F a) + (∫t∈{a<..x}. g t / t ∂lborel) = ln (?F x)"
if x[arith]:"a ≤ x" for x
proof -
have "(∫t∈{a<..x}. - g t / t ∂lborel) = (∫t∈{a<..x}. 1 / ?F t * U t ∂lborel)"
using U_pos
by(intro set_integral_cong) (auto simp: g_def)
also have "... = (∫t∈{?F x<..?F a}. 1 / t ∂lborel)"
by(intro set_integral_compose_integral_tail[where a=a]
integrable measurable_restrict_space1 U_pos)
auto
also have "... = ln (?F a) - ln (?F x)"
by(subst set_integral_inverse)
(auto intro!: set_integral_subset set_integrable_subset[OF integrable]
less_imp_le[OF U_pos])
finally show ?thesis
by (simp add: set_integral_uminus)
qed
define r where "r ≡ λx. g x - 1"
define c where "c ≡ λx. - g x * ?F a / a"
define C where "C ≡ - (ρ + 1) * ?F a / a"
have 1:"∀x≥a. U x = c x * exp (∫t∈{a<..x}. r t / t ∂lborel)"
proof safe
fix x
assume x[arith]:"a ≤ x"
have [arith]:"0 < ?F x"
by simp
have "U x = - g x * ?F x / x"
by(simp add: g_def)
also have "... = - g x * exp (- ln x) * exp (ln (?F x))"
by(simp add: ln_inverse[symmetric] divide_real_def)
thm ln_inverse[symmetric]
also have "... = - g x * exp (ln (1 / a) - (∫t∈{a<..x}. 1 / t ∂lborel))
* exp (ln (?F a) + (∫t∈{a<..x}. g t / t ∂lborel))"
by(simp add: set_integral_inverse lnF_eq ln_divide_pos)
also have "... = c x * exp ((∫t∈{a<..x}. g t / t ∂lborel) - (∫t∈{a<..x}. 1 / t ∂lborel))"
by(simp add: c_def exp_diff exp_add)
also have "... = c x * exp (∫t∈{a<..x}. r t / t ∂lborel)"
using g_integ[OF x] set_integrable_inverse'
by(auto simp: r_def diff_divide_distrib)
finally show "U x = c x * exp (∫t∈{a<..x}. r t / t ∂lborel)" .
qed
have 2:"∀x≥a. set_integrable lborel {a<..x} (λt. r t / t)"
unfolding r_def diff_divide_distrib
by(intro allI impI set_integral_diff set_integrable_inverse' g_integ) auto
have 3:"(r ⤏ ρ) at_top"
using tendsto_diff[OF lim tendsto_const[where k="- 1"]]
by(simp add: r_def g_def tendsto_minus_cancel_left)
have 4:"(c ⤏ C) at_top"
unfolding c_def C_def times_divide_eq_right[symmetric] using lim
by(intro tendsto_mult)
(auto simp: g_def )
have 5:"0 < C"
using rho by(simp add: C_def)
show "regularly_varying U ρ"
using 1 2 3 4 5
by(subst Karamata_representation_iff[OF U_meas U_pos])
(auto intro!: exI[where x=a,OF conjI[OF _ exI[where x=c,
OF exI[where x=r,OF exI[where x=C]]]]]
simp del: ex_simps)
qed
subsection ‹Properties Related to Derivative›
text ‹Proposition~2.5 (a)~\<^cite>‹Resnick›.›
lemma deriv_ratio_regularly_varying_uniform:
fixes U U' :: "real ⇒ real" and ρ a b :: real
assumes t0: "0 < t0"
and deriv: "⋀t. t0 < t ⟹ (U has_real_derivative U' t) (at t)"
and U'cont: "continuous_on {t0<..} U'"
and Upos: "⋀t. t0 < t ⟹ 0 < U t"
and lim: "((λt. t * U' t / U t) ⤏ ρ) at_top"
and a: "0 < a"
shows "uniform_limit {a..b} (λt x. U (t * x) / U t) (λx. x powr ρ) at_top"
proof -
have Ucont:"continuous_on {t0<..} U"
by(auto intro!: has_real_derivative_imp_continuous_on[where f'=U'] deriv)
define V where "V ≡ λx. if x ∈ {t0<..} then U x else 1"
have V_eq_U:"⋀x. t0 < x ⟹ V x = U x"
by(simp add: V_def)
have cong:"∀⇩F t in at_top. ∀x∈{a..b}. V (t * x) / V t = U (t * x) / U t"
proof(safe intro!: eventually_at_top_linorderI[where c="max (t0 + 1) ((t0 + 1) / a)"])
fix t x
assume "max (t0 + 1) ((t0 + 1) / a) ≤ t" "x ∈ {a..b}"
then have "t0 < t" "t0 < t * x"
using a t0 by(auto intro!: order.strict_trans2[of t0 "t0 + 1" "t * x"]
order.trans[of "t0 + 1" "t * a" "t * x"] simp: pos_divide_le_eq )
thus "V (t * x) / V t = U (t * x) / U t"
by(simp add: V_eq_U)
qed
have rv:"regularly_varying V ρ"
proof(subst Karamata_representation_iff)
show "V ∈ borel_measurable (restrict_space borel {0<..})"
unfolding V_def
by(intro measurable_restrict_space1 borel_measurable_continuous_on_if Ucont) auto
show V_pos:"⋀x. 0 < V x"
by(auto simp: V_def Upos)
define A where "A ≡ t0 + 1"
have A_pos[arith]:"0 < A" and t0A[arith]:"t0 < A"
using t0 by(simp_all add: A_def)
define r where "r ≡ λx. x * U' x / U x"
have r_lim:"(r ⤏ ρ) at_top"
unfolding r_def by fact
have deriv':"A ≤ x ⟹ ((λx. ln (U x)) has_real_derivative r x / x) (at x)" for x
by(intro DERIV_cong[where X="1 / U x * U' x" and Y="r x / x"] derivative_intros deriv)
(auto simp: r_def Upos)
have rcont:"continuous_on {t0<..} (λx. r x / x)"
unfolding r_def using Upos A_pos t0A t0
by(intro continuous_intros continuous_on_subset[OF U'cont]
continuous_on_subset[OF Ucont] ballI dual_order.strict_implies_not_eq) auto
have "(∫t∈{A<..x}. r t / t ∂lborel) = ln (V x) - ln (V A)" if x:"A ≤ x" for x
proof -
have "(∫t∈{A<..x}. r t / t ∂lborel) = (∫t. r t / t * indicator {A..x} t ∂lborel)"
unfolding LBINT_Ioc_eq_Icc by(simp add: set_lebesgue_integral_def mult.commute)
also have "... = ln (U x) - ln (U A)"
using x
by(intro integral_FTC_Icc_real deriv' continuous_on_interior[OF rcont])
(auto simp: interior_open)
finally show ?thesis
using x by(simp add: V_eq_U)
qed
hence eq:"A ≤ x ⟹ V x = V A * exp (∫t∈{A<..x}. r t / t ∂lborel)" for x
using V_pos[of A] by(auto simp add: exp_diff V_pos[of x])
have integ:"set_integrable lborel {A<..x} (λt. r t / t)" if "A ≤ x" for x
by(auto intro!: set_integrable_subset[OF borel_integrable_atLeastAtMost'[of A x]]
continuous_on_subset[OF rcont])
show "∃A>0. ∃c r C.
(∀x ≥ A. V x = c x * exp (∫t∈{A<..x}. r t / t ∂lborel))
∧ (∀x ≥ A. set_integrable lborel {A<..x} (λt. r t / t))
∧ (r ⤏ ρ) at_top
∧ (c ⤏ C) at_top
∧ 0 < C"
using eq integ r_lim V_pos[of A] tendsto_const[of "V A"] A_pos
by fast
qed
hence "uniform_limit {a..b} (λt x. V (t * x) / V t) (λx. x powr ρ) at_top"
by(simp add: a regularly_varying_UCT_interval)
with cong show ?thesis
using uniform_limit_cong by fast
qed
corollary deriv_ratio_regularly_varying:
fixes U U' :: "real ⇒ real" and γ x :: real
assumes "0 < t0"
and "⋀t. t0 < t ⟹ (U has_real_derivative U' t) (at t)"
and "continuous_on {t0<..} U'"
and "⋀t. t0 < t ⟹ 0 < U t"
and "((λt. t * U' t / U t) ⤏ γ) at_top"
and "0 < x"
shows "((λt. U (t * x) / U t) ⤏ x powr γ) at_top"
by(auto intro!: tendsto_uniform_limitI[OF
deriv_ratio_regularly_varying_uniform[where a=x and b=x,OF assms]])
lemma deriv_ratio_regularly_varying_uminus:
fixes U u :: "real ⇒ real" and γ L x :: real
assumes t0: "0 < t0"
and Uderiv: "⋀t. t0 < t ⟹ (U has_real_derivative u t) (at t)"
and ucont: "continuous_on {t0<..} u"
and Ult: "⋀t. t0 < t ⟹ U t < L"
and lim: "((λt. t * u t / (L - U t)) ⤏ - γ) at_top"
and x: "0 < x"
shows "((λt. (L - U (t * x)) / (L - U t)) ⤏ x powr γ) at_top"
using DERIV_diff[OF DERIV_const[of L] Uderiv] ucont tendsto_minus[OF lim]
by(auto intro!: deriv_ratio_regularly_varying[where U'="λx. - u x",OF t0] continuous_minus
Ult x simp: continuous_on_eq_continuous_within)
text ‹Corollary~1.1.10~\<^cite>‹deHaanFerreira›.›
lemma deriv_diff_ratio_regularly_varying:
fixes U u u' :: "real ⇒ real" and γ x :: real
assumes t0: "0 < t0"
and U_deriv: "⋀t. t0 < t ⟹ (U has_real_derivative u t) (at t)"
and u_deriv: "⋀t. t0 < t ⟹ (u has_real_derivative u' t) (at t)"
and u'_cont: "continuous_on {t0<..} u'"
and u_pos: "⋀t. t0 < t ⟹ 0 < u t"
and lim: "((λt. t * u' t / u t) ⤏ γ - 1) at_top"
and x: "0 < x"
shows "((λt. (U (t * x) - U t) / (t * u t))
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
proof -
have u_cont:"continuous_on {t0<..} u"
by(intro has_real_derivative_imp_continuous_on[where f'=u'] u_deriv) auto
define v where "v ≡ λx. (if x ∈ {t0<..} then u x else 1)"
have v_eq:"⋀t. t0 < t ⟹ v t = u t"
by(simp add: v_def)
have v_pos:"⋀t. 0 < v t"
using u_pos by(simp add: v_def)
have [measurable]:"v ∈ borel_measurable borel"
unfolding v_def
by(intro measurable_restrict_space1 borel_measurable_continuous_on_if u_cont) auto
have rv:"regularly_varying v (γ - 1)"
proof(safe intro!: regularly_varyingI_total)
fix y::real
assume "0 < y"
then show "((λt. v (t * y) / v t) ⤏ y powr (γ - 1)) at_top"
by(intro Lim_transform_eventually
[OF deriv_ratio_regularly_varying[OF t0 u_deriv u'_cont u_pos lim]]
eventually_at_top_linorderI[where c="max (t0 + 1) (t0 / y + 1)"]
arg_cong2[where f=divide,OF v_eq[symmetric] v_eq[symmetric]])
(auto simp: field_simps)
qed (use v_pos in auto)
obtain t' where t':"⋀x y. t' ≤ x ⟹ x ≤ y ⟹ v y / v x ≤ 2 * (y / x) powr γ"
using Potter_bounds1[where A=2 and d=1,OF rv] by auto
obtain t'' where t'':"⋀x y. t'' ≤ y ⟹ y ≤ x ⟹ v y / v x ≤ 2 * (y / x) powr (γ - 2)"
using Potter_bounds2[where A=2 and d=1,OF rv] by auto
define T where "T ≡ max (max (t0 + 1) (t0 / x + 1)) (max t' (t'' / x + 1))"
have T:"t0 < T" "⋀t. T ≤ t ⟹ t0 < t" "⋀t. T ≤ t ⟹ t0 < t * x" "t' ≤ T"
"⋀t. T ≤ t ⟹ t'' ≤ t * x"
and T_pos:"0 < T"
using x t0 by(auto simp: T_def field_simps)
have div_eq1:"T ≤ t ⟹ 1 ≤ s ⟹ v (t * s)/ v t = u (t * s) / u t" for t s
using T_pos T
by(intro arg_cong2[where f=divide,OF v_eq v_eq] order.strict_trans2[of t0 t "t * s"])
auto
have div_eq2:"T ≤ t ⟹ x ≤ s ⟹ v (t * s)/ v t = u (t * s) / u t" for t s
using T_pos T x
by(intro arg_cong2[where f=divide,OF v_eq v_eq] order.strict_trans2[of t0 "t * x" "t * s"])
auto
have leq1:"T ≤ x ⟹ x ≤ y ⟹ v y / v x ≤ 2 * (y / x) powr γ" for x y
using t' t'' T by simp_all
consider "x < 1" | "1 < x" | "x = 1"
by linarith
thus ?thesis
proof cases
assume x1:"1 < x"
have "∀⇩F t in at_top. (U (t * x) - U t) / (t * u t) = (∫s∈{1..x}. v (t * s) / v t ∂lborel)"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
hence t_pos:"0 < t" and t0t:"t0 < t"
using T_pos T by simp_all
have "(U (t * x) - U t) / (t * u t)
= (∫s. v s / (t * v t) * indicat_real {t..t * x} s ∂lborel)"
using U_deriv x1 t_pos v_pos t0t
by(subst integral_FTC_Icc_nonneg[where F="λx. U x / (t * v t)"])
(auto simp: v_eq[symmetric] diff_divide_distrib
intro!: divide_nonneg_pos less_imp_le DERIV_cdivide)
also have "... = (∫s∈{1..x}. v (t * s) / v t ∂lborel)"
using t_pos v_pos
by(subst lborel_integral_real_affine
[of t "λs. v s / (t * v t) * indicat_real {t..t * x} s" 0])
(auto simp: set_lebesgue_integral_def indicator_def
intro!: Bochner_Integration.integral_cong)
finally show "(U (t * x) - U t) / (t * u t) = (∫s∈{1..x}. v (t * s) / v t ∂lborel)" .
qed
moreover have "((λt. (∫s∈{1..x}. v (t * s) / v t ∂lborel))
⤏ (∫s∈{1..x}. s powr (γ - 1) ∂lborel)) at_top"
unfolding set_lebesgue_integral_def
proof(rule integral_dominated_convergence_real[OF _ _ _ AE_I2 AE_I2])
fix t s
assume "T ≤ t"
thus "norm (indicat_real {1..x} s *⇩R (v (t * s) / v t))
≤ 2 * (indicator {1..x} s *⇩R s powr γ)"
using v_pos leq1[of t "t * s"] T_pos
by(auto simp: indicator_def abs_of_pos)
next
fix y
show "((λt. indicat_real {1..x} y *⇩R (v (t * y) / v t))
⤏ indicat_real {1..x} y *⇩R y powr (γ - 1)) at_top"
using regularly_varying_lim[OF rv,of y] by(auto simp: indicator_def)
qed(auto intro!: borel_integrable_compact continuous_on_powr continuous_on_mult
simp del: real_scaleR_def)
ultimately have lim':"((λt. (U (t * x) - U t) / (t * u t))
⤏ (∫s∈{1..x}. s powr (γ - 1) ∂lborel)) at_top"
using tendsto_cong by fast
have "(∫s∈{1..x}. s powr (γ - 1) ∂lborel) = (if γ = 0 then ln x else (x powr γ - 1) / γ)"
proof(cases "γ = 0")
assume gamma:"γ = 0"
then have "(∫s∈{1..x}. s powr (γ - 1) ∂lborel) = (∫s∈{1<..x}. 1 / s ∂lborel)"
by(auto intro!: set_integral_cong simp: LBINT_Ioc_eq_Icc )
also have "... = ln x"
using x1 by(simp add: set_integral_inverse)
finally show ?thesis
using gamma by simp
qed(use x1 in "auto simp: set_integral_powr_Icc diff_divide_distrib")
with lim' show ?thesis
by simp
next
assume x1:"x < 1"
have "∀⇩F t in at_top. (U (t * x) - U t) / (t * u t) = - (∫s∈{x..1}. v (t * s) / v t ∂lborel)"
proof(safe intro!: eventually_at_top_linorderI[where c=T])
fix t
assume t:"T ≤ t"
hence t_pos:"0 < t" and t0t:"t0 < t * x" "t0 < t"
using T_pos T by simp_all
have "(U (t * x) - U t) / (t * u t)
= - (∫s. v s / (t * v t) * indicat_real {t * x..t} s ∂lborel)"
using x1 t_pos v_pos t0t U_deriv
by(subst integral_FTC_Icc_nonneg[where F="λx. U x / (t * v t)"])
(auto simp: v_eq[symmetric] diff_divide_distrib
intro!: divide_nonneg_pos less_imp_le DERIV_cdivide)
also have "... = - (∫s∈{x..1}. v (t * s) / v t ∂lborel)"
using t_pos v_pos
by(subst lborel_integral_real_affine
[of t "λs. v s / (t * v t) * indicat_real {t * x..t} s" 0])
(auto simp: set_lebesgue_integral_def indicator_def
intro!: Bochner_Integration.integral_cong)
finally show "(U (t * x) - U t) / (t * u t) = - (∫s∈{x..1}. v (t * s) / v t ∂lborel)" .
qed
moreover have "((λt. (∫s∈{x..1}. v (t * s) / v t ∂lborel))
⤏ (∫s∈{x..1}. s powr (γ - 1) ∂lborel)) at_top"
unfolding set_lebesgue_integral_def
proof(rule integral_dominated_convergence_real[OF _ _ _ AE_I2 AE_I2])
fix t s
assume t:"T ≤ t"
hence "x ≤ s ⟹ t'' ≤ t * s"
using T_pos t x by(auto intro!: order.trans[OF T(5)[OF t]] mult_mono)
thus "norm (indicat_real {x..1} s *⇩R (v (t * s) / v t))
≤ 2 * (indicator {x..1} s *⇩R s powr (γ - 2))"
using v_pos t''[of "t * s" t] T_pos t
by(auto simp: indicator_def abs_of_pos)
next
fix y
show "((λt. indicat_real {x..1} y *⇩R (v (t * y) / v t))
⤏ indicat_real {x..1} y *⇩R y powr (γ - 1)) at_top"
using regularly_varying_lim[OF rv,of y] x by(auto simp: indicator_def)
qed(use x in "auto intro!: borel_integrable_compact continuous_on_powr continuous_on_mult
simp del: real_scaleR_def")
ultimately have lim':"((λt. (U (t * x) - U t) / (t * u t))
⤏ - (∫s∈{x..1}. s powr (γ - 1) ∂lborel)) at_top"
using tendsto_cong tendsto_minus by fast
have "(∫s∈{x..1}. s powr (γ - 1) ∂lborel) = - (if γ = 0 then ln x else (x powr γ - 1) / γ)"
proof(cases "γ = 0")
assume gamma:"γ = 0"
then have "(∫s∈{x..1}. s powr (γ - 1) ∂lborel) = (∫s∈{x<..1}. 1 / s ∂lborel)"
using x by(auto intro!: set_integral_cong simp: LBINT_Ioc_eq_Icc)
also have "... = - ln x"
using x x1 by(simp add: set_integral_inverse)
finally show ?thesis
using gamma by simp
qed(use x1 x in "auto simp: set_integral_powr_Icc diff_divide_distrib")
with lim' show ?thesis
by simp
qed simp
qed
end