Theory Peaks_Over_Threshold
section ‹Peaks Over Threshold›
theory Peaks_Over_Threshold
imports
"Domain_of_Attraction"
begin
text ‹In this section, we formalize the Pickands--Balkema--de Haan theorem.
Our formalization is stated in the form of Theorem~3.4.13(b)
in the book by Embrechts et al.~\<^cite>‹EmbrechtsKluppelbergMikosch›.
The original sources of the theorem are Theorems~3 and~4 in the paper
by Balkema and de Haan~\<^cite>‹BalkemaDeHaan1974› and
Theorem~7 in the paper by Pickands~\<^cite>‹Pickands1975›.›
subsection ‹Excess (Peaks-Over-Threshold) Distribution Function›
definition excess_cdf :: "(real ⇒ real) ⇒ real ⇒ real ⇒ real" where
"excess_cdf F u x = 1 - (1 - F (u + x)) / (1 - F u)"
lemma excess_cdf_def2:"F u < 1 ⟹ excess_cdf F u x = (F (u + x) - F u) / (1 - F u)"
by (smt (verit, ccfv_threshold) add_divide_distrib divide_self_if excess_cdf_def)
lemma excess_cdf_0[simp]: "F u < 1 ⟹ excess_cdf F u 0 = 0"
by (simp add: excess_cdf_def)
lemma excess_cdf_eq_1_of_F_eq_1:
assumes "F u = 1"
shows "excess_cdf F u x = 1"
using assms by (simp add: excess_cdf_def)
lemma excess_cdf_mono:
assumes F: "right_continuous_mono F 0 1" and xy: "x ≤ y"
shows "excess_cdf F u x ≤ excess_cdf F u y"
proof (cases "F u < 1")
assume Fu: "F u < 1"
have mono: "F (u + x) ≤ F (u + y)"
using xy by (intro monoD[OF right_continuous_mono.mono[OF F]]) simp
have "(1 - F (u + y)) / (1 - F u) ≤ (1 - F (u + x)) / (1 - F u)"
using mono Fu by (intro divide_right_mono) auto
thus ?thesis
by (simp add: excess_cdf_def)
next
case False
hence "F u = 1"
using right_continuous_mono.f_le_b[OF F, of u] by linarith
thus ?thesis
by (simp add: excess_cdf_eq_1_of_F_eq_1)
qed
lemma excess_cdf_bounds:
assumes F: "right_continuous_mono F 0 1" and x: "0 ≤ x"
shows "0 ≤ excess_cdf F u x" "excess_cdf F u x ≤ 1"
proof -
have "0 ≤ excess_cdf F u x ∧ excess_cdf F u x ≤ 1"
proof (cases "F u < 1")
case Fu: True
have le1: "F (u + x) ≤ 1"
using right_continuous_mono.f_le_b[OF F] .
have ge: "F u ≤ F (u + x)"
using x by (intro monoD[OF right_continuous_mono.mono[OF F]]) simp
have "(1 - F (u + x)) / (1 - F u) ≤ 1"
using ge Fu by (simp add: divide_le_eq)
moreover have "0 ≤ (1 - F (u + x)) / (1 - F u)"
using le1 Fu by (simp add: divide_nonneg_pos)
ultimately show ?thesis
by (simp add: excess_cdf_def)
next
case False
hence "F u = 1"
using right_continuous_mono.f_le_b[OF F, of u] by linarith
thus ?thesis
by (simp add: excess_cdf_eq_1_of_F_eq_1)
qed
thus "0 ≤ excess_cdf F u x" "excess_cdf F u x ≤ 1"
by auto
qed
lemma excess_cdf_eq_1_beyond_support:
assumes F: "right_continuous_mono F 0 1" and bdd: "bdd_support F"
and xu: "x_star F ≤ u + x"
shows "excess_cdf F u x = 1"
proof -
have "F (x_star F) = 1"
by (intro F_x_star_eq_1 F bdd)
moreover have "F (x_star F) ≤ F (u + x)"
using xu by (intro monoD[OF right_continuous_mono.mono[OF F]])
ultimately have "F (u + x) = 1"
using right_continuous_mono.f_le_b[OF F, of "u + x"] by linarith
thus ?thesis
by (simp add: excess_cdf_def)
qed
lemma excess_tendsto_of_divide_tail:
fixes F f :: "real ⇒ real" and γ x :: real
assumes F: "right_continuous_mono F 0 1"
and fpos: "⋀t. 0 < f t"
and lim: "⋀x. 1 + γ * x > 0 ⟹
((λt. (1 - F (t + x * f t)) / (1 - F t))
⤏ - ln (EVD_cdf γ 0 1 x)) (endpoint_filter F)"
and x: "0 ≤ x"
shows "((λt. excess_cdf F t (f t * x)) ⤏ GPD_cdf γ 0 1 x) (endpoint_filter F)"
proof -
have main: "((λt. excess_cdf F t (f t * y)) ⤏ GPD_cdf γ 0 1 y) (endpoint_filter F)"
if y: "0 ≤ y" and supp: "1 + γ * y > 0" for y
proof -
have ratio_lim: "((λt. (1 - F (t + y * f t)) / (1 - F t))
⤏ 1 - GPD_cdf γ 0 1 y) (endpoint_filter F)"
using lim[OF supp] EVD_tail_eq_GPD_cdf[OF supp y] by simp
have "((λt. 1 - (1 - F (t + y * f t)) / (1 - F t))
⤏ 1 - (1 - GPD_cdf γ 0 1 y)) (endpoint_filter F)"
by (intro tendsto_diff tendsto_const ratio_lim)
thus ?thesis
by (simp add: excess_cdf_def mult.commute)
qed
show ?thesis
proof (cases "1 + γ * x > 0")
case True
show ?thesis
by (rule main[OF x True])
next
case False
hence notsupp: "1 + γ * x ≤ 0"
by simp
have gneg: "γ < 0"
proof (rule ccontr)
assume "¬ γ < 0"
hence "0 ≤ γ * x"
using x by (intro mult_nonneg_nonneg) auto
with notsupp show False
by simp
qed
have gpdx1: "GPD_cdf γ 0 1 x = 1"
using x gneg notsupp by (auto simp: GPD_cdf_def[OF zero_less_one] Let_def)
have gpdbdry: "GPD_cdf γ 0 1 (- 1 / γ) = 1"
using gneg by (simp add: GPD_cdf_def[OF zero_less_one] Let_def)
have gpd_cont: "(GPD_cdf γ 0 1 ⤏ 1) (at (- 1 / γ))"
using isCont_GPD_cdf[OF zero_less_one, where ξ = γ and μ = 0 and x = "- 1 / γ"] gpdbdry
by (simp add: isCont_def)
have gpd_cont_left: "(GPD_cdf γ 0 1 ⤏ 1) (at_left (- 1 / γ))"
using gpd_cont by (simp add: filterlim_at_split)
have le1: "excess_cdf F t (f t * x) ≤ 1" for t
using fpos[of t] x by (intro excess_cdf_bounds(2)[OF F]) simp
have "((λt. excess_cdf F t (f t * x)) ⤏ 1) (endpoint_filter F)"
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e: "0 < e"
have "∀⇩F y in at_left (- 1 / γ). 1 - e < GPD_cdf γ 0 1 y"
using order_tendstoD(1)[OF gpd_cont_left, of "1 - e"] e by simp
moreover have "∀⇩F y in at_left (- 1 / γ). y < - 1 / γ ∧ 0 ≤ y"
using gneg by (intro eventually_at_leftI[of 0]) auto
ultimately obtain x0 where x0: "1 - e < GPD_cdf γ 0 1 x0" "x0 < - 1 / γ" "0 ≤ x0"
using eventually_happens'[OF trivial_limit_at_left_real eventually_conj] by blast
have supp0: "1 + γ * x0 > 0"
using mult_strict_left_mono_neg[OF x0(2) gneg] gneg by simp
have x0x: "x0 < x"
proof (rule ccontr)
assume "¬ x0 < x"
hence "1 + γ * x0 ≤ 1 + γ * x"
using gneg by (intro add_left_mono mult_left_mono_neg) auto
with supp0 notsupp show False
by simp
qed
have "∀⇩F t in endpoint_filter F. 1 - e < excess_cdf F t (f t * x0)"
using order_tendstoD(1)[OF main[OF x0(3) supp0] x0(1)] .
thus "∀⇩F t in endpoint_filter F. ¦excess_cdf F t (f t * x) - 1¦ < e"
proof eventually_elim
case (elim t)
have "excess_cdf F t (f t * x0) ≤ excess_cdf F t (f t * x)"
using fpos[of t] x0x
by (intro excess_cdf_mono[OF F] mult_left_mono less_imp_le) auto
with elim le1[of t] show ?case
by (simp add: abs_less_iff)
qed
qed
thus ?thesis
using gpdx1 by simp
qed
qed
lemma tail_probability_u_form:
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and dom: "domain_of_attraction F (EVD_cdf γ 0 1)"
shows "∃β. (∀u. 0 < β u) ∧
(∀x≥0. ((λu. excess_cdf F u (β u * x) - GPD_cdf γ 0 1 x)
⤏ 0) (endpoint_filter F))"
proof -
obtain f where fpos: "⋀t. 0 < f t"
and lim: "⋀x. 1 + γ * x > 0 ⟹
((λt. (1 - F (t + x * f t)) / (1 - F t))
⤏ - ln (EVD_cdf γ 0 1 x)) (endpoint_filter F)"
using MDA_iff_divide_tail[OF F] dom by blast
show ?thesis
proof (safe intro!: exI[of _ f])
show "⋀u. 0 < f u"
using fpos by blast
next
fix x :: real
assume x: "0 ≤ x"
from tendsto_diff[OF excess_tendsto_of_divide_tail[OF F fpos lim x] tendsto_const,
of "GPD_cdf γ 0 1 x"]
show "((λu. excess_cdf F u (f u * x) - GPD_cdf γ 0 1 x) ⤏ 0) (endpoint_filter F)"
by simp
qed
qed
lemma excess_pointwise_imp_uniform:
fixes F :: "real ⇒ real" and β :: "real ⇒ real" and FF :: "real filter"
assumes F: "right_continuous_mono F 0 1" and βpos: "⋀u. 0 < β u"
and pconv: "⋀x. 0 ≤ x ⟹ ((λu. excess_cdf F u (β u * x)) ⤏ GPD_cdf γ 0 1 x) FF"
shows "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1) FF"
proof -
interpret GPD: right_continuous_mono "GPD_cdf γ 0 1" 0 1
by (intro right_continuous_mono_GPD_cdf zero_less_one)
interpret F: right_continuous_mono F 0 1
by fact
show ?thesis
proof (rule mono_on_UCT_atLeast[OF eventuallyI[OF mono_onI] eventuallyI mono_onI])
fix u :: real and x y :: real
assume "x ∈{0..}" "x ≤ y"
thus "excess_cdf F u (β u * x) ≤ excess_cdf F u (β u * y)"
using βpos[of u] by (intro excess_cdf_mono[OF F] mult_left_mono) auto
next
fix u :: real
show "∀x≥0. excess_cdf F u (β u * x) ≤ 1"
using βpos[of u] excess_cdf_bounds[OF F] by simp
next
fix x y :: real
assume "x ∈{0..}" "x ≤ y"
thus "GPD_cdf γ 0 1 x ≤ GPD_cdf γ 0 1 y"
by (intro monoD[OF GPD.mono])
next
show "continuous_on {0..} (GPD_cdf γ 0 1)"
using isCont_GPD_cdf by(auto intro!: continuous_at_imp_continuous_on)
next
show "(GPD_cdf γ 0 1 ⤏ 1) at_top"
by (intro GPD_cdf_at_top_1 zero_less_one)
qed fact
qed
lemma tail_probability_u_form_uniform:
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and dom: "domain_of_attraction F (EVD_cdf γ 0 1)"
shows "∃β. (∀u. 0 < β u) ∧
uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
proof -
obtain β where βpos: "⋀u. 0 < β u"
and pconv0: "⋀x. 0 ≤ x ⟹
((λu. excess_cdf F u (β u * x) - GPD_cdf γ 0 1 x) ⤏ 0) (endpoint_filter F)"
using tail_probability_u_form[OF F dom] by blast
have pconv: "((λu. excess_cdf F u (β u * x)) ⤏ GPD_cdf γ 0 1 x) (endpoint_filter F)"
if x: "0 ≤ x" for x
using tendsto_add[OF pconv0[OF x] tendsto_const, of "GPD_cdf γ 0 1 x"] by simp
have "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1) (endpoint_filter F)"
by (intro excess_pointwise_imp_uniform[OF F βpos] pconv)
thus ?thesis
using βpos by blast
qed
subsection ‹Pickands--Balkema--de Haan Theorem›
text ‹The proof of the direct half follows the proof of Theorem~3.4.13(b) in the
same book: the pointwise statement is Theorem~1.1.6(4) of the book by
de Haan and Ferreira~\<^cite>‹deHaanFerreira›, and uniformity follows since the
limit is continuous.
The converse half follows the route sketched in the proof
of Theorem~3.4.5 of Embrechts et al.~\<^cite>‹EmbrechtsKluppelbergMikosch›.›
subsubsection ‹Direct Half›
theorem Pickands_Balkema_de_Haan_forward:
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and dom: "domain_of_attraction F (EVD_cdf γ 0 1)"
shows "∃β. (∀u. 0 < β u) ∧
uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x)
(λx. 0) (endpoint_filter F)"
proof -
obtain β where βpos: "⋀u. 0 < β u"
and ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
using tail_probability_u_form_uniform[OF F dom] by blast
have "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0)
(endpoint_filter F)"
proof (rule uniform_limitI)
fix ε :: real
assume ε: "0 < ε"
show "∀⇩F u in endpoint_filter F.
∀x∈{0..}. dist (excess_cdf F u x - GPD_cdf γ 0 (β u) x) 0 < ε"
using uniform_limitD[OF ul ε]
proof eventually_elim
case (elim u)
show ?case
proof
fix x :: real
assume "x ∈ {0..}"
hence x: "0 ≤ x"
by simp
have y: "x / β u ∈ {0..}"
using x βpos[of u] by simp
have dist_lt: "dist (excess_cdf F u (β u * (x / β u))) (GPD_cdf γ 0 1 (x / β u)) < ε"
using elim y by blast
have rescale: "β u * (x / β u) = x"
using βpos[of u] by simp
have target: "GPD_cdf γ 0 1 (x / β u) = GPD_cdf γ 0 (β u) x"
using GPD_cdf_location_scale[OF βpos[of u], of γ x] by simp
show "dist (excess_cdf F u x - GPD_cdf γ 0 (β u) x) 0 < ε"
using dist_lt unfolding rescale target by (simp add: dist_real_def)
qed
qed
qed
thus ?thesis
using βpos by blast
qed
subsubsection ‹Converse Half›
lemma GPD_level_nonneg:
fixes γ x :: real
assumes "1 ≤ x"
shows "0 ≤ (if γ = 0 then ln x else (x powr γ - 1) / γ)"
by (smt (verit) assms ge_one_powr_ge_zero ln_ge_zero nle_le powr_less_one
powr_one_eq_one zero_le_divide_iff)
lemma GPD_level_pos:
fixes γ x :: real
assumes "1 < x"
shows "0 < (if γ = 0 then ln x else (x powr γ - 1) / γ)"
by (smt (verit, ccfv_SIG) assms divide_neg_neg divide_pos_pos
gr_one_powr ln_one ln_strict_mono powr_less_one)
lemma GPD_level_supp:
fixes γ x :: real
assumes "1 ≤ x"
shows "1 + γ * (if γ = 0 then ln x else (x powr γ - 1) / γ) = (if γ = 0 then 1 else x powr γ)"
using assms by simp
lemma GPD_tail_eq:
assumes x: "0 ≤ x"
shows "1 - GPD_cdf γ 0 1 x
= (if γ = 0 then exp (- x)
else if 0 ≤ 1 + γ * x then (1 + γ * x) powr (- 1 / γ) else 0)"
using x by (simp add: GPD_cdf_def[OF zero_less_one] Let_def)
lemma GPD_tail_level:
assumes x: "1 ≤ x"
shows "1 - GPD_cdf γ 0 1 ((if γ = 0 then ln x else (x powr γ - 1) / γ)) = 1 / x"
proof (cases "γ = 0")
case True
thus ?thesis
using x by (simp add: GPD_tail_eq GPD_level_nonneg exp_minus inverse_eq_divide)
next
case False
have x0: "0 < x"
using x by simp
have supp: "1 + γ * (if γ = 0 then ln x else (x powr γ - 1) / γ) = x powr γ"
using GPD_level_supp[OF x, of γ] False by simp
have "0 < x powr γ"
using x0 by simp
hence "1 - GPD_cdf γ 0 1 (if γ = 0 then ln x else (x powr γ - 1) / γ)
= (x powr γ) powr (- 1 / γ)"
using GPD_level_nonneg[OF x, of γ] False supp by (simp add: GPD_tail_eq)
also have "... = x powr (γ * (- 1 / γ))"
using x0 by (simp add: powr_powr)
also have "... = 1 / x"
using False x0 by (simp add: powr_minus_divide field_simps)
finally show ?thesis .
qed
lemma GPD_tail_strict_antimono:
assumes y: "0 ≤ y" and yz: "y < z" and supp: "0 < 1 + γ * y"
shows "1 - GPD_cdf γ 0 1 z < 1 - GPD_cdf γ 0 1 y"
proof -
have z: "0 ≤ z"
using y yz by simp
show ?thesis
proof (cases "γ = 0")
case True
thus ?thesis
using y z yz by (simp add: GPD_tail_eq)
next
case nonzero: False
show ?thesis
proof (cases "0 < 1 + γ * z")
case True
show ?thesis
proof (cases "0 < γ")
case gpos: True
have "1 + γ * y < 1 + γ * z"
using yz gpos by simp
hence "(1 + γ * z) powr (- 1 / γ) < (1 + γ * y) powr (- 1 / γ)"
using supp gpos by (intro powr_less_mono2_neg) auto
thus ?thesis
using y z supp True nonzero by (simp add: GPD_tail_eq)
next
case False
hence gneg: "γ < 0"
using nonzero by simp
have "1 + γ * z < 1 + γ * y"
using yz gneg by simp
hence "(1 + γ * z) powr (- 1 / γ) < (1 + γ * y) powr (- 1 / γ)"
using True gneg by (intro powr_less_mono2) auto
thus ?thesis
using y z supp True nonzero by (simp add: GPD_tail_eq)
qed
next
case False
hence "1 - GPD_cdf γ 0 1 z ≤ 0"
using z nonzero by (auto simp: GPD_tail_eq)
moreover have "0 < 1 - GPD_cdf γ 0 1 y"
using y supp by (simp add: GPD_tail_eq)
ultimately show ?thesis
by simp
qed
qed
qed
lemma GPD_tail_gt_level:
assumes x: "1 < x" and y: "0 ≤ y" and lt: "y < (if γ = 0 then ln x else (x powr γ - 1) / γ)"
shows "1 / x < 1 - GPD_cdf γ 0 1 y"
proof -
have x1: "1 ≤ x"
using x by simp
have supp: "0 < 1 + γ * y"
proof (cases "γ = 0")
case True
thus ?thesis
by simp
next
case False
hence sup': "1 + γ * (if γ = 0 then ln x else (x powr γ - 1) / γ) = x powr γ"
using GPD_level_supp[OF x1, of γ] by simp
have pos: "0 < x powr γ"
using x by simp
show ?thesis
proof (cases "0 < γ")
case True
hence "0 ≤ γ * y"
using y by simp
thus ?thesis
by simp
next
case False
hence gneg: "γ < 0"
using ‹γ ≠ 0› by simp
have "γ * (if γ = 0 then ln x else (x powr γ - 1) / γ) < γ * y"
by (rule mult_strict_left_mono_neg[OF lt gneg])
thus ?thesis
using sup' pos by linarith
qed
qed
have "1 - GPD_cdf γ 0 1 ((if γ = 0 then ln x else (x powr γ - 1) / γ)) < 1 - GPD_cdf γ 0 1 y"
by (intro GPD_tail_strict_antimono y lt supp)
thus ?thesis
using GPD_tail_level[OF x1, of γ] by simp
qed
lemma GPD_tail_lt_level:
assumes x: "1 < x" and gt: "(if γ = 0 then ln x else (x powr γ - 1) / γ) < y"
shows "1 - GPD_cdf γ 0 1 y < 1 / x"
proof -
have x1: "1 ≤ x"
using x by simp
note L0 = GPD_level_nonneg[OF x1]
have supp: "0 < 1 + γ * (if γ = 0 then ln x else (x powr γ - 1) / γ)"
using GPD_level_supp[OF x1, of γ] x by (cases "γ = 0") auto
have "1 - GPD_cdf γ 0 1 y < 1 - GPD_cdf γ 0 1 ((if γ = 0 then ln x else (x powr γ - 1) / γ))"
by (intro GPD_tail_strict_antimono L0 gt supp)
thus ?thesis
using GPD_tail_level[OF x1, of γ] by simp
qed
lemma endpoint_filter_eventually_at_left:
fixes F :: "real ⇒ real"
assumes ev: "eventually P (endpoint_filter F)"
shows "∀⇩F t in endpoint_filter F. eventually P (at_left t)"
proof (cases "bdd_support F")
case True
hence eq: "endpoint_filter F = at_left (x_star F)"
by (simp add: endpoint_filter)
obtain c where c: "c < x_star F"
and P: "⋀z. c < z ⟹ z < x_star F ⟹ P z"
by (metis assms eq eventually_at_left_field)
show ?thesis
unfolding eq
proof (rule eventually_at_leftI[where a = c])
fix t :: real
assume "t ∈ {c<..<x_star F}"
hence t: "c < t" "t < x_star F"
by auto
show "eventually P (at_left t)"
proof (rule eventually_at_leftI[where a = c])
fix z :: real
assume "z ∈ {c<..<t}"
thus "P z"
using t by (auto intro!: P)
next
show "c < t"
using t by simp
qed
next
show "c < x_star F"
by (rule c)
qed
next
case False
hence eq: "endpoint_filter F = at_top"
by (simp add: endpoint_filter)
obtain d where d: "⋀z. d ≤ z ⟹ P z"
using ev[unfolded eq] by (auto simp: eventually_at_top_linorder)
show ?thesis
unfolding eq
proof (rule eventually_at_top_linorderI[where c = "d + 1"])
fix t :: real
assume t: "d + 1 ≤ t"
show "eventually P (at_left t)"
proof (rule eventually_at_leftI[where a = d])
fix z :: real
assume "z ∈ {d<..<t}"
thus "P z"
by (auto intro!: d)
next
show "d < t"
using t by simp
qed
qed
qed
lemma excess_uniform_scaled_iff:
fixes F :: "real ⇒ real" and β :: "real ⇒ real" and FF :: "real filter"
assumes βpos: "⋀u. 0 < β u"
shows "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0) FF
⟷ uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1) FF"
proof
assume ul: "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0) FF"
show "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1) FF"
proof (rule uniform_limitI)
fix ε :: real
assume ε: "0 < ε"
show "∀⇩F u in FF. ∀y∈{0..}. dist (excess_cdf F u (β u * y)) (GPD_cdf γ 0 1 y) < ε"
proof(safe intro!: eventually_mono[OF uniform_limitD[OF ul ε]])
fix u y :: real
assume h:"∀z∈{0..}. dist (excess_cdf F u z - GPD_cdf γ 0 (β u) z) 0 < ε"
and y:"0 ≤ y"
have mem: "β u * y ∈ {0..}"
using βpos[of u] y by simp
have target: "GPD_cdf γ 0 (β u) (β u * y) = GPD_cdf γ 0 1 y"
using GPD_cdf_location_scale[OF βpos[of u], of γ "β u * y"] βpos[of u] by simp
have "¦excess_cdf F u (β u * y) - GPD_cdf γ 0 (β u) (β u * y)¦ < ε"
using h mem by (simp add: dist_real_def)
thus "dist (excess_cdf F u (β u * y)) (GPD_cdf γ 0 1 y) < ε"
using target by (simp add: dist_real_def)
qed
qed
next
assume ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1) FF"
show "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0) FF"
proof (rule uniform_limitI)
fix ε :: real
assume ε: "0 < ε"
show "∀⇩F u in FF. ∀x∈{0..}. dist (excess_cdf F u x - GPD_cdf γ 0 (β u) x) 0 < ε"
proof(safe intro!: eventually_mono[OF uniform_limitD[OF ul ε]])
fix u x :: real
assume h:"∀y∈{0..}. dist (excess_cdf F u (β u * y)) (GPD_cdf γ 0 1 y) < ε"
and x:"0 ≤ x"
hence x: "0 ≤ x"
by simp
have mem: "x / β u ∈ {0..}"
using βpos[of u] x by simp
have rescale: "excess_cdf F u (β u * (x / β u)) = excess_cdf F u x"
using βpos[of u] by simp
have target: "GPD_cdf γ 0 1 (x / β u) = GPD_cdf γ 0 (β u) x"
using GPD_cdf_location_scale[OF βpos[of u], of γ x] by simp
have "dist (excess_cdf F u (β u * (x / β u))) (GPD_cdf γ 0 1 (x / β u)) < ε"
using h mem by blast
hence "¦excess_cdf F u x - GPD_cdf γ 0 (β u) x¦ < ε"
using rescale target by (simp add: dist_real_def)
thus "dist (excess_cdf F u x - GPD_cdf γ 0 (β u) x) 0 < ε"
by (simp add: dist_real_def)
qed
qed
qed
lemma excess_uniform_eventually:
fixes F :: "real ⇒ real" and β :: "real ⇒ real"
assumes F: "right_continuous_mono F 0 1"
and ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
and δ: "0 < δ"
shows "∀⇩F t in endpoint_filter F. F t < 1 ∧
(∀x≥0. ¦excess_cdf F t (β t * x) - GPD_cdf γ 0 1 x¦ < δ)"
by(auto intro!: eventually_mono[OF eventually_conj
[OF F_lt_1_endpoint[OF F] uniform_limitD[OF ul δ]]] simp: dist_real_def)
lemma excess_iterate_tail_small:
fixes F :: "real ⇒ real" and β :: "real ⇒ real"
assumes βpos: "⋀u. 0 < β u"
and Y0: "0 < Y0" and KY0: "1 / 2 ≤ GPD_cdf γ 0 1 Y0"
and cT: "c < T"
and lt1: "⋀z. c < z ⟹ z < T ⟹ F z < 1"
and near: "⋀z. c < z ⟹ z < T ⟹
¦excess_cdf F z (β z * Y0) - GPD_cdf γ 0 1 Y0¦ < 1 / 4"
and step: "⋀z. c < z ⟹ z < T ⟹ z + β z * Y0 < T"
and δ: "0 < δ"
shows "∃z. c < z ∧ z < T ∧ 1 - F z < δ"
proof -
define w :: "nat ⇒ real" where "w = rec_nat ((c + T) / 2) (λn wn. wn + β wn * Y0)"
have w0: "w 0 = (c + T) / 2"
by (simp add: w_def)
have wSuc: "w (Suc n) = w n + β (w n) * Y0" for n
by (simp add: w_def)
have inv: "c < w n ∧ w n < T" for n
proof (induction n)
case 0
thus ?case
using cT by (simp add: w0)
next
case (Suc n)
have bY: "0 < β (w n) * Y0"
using βpos[of "w n"] Y0 by simp
have lo: "c < w n + β (w n) * Y0"
using Suc[THEN conjunct1] bY by linarith
have hi: "w n + β (w n) * Y0 < T"
using Suc by (intro step) auto
show ?case
using lo hi by (simp add: wSuc)
qed
have wlo: "c < w n" and whi: "w n < T" for n
using inv by blast+
have pos: "0 < 1 - F (w n)" for n
using lt1[OF wlo whi] by simp
have decay: "1 - F (w (Suc n)) ≤ 3 / 4 * (1 - F (w n))" for n
proof -
have "¦excess_cdf F (w n) (β (w n) * Y0) - GPD_cdf γ 0 1 Y0¦ < 1 / 4"
by (intro near wlo whi)
hence e: "1 - excess_cdf F (w n) (β (w n) * Y0) ≤ 3 / 4"
using KY0 by linarith
have "1 - F (w n + β (w n) * Y0)
= (1 - excess_cdf F (w n) (β (w n) * Y0)) * (1 - F (w n))"
using lt1[OF wlo whi, of n] by (simp add: excess_cdf_def)
also have "... ≤ 3 / 4 * (1 - F (w n))"
using e pos[of n] by (intro mult_right_mono) auto
finally show ?thesis
by (simp add: wSuc)
qed
have geom: "1 - F (w n) ≤ (3 / 4) ^ n * (1 - F (w 0))" for n
proof (induction n)
case 0
thus ?case
by simp
next
case (Suc n)
have "1 - F (w (Suc n)) ≤ 3 / 4 * (1 - F (w n))"
by (rule decay)
also have "... ≤ 3 / 4 * ((3 / 4) ^ n * (1 - F (w 0)))"
using Suc by simp
finally show ?case
by simp
qed
have pow0: "(λn. (3 / 4:: real) ^ n) ⇢ 0"
by (rule LIMSEQ_realpow_zero) auto
have "(λn. (3 / 4:: real) ^ n * (1 - F (w 0))) ⇢ 0"
using tendsto_mult[OF pow0 tendsto_const[of "1 - F (w 0)"]] by simp
from order_tendstoD(2)[OF this δ] obtain n
where "(3 / 4 :: real) ^ n * (1 - F (w 0)) < δ"
by (auto simp: eventually_sequentially)
hence "1 - F (w n) < δ"
using geom[of n] by simp
thus ?thesis
using wlo whi by blast
qed
lemma excess_tail_small_below_x_star:
fixes F :: "real ⇒ real" and β :: "real ⇒ real"
assumes F: "right_continuous_mono F 0 1" and βpos: "⋀u. 0 < β u"
and ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
and bdd: "bdd_support F" and δ: "0 < δ"
shows "∃z. z < x_star F ∧ 1 - F z < δ"
proof -
define Y0 where "Y0 = (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)"
have Y0pos: "0 < Y0"
unfolding Y0_def by (intro GPD_level_pos) simp
have KY0: "GPD_cdf γ 0 1 Y0 = 1 / 2"
unfolding Y0_def using GPD_tail_level[of 2 γ] by simp
have eq: "endpoint_filter F = at_left (x_star F)"
using bdd by (simp add: endpoint_filter)
have "∃c<x_star F. ∀z>c. z < x_star F ⟶
F z < 1 ∧ (∀x≥0. ¦excess_cdf F z (β z * x) - GPD_cdf γ 0 1 x¦ < 1 / 4)"
using excess_uniform_eventually[OF F ul, of "1 / 4"]
unfolding eq eventually_at_left_field by simp
then obtain c where c: "c < x_star F"
and P: "⋀z. c < z ⟹ z < x_star F ⟹
F z < 1 ∧ (∀x≥0. ¦excess_cdf F z (β z * x) - GPD_cdf γ 0 1 x¦ < 1 / 4)"
by blast
have near: "¦excess_cdf F z (β z * Y0) - GPD_cdf γ 0 1 Y0¦ < 1 / 4"
if z: "c < z" "z < x_star F" for z
using P[OF z] Y0pos by simp
have step: "z + β z * Y0 < x_star F" if z: "c < z" "z < x_star F" for z
proof (rule ccontr)
assume "¬ z + β z * Y0 < x_star F"
hence ge: "x_star F ≤ z + β z * Y0"
by simp
have "excess_cdf F z (β z * Y0) = 1"
by (rule excess_cdf_eq_1_beyond_support[OF F bdd ge])
hence "(1::real) / 2 < 1 / 4"
using near[OF z] KY0 by simp
thus False
by simp
qed
have "∃z. c < z ∧ z < x_star F ∧ 1 - F z < δ"
proof (rule excess_iterate_tail_small[OF βpos Y0pos])
show "1 / 2 ≤ GPD_cdf γ 0 1 Y0"
by (simp add: KY0)
show "c < x_star F"
by (rule c)
show "⋀z. c < z ⟹ z < x_star F ⟹ F z < 1"
using P by blast
show "⋀z. c < z ⟹ z < x_star F ⟹ ¦excess_cdf F z (β z * Y0) - GPD_cdf γ 0 1 Y0¦ < 1 / 4"
by (rule near)
show "⋀z. c < z ⟹ z < x_star F ⟹ z + β z * Y0 < x_star F"
by (rule step)
show "0 < δ"
by (rule δ)
qed
thus ?thesis
by blast
qed
lemma F_tendsto_1_endpoint_of_excess:
fixes F :: "real ⇒ real" and β :: "real ⇒ real"
assumes F: "right_continuous_mono F 0 1" and βpos: "⋀u. 0 < β u"
and ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
shows "(F ⤏ 1) (endpoint_filter F)"
proof (cases "bdd_support F")
case False
thus ?thesis
using right_continuous_mono.top[OF F] by (simp add: endpoint_filter)
next
case bdd: True
interpret right_continuous_mono F 0 1
by fact
show ?thesis
unfolding endpoint_filter(1)[OF bdd] order_tendsto_iff
proof safe
fix a :: real
assume a: "a < 1"
obtain z where z: "z < x_star F" "1 - F z < 1 - a"
using excess_tail_small_below_x_star[OF F βpos ul bdd, of "1 - a"] a by auto
show "∀⇩F t in at_left (x_star F). a < F t"
proof (intro eventually_at_leftI[OF _ z(1)])
fix t
assume "t ∈ {z<..<x_star F}"
hence "F z ≤ F t"
by (intro monoD[OF mono]) simp
thus "a < F t"
using z(2) by simp
qed
next
fix a :: real
assume "1 < a"
thus "∀⇩F t in at_left (x_star F). F t < a"
using f_le_b[THEN order_le_less_trans]
by (auto intro!: eventually_at_leftI[of "x_star F - 1"])
qed
qed
lemma tail_quantile_asymp_inverse_of_excess:
fixes F :: "real ⇒ real" and β :: "real ⇒ real"
assumes F: "right_continuous_mono F 0 1" and βpos: "⋀u. 0 < β u"
and ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
shows "((λs. s * (1 - F (tail_quantile F s))) ⤏ 1) at_top"
proof -
define Y0 where "Y0 = (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)"
have Y0pos: "0 < Y0"
unfolding Y0_def by (intro GPD_level_pos) simp
have KY0: "GPD_cdf γ 0 1 Y0 = 1 / 2"
unfolding Y0_def using GPD_tail_level[of 2 γ] by simp
note Flim = F_tendsto_1_endpoint_of_excess[OF F βpos ul]
note Uendpoint = tail_quantile_tendsto_endpoint[OF F Flim]
show ?thesis
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e: "0 < e"
define δ where "δ = min (e / 16) (1 / 8)"
define η where "η = min (e / 8) (1 / 8)"
have δpos: "0 < δ" and δle: "δ ≤ 1 / 8" and δe: "δ ≤ e / 16"
using e by (simp_all add: δ_def)
have ηpos: "0 < η" and ηle: "η ≤ 1 / 8" and ηe: "η ≤ e / 8"
using e by (simp_all add: η_def)
define Q where
"Q = (λz. F z < 1 ∧ (∀x≥0. ¦excess_cdf F z (β z * x) - GPD_cdf γ 0 1 x¦ < δ))"
have evP: "∀⇩F t in endpoint_filter F. eventually Q (at_left t)"
unfolding Q_def
by (intro endpoint_filter_eventually_at_left excess_uniform_eventually[OF F ul δpos])
note evU = eventually_compose_filterlim[OF evP Uendpoint]
show "∀⇩F s in at_top. ¦s * (1 - F (tail_quantile F s)) - 1¦ < e"
using evU eventually_gt_at_top[of 1]
proof eventually_elim
case (elim s)
define t0 where "t0 = tail_quantile F s"
have s1: "1 < s"
using elim(2) .
have spos: "0 < s"
using s1 by simp
have fA: "1 - F t0 ≤ 1 / s"
using lt_tail_quantile_iff[OF F s1, of t0] by (simp add: t0_def)
have fB: "1 / s < 1 - F w" if "w < t0" for w
using lt_tail_quantile_iff[OF F s1] that by (simp add: t0_def)
obtain c where c: "c < t0" and Q: "⋀z. c < z ⟹ z < t0 ⟹ Q z"
using elim(1) eventually_at_left_field t0_def by blast
have Qlt1: "F z < 1" if "c < z" "z < t0" for z
using Q[OF that] by (simp add: Q_def)
have Qnear: "¦excess_cdf F z (β z * x) - GPD_cdf γ 0 1 x¦ < δ"
if z: "c < z" "z < t0" and x: "0 ≤ x" for z x
using Q[OF z] x by (simp add: Q_def)
have "∃z. c < z ∧ z < t0 ∧ t0 ≤ z + β z * Y0"
proof (rule ccontr)
assume "¬ (∃z. c < z ∧ z < t0 ∧ t0 ≤ z + β z * Y0)"
hence step: "⋀z. c < z ⟹ z < t0 ⟹ z + β z * Y0 < t0"
by (auto simp: not_le)
have "∃z. c < z ∧ z < t0 ∧ 1 - F z < 1 / s"
proof (rule excess_iterate_tail_small[OF βpos Y0pos])
show "¦excess_cdf F z' (β z' * Y0) - GPD_cdf γ 0 1 Y0¦ < 1 / 4"
if "c < z'" "z' < t0" for z'
using Qnear[OF that less_imp_le[OF Y0pos]] δle by simp
qed(simp_all add: KY0 c Qlt1 step spos)
then obtain z where z: "c < z" "z < t0" "1 - F z < 1 / s"
by blast
show False
using fB[OF z(2)] z(3) by simp
qed
then obtain z where z: "c < z" "z < t0" and zA: "t0 ≤ z + β z * Y0"
by blast
define y0 where "y0 = (t0 - z) / β z"
have βz: "0 < β z"
by (rule βpos)
have y0pos: "0 < y0"
using z(2) βz by (simp add: y0_def)
have y0_le: "y0 ≤ Y0"
using zA βz by (simp add: y0_def field_simps)
have y0_eq: "z + β z * y0 = t0"
using βz by (simp add: y0_def)
define B where "B = 1 - GPD_cdf γ 0 1 y0"
have Bge: "1 / 2 ≤ B"
using monoD[OF right_continuous_mono.mono[OF right_continuous_mono_GPD_cdf[of 1]]
y0_le,of γ 0] KY0
by(simp add: B_def)
have Bpos: "0 < B"
using Bge by simp
have Fzpos: "0 < 1 - F z"
using Qlt1[OF z(1,2)] by simp
have factor: "1 - F (z + h) = (1 - excess_cdf F z h) * (1 - F z)" for h
using Qlt1[OF z(1,2)] by (simp add: excess_cdf_def)
have lower1: "(B - δ) * (1 - F z) < 1 - F t0"
proof -
have "¦excess_cdf F z (β z * y0) - GPD_cdf γ 0 1 y0¦ < δ"
using Qnear[OF z(1,2) less_imp_le[OF y0pos]] .
hence "B - δ < 1 - excess_cdf F z (β z * y0)"
by (simp add: B_def)
moreover have "1 - F t0 = (1 - excess_cdf F z (β z * y0)) * (1 - F z)"
using factor[of "β z * y0"] y0_eq by simp
ultimately show ?thesis
using Fzpos by (simp add: mult_strict_right_mono)
qed
have upper1: "1 / s < (B + η + δ) * (1 - F z)"
proof -
have cont: "isCont (GPD_cdf γ 0 1) y0"
by (intro isCont_GPD_cdf zero_less_one)
obtain ρ where ρ: "0 < ρ"
and ρnear0: "⋀y. y ≠ y0 ⟹ ¦y - y0¦ < ρ ⟹
¦GPD_cdf γ 0 1 y - GPD_cdf γ 0 1 y0¦ < η"
using LIM_D[OF cont[unfolded isCont_def] ηpos] by auto
have ρnear: "¦GPD_cdf γ 0 1 y - GPD_cdf γ 0 1 y0¦ < η" if "¦y - y0¦ < ρ" for y
using ρnear0[of y] that ηpos by (cases "y = y0") auto
define θ where "θ = min (β z * ρ / 2) ((t0 - z) / 2)"
have θpos: "0 < θ"
using βz ρ z(2) by (simp add: θ_def)
have θ1: "θ ≤ β z * ρ / 2"
unfolding θ_def by (rule min.cobounded1)
have θ2: "θ ≤ (t0 - z) / 2"
unfolding θ_def by (rule min.cobounded2)
define w where "w = t0 - θ"
have wlt: "w < t0"
using θpos by (simp add: w_def)
have wgt: "z < w"
using θ2 z(2) by (simp add: w_def)
define yw where "yw = (w - z) / β z"
have yw_eq: "z + β z * yw = w"
using βz by (simp add: yw_def)
have yw0: "0 ≤ yw"
using wgt βz by (simp add: yw_def)
have yw_diff: "yw - y0 = - (θ / β z)"
using βz by (simp add: yw_def y0_def w_def field_simps)
have "¦yw - y0¦ < ρ"
using θ1 βz ρ θpos by (simp add: yw_diff field_simps)
hence "¦GPD_cdf γ 0 1 yw - GPD_cdf γ 0 1 y0¦ < η"
by (rule ρnear)
hence Byw: "1 - GPD_cdf γ 0 1 yw < B + η"
by (simp add: B_def)
have "¦excess_cdf F z (β z * yw) - GPD_cdf γ 0 1 yw¦ < δ"
using Qnear[OF z(1,2) yw0] .
hence "1 - excess_cdf F z (β z * yw) < B + η + δ"
using Byw by simp
moreover have "1 - F w = (1 - excess_cdf F z (β z * yw)) * (1 - F z)"
using factor[of "β z * yw"] yw_eq by simp
ultimately have "1 - F w < (B + η + δ) * (1 - F z)"
using Fzpos by (simp add: mult_strict_right_mono)
thus ?thesis
using fB[OF wlt] by simp
qed
have Bden: "0 < B + η + δ"
using Bpos ηpos δpos by simp
have Bnum: "0 < B - δ"
using Bge δle by simp
have "(B - δ) / (B + η + δ) < s * (1 - F t0)"
proof -
have "1 / s < (B + η + δ) * (1 - F z)"
by (rule upper1)
hence "(B - δ) * (1 / s) < (B - δ) * ((B + η + δ) * (1 - F z))"
using Bnum by (intro mult_strict_left_mono) auto
also have "... = (B + η + δ) * ((B - δ) * (1 - F z))"
by (simp add: algebra_simps)
also have "... < (B + η + δ) * (1 - F t0)"
using lower1 Bden by (simp add: mult_strict_left_mono)
finally have "(B - δ) * (1 / s) < (B + η + δ) * (1 - F t0)" .
hence "(B - δ) / (B + η + δ) < s * (1 - F t0)"
using Bden spos by (simp add: field_simps)
thus ?thesis .
qed
moreover have "1 - 2 * (η + 2 * δ) ≤ (B - δ) / (B + η + δ)"
proof -
have "(B - δ) / (B + η + δ) = 1 - (η + 2 * δ) / (B + η + δ)"
using Bden by (simp add: field_simps)
moreover have "(η + 2 * δ) / (B + η + δ) ≤ 2 * (η + 2 * δ)"
proof -
have "1 / 2 ≤ B + η + δ"
using Bge ηpos δpos by simp
hence "(η + 2 * δ) / (B + η + δ) ≤ (η + 2 * δ) / (1 / 2)"
using ηpos δpos Bden by (intro divide_left_mono) auto
thus ?thesis
by simp
qed
ultimately show ?thesis
by simp
qed
moreover have "s * (1 - F t0) ≤ 1"
using fA spos by (simp add: field_simps)
ultimately show ?case
using ηe δe e by (simp add: t0_def abs_real_def)
qed
qed
qed
lemma tail_quantile_gap_of_excess:
fixes F :: "real ⇒ real" and β :: "real ⇒ real"
assumes F: "right_continuous_mono F 0 1" and βpos: "⋀u. 0 < β u"
and ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
and x: "1 < x"
shows "((λs. (tail_quantile F (s * x) - tail_quantile F s) / β (tail_quantile F s))
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
proof -
note Flim = F_tendsto_1_endpoint_of_excess[OF F βpos ul]
note Uendpoint = tail_quantile_tendsto_endpoint[OF F Flim]
note P1 = tail_quantile_asymp_inverse_of_excess[OF F βpos ul]
have xpos: "0 < x"
using x by simp
define q where "q = 1 / x"
have qpos: "0 < q"
using xpos by (simp add: q_def)
show ?thesis
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e: "0 < e"
define L where "L = (if γ = 0 then ln x else (x powr γ - 1) / γ)"
have Lpos: "0 < L"
unfolding L_def by (intro GPD_level_pos x)
define ε where "ε = min (e / 2) (L / 2)"
have εpos: "0 < ε" and εe: "ε < e" and εL: "ε < L"
using e Lpos by (simp_all add: ε_def)
define ym yp where "ym = L - ε" and "yp = L + ε"
have ym0: "0 < ym"
using εL by (simp add: ym_def)
have ymL: "ym < L"
using εpos by (simp add: ym_def)
have Lyp: "L < yp"
using εpos by (simp add: yp_def)
define Km Kp where "Km = 1 - GPD_cdf γ 0 1 ym" and "Kp = 1 - GPD_cdf γ 0 1 yp"
have Km_gt: "q < Km"
unfolding Km_def q_def
using ym0 ymL by (intro GPD_tail_gt_level[OF x]) (auto simp: L_def)
have Kp_lt: "Kp < q"
unfolding Kp_def q_def
using Lyp by (intro GPD_tail_lt_level[OF x]) (simp add: L_def)
have Kp0: "0 ≤ Kp"
using GPD_cdf_le_1
unfolding Kp_def by simp
define δ where "δ = min ((q - Kp) / 2) ((Km - q) / 2)"
have δ1: "δ ≤ (q - Kp) / 2"
unfolding δ_def by (rule min.cobounded1)
have δ2: "δ ≤ (Km - q) / 2"
unfolding δ_def by (rule min.cobounded2)
have δpos: "0 < δ"
using Kp_lt Km_gt by (simp add: δ_def)
have Kpδ: "Kp + δ ≤ q"
proof -
have "2 * (Kp + δ) ≤ 2 * Kp + (q - Kp)"
using δ1 by simp
also have "... ≤ 2 * q"
using Kp_lt by simp
finally show ?thesis
by simp
qed
have Kmδ: "q < Km - δ"
proof -
have "2 * δ ≤ Km - q"
using δ2 by simp
hence "2 * q < 2 * (Km - δ)"
using Km_gt by simp
thus ?thesis
by simp
qed
have Kmδpos: "0 < Km - δ"
using Kmδ qpos by linarith
define r where "r = q / (Km - δ)"
have r_lt1: "r < 1"
unfolding r_def using Kmδ Kmδpos by simp
define ζ where "ζ = (1 - r) / 2"
have ζpos: "0 < ζ"
using r_lt1 by (simp add: ζ_def)
have rζ: "r < 1 - ζ"
proof -
have "1 - ζ = (1 + r) / 2"
by (simp add: ζ_def field_simps)
moreover have "r < (1 + r) / 2"
using r_lt1 by simp
ultimately show ?thesis
by simp
qed
have key: "q < (Km - δ) * (1 - ζ)"
proof -
have "(Km - δ) * r = q"
using Kmδpos by (simp add: r_def)
moreover have "(Km - δ) * r < (Km - δ) * (1 - ζ)"
using rζ Kmδpos by (intro mult_strict_left_mono) auto
ultimately show ?thesis
by simp
qed
define Q where
"Q = (λt. F t < 1 ∧ (∀y≥0. ¦excess_cdf F t (β t * y) - GPD_cdf γ 0 1 y¦ < δ))"
have evQ: "∀⇩F s in at_top. Q (tail_quantile F s)"
unfolding Q_def
by (intro eventually_compose_filterlim[OF excess_uniform_eventually[OF F ul δpos]]
Uendpoint)
have evP1: "∀⇩F s in at_top. 1 - ζ < s * (1 - F (tail_quantile F s))"
using order_tendstoD(1)[OF P1, of "1 - ζ"] ζpos by simp
have evx: "∀⇩F s::real in at_top. 1 < s * x"
using x by real_asymp
show "∀⇩F s in at_top. ¦(tail_quantile F (s * x) - tail_quantile F s)
/ β (tail_quantile F s)
- (if γ = 0 then ln x else (x powr γ - 1) / γ)¦ < e"
using evQ evP1 evx eventually_gt_at_top[of 1]
proof eventually_elim
case (elim s)
define t0 where "t0 = tail_quantile F s"
have s1: "1 < s" and sx1: "1 < s * x"
using elim(3,4) by simp_all
have spos: "0 < s"
using s1 by simp
have qs: "q / s = 1 / (s * x)"
using xpos spos by (simp add: q_def field_simps)
have βt: "0 < β t0"
by (rule βpos)
have Ft0: "F t0 < 1"
using elim(1) by (simp add: Q_def t0_def)
have Ft0pos: "0 < 1 - F t0"
using Ft0 by simp
have near: "¦excess_cdf F t0 (β t0 * y) - GPD_cdf γ 0 1 y¦ < δ" if "0 ≤ y" for y
using elim(1) that by (simp add: Q_def t0_def)
have factor: "1 - F (t0 + h) = (1 - excess_cdf F t0 h) * (1 - F t0)" for h
using Ft0 by (simp add: excess_cdf_def)
have upper_tail: "1 - F t0 ≤ 1 / s"
using lt_tail_quantile_iff[OF F s1, of "tail_quantile F s"] by (simp add: t0_def)
have lower_tail: "1 - ζ < s * (1 - F t0)"
using elim(2) by (simp add: t0_def)
have p_bounds: "0 < 1 - 1 / (s * x)" "1 - 1 / (s * x) < 1"
using sx1 by simp_all
have Uup: "tail_quantile F (s * x) ≤ t0 + β t0 * yp"
proof -
have "¦excess_cdf F t0 (β t0 * yp) - GPD_cdf γ 0 1 yp¦ < δ"
using ym0 εpos by (intro near) (simp add: yp_def ym_def)
hence "1 - excess_cdf F t0 (β t0 * yp) < Kp + δ"
by (simp add: Kp_def)
hence step1: "1 - F (t0 + β t0 * yp) < (Kp + δ) * (1 - F t0)"
using Ft0pos factor[of "β t0 * yp"] by (simp add: mult_strict_right_mono)
have step2: "(Kp + δ) * (1 - F t0) ≤ q * (1 / s)"
using Kpδ upper_tail Ft0pos qpos by (intro mult_mono) auto
have step3: "q * (1 / s) = 1 / (s * x)"
using qs by simp
have "1 - F (t0 + β t0 * yp) ≤ 1 / (s * x)"
using step1 step2 step3 by simp
hence "1 - 1 / (s * x) ≤ F (t0 + β t0 * yp)"
by simp
thus ?thesis
using right_continuous_mono.ginv_le_iff[OF F p_bounds, of "t0 + β t0 * yp"] by simp
qed
have Ulo: "t0 + β t0 * ym < tail_quantile F (s * x)"
proof -
have "¦excess_cdf F t0 (β t0 * ym) - GPD_cdf γ 0 1 ym¦ < δ"
using ym0 by (intro near) simp
hence "Km - δ < 1 - excess_cdf F t0 (β t0 * ym)"
by (simp add: Km_def)
hence "(Km - δ) * (1 - F t0) < 1 - F (t0 + β t0 * ym)"
using Ft0pos factor[of "β t0 * ym"] by (simp add: mult_strict_right_mono)
hence "s * ((Km - δ) * (1 - F t0)) < s * (1 - F (t0 + β t0 * ym))"
using spos by (intro mult_strict_left_mono) auto
moreover have "q < s * ((Km - δ) * (1 - F t0))"
using key mult_strict_left_mono[OF lower_tail Kmδpos] by (simp add: algebra_simps)
ultimately have "q < s * (1 - F (t0 + β t0 * ym))"
by simp
hence "q / s < 1 - F (t0 + β t0 * ym)"
using spos by (simp add: divide_less_eq mult.commute)
hence "1 / (s * x) < 1 - F (t0 + β t0 * ym)"
using qs by simp
thus ?thesis
using right_continuous_mono.ginv_le_iff[OF F p_bounds, of "t0 + β t0 * ym"]
by linarith
qed
have "ym < (tail_quantile F (s * x) - t0) / β t0"
using Ulo βt by (simp add: field_simps)
moreover have "(tail_quantile F (s * x) - t0) / β t0 ≤ yp"
using Uup βt by (simp add: field_simps)
ultimately show ?case
using εe by (simp add: t0_def ym_def yp_def L_def abs_real_def)
qed
qed
qed
lemma GPD_level_mult:
fixes γ y :: real
assumes y: "0 < y"
shows "(if γ = 0 then ln (2 * y) else ((2 * y) powr γ - 1) / γ)
- (if γ = 0 then ln y else (y powr γ - 1) / γ)
= y powr γ * (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)"
proof (cases "γ = 0")
next
case False
have "(2 * y) powr γ = 2 powr γ * y powr γ"
using y by (simp add: powr_mult)
thus ?thesis
using False by (simp add: field_simps)
qed(use y in "simp add: ln_mult")
lemma GPD_level_inverse:
fixes γ x :: real
assumes x: "0 < x"
shows "- ((if γ = 0 then ln (1 / x) else ((1 / x) powr γ - 1) / γ) * x powr γ)
= (if γ = 0 then ln x else (x powr γ - 1) / γ)"
proof (cases "γ = 0")
case True
thus ?thesis
using x by (simp add: ln_div)
next
case False
have xpowr: "0 < x powr γ"
using x by simp
have "- ((if γ = 0 then ln (1 / x) else ((1 / x) powr γ - 1) / γ) * x powr γ)
= - ((1 / x powr γ - 1) / γ * x powr γ)"
using False by (simp add: divide_inverse inverse_powr)
also have "... = - ((1 - x powr γ) / γ)"
using xpowr False by (simp add: field_simps)
also have "... = (if γ = 0 then ln x else (x powr γ - 1) / γ)"
using False by (simp add: field_simps)
finally show ?thesis .
qed
lemma tail_quantile_gap_of_excess_all:
fixes F :: "real ⇒ real" and β :: "real ⇒ real"
assumes F: "right_continuous_mono F 0 1" and βpos: "⋀u. 0 < β u"
and ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
and x: "0 < x"
shows "((λs. (tail_quantile F (s * x) - tail_quantile F s) / β (tail_quantile F s))
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
proof -
define U where "U = tail_quantile F"
define a where "a = (λs. β (tail_quantile F s))"
have apos: "0 < a s" for s
by (simp add: a_def βpos)
have anz: "a s ≠ 0" for s
using apos[of s] by simp
have Q: "((λs. (U (s * y) - U s) / a s)
⤏ (if γ = 0 then ln y else (y powr γ - 1) / γ)) at_top" if "1 < y" for y
using tail_quantile_gap_of_excess[OF F βpos ul that] by (simp add: U_def a_def)
have L2pos: "0 < (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)"
by (intro GPD_level_pos) simp
have shift: "filterlim (λs::real. s * y) at_top at_top" if "0 < y" for y
using that by real_asymp
have RV: "((λs. a (s * y) / a s) ⤏ y powr γ) at_top" if y: "1 < y" for y
proof -
have ypos: "0 < y"
using y by simp
have Q2y: "((λs. (U (s * (2 * y)) - U s) / a s)
⤏ (if γ = 0 then ln (2 * y) else ((2 * y) powr γ - 1) / γ)) at_top"
using y by (intro Q) simp
have eq: "(U (s * (2 * y)) - U s) / a s - (U (s * y) - U s) / a s
= (U (s * y * 2) - U (s * y)) / a s" for s
proof -
have arg: "s * (2 * y) = s * y * 2"
by (simp add: algebra_simps)
have "(U (s * (2 * y)) - U s) / a s - (U (s * y) - U s) / a s
= ((U (s * (2 * y)) - U s) - (U (s * y) - U s)) / a s"
by (simp add: diff_divide_distrib)
also have "... = (U (s * (2 * y)) - U (s * y)) / a s"
by simp
finally show ?thesis
by (simp add: arg)
qed
have Ndiff: "((λs. (U (s * y * 2) - U (s * y)) / a s)
⤏ (if γ = 0 then ln (2 * y) else ((2 * y) powr γ - 1) / γ)
- (if γ = 0 then ln y else (y powr γ - 1) / γ)) at_top"
proof -
have "((λs. (U (s * (2 * y)) - U s) / a s - (U (s * y) - U s) / a s)
⤏ (if γ = 0 then ln (2 * y) else ((2 * y) powr γ - 1) / γ)
- (if γ = 0 then ln y else (y powr γ - 1) / γ)) at_top"
by (intro tendsto_diff Q2y Q y)
thus ?thesis
by (simp add: eq)
qed
have D: "((λs. (U (s * y * 2) - U (s * y)) / a (s * y))
⤏ (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)) at_top"
proof -
have "((λr. (U (r * 2) - U r) / a r)
⤏ (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)) at_top"
by (intro Q) simp
from filterlim_compose[OF this shift[OF ypos]] show ?thesis
by (simp add: comp_def)
qed
have Dpos: "∀⇩F s in at_top. 0 < (U (s * y * 2) - U (s * y)) / a (s * y)"
by (rule order_tendstoD(1)[OF D L2pos])
have "((λs. ((U (s * y * 2) - U (s * y)) / a s)
/ ((U (s * y * 2) - U (s * y)) / a (s * y)))
⤏ ((if γ = 0 then ln (2 * y) else ((2 * y) powr γ - 1) / γ)
- (if γ = 0 then ln y else (y powr γ - 1) / γ))
/ (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)) at_top"
using L2pos by (intro tendsto_divide Ndiff D) simp
moreover have "∀⇩F s in at_top. ((U (s * y * 2) - U (s * y)) / a s)
/ ((U (s * y * 2) - U (s * y)) / a (s * y)) = a (s * y) / a s"
using apos anz
by (auto intro!: eventually_mono[OF Dpos] simp: zero_less_divide_iff field_simps)
ultimately have "((λs. a (s * y) / a s)
⤏ ((if γ = 0 then ln (2 * y) else ((2 * y) powr γ - 1) / γ)
- (if γ = 0 then ln y else (y powr γ - 1) / γ))
/ (if γ = 0 then ln 2 else (2 powr γ - 1) / γ)) at_top"
by (rule Lim_transform_eventually)
thus ?thesis
using GPD_level_mult[OF ypos, of γ] L2pos by simp
qed
have RVall: "((λs. a (s * y) / a s) ⤏ y powr γ) at_top" if y: "0 < y" for y
proof (cases "1 < y")
case True
thus ?thesis
by (rule RV)
next
case notgt: False
show ?thesis
proof (cases "y = 1")
case True
thus ?thesis
using anz by simp
next
case ne: False
have ylt: "y < 1"
using notgt ne by simp
define μ where "μ = 1 / y"
have μ1: "1 < μ"
using y ylt by (simp add: μ_def)
have "((λr. a (r * μ) / a r) ⤏ μ powr γ) at_top"
by (rule RV[OF μ1])
from filterlim_compose[OF this shift[OF y]]
have "((λs. a (s * y * μ) / a (s * y)) ⤏ μ powr γ) at_top"
by (simp add: comp_def)
moreover have "s * y * μ = s" for s
using y by (simp add: μ_def)
ultimately have inv: "((λs. a s / a (s * y)) ⤏ μ powr γ) at_top"
by simp
have ypowr: "0 < y powr γ"
using y by simp
have μpowr: "μ powr γ = 1 / y powr γ"
using y by (simp add: μ_def divide_inverse inverse_powr)
have μnz: "μ powr γ ≠ 0"
using μ1 by simp
from tendsto_inverse[OF inv μnz]
have "((λs. inverse (a s / a (s * y))) ⤏ inverse (μ powr γ)) at_top" .
moreover have "inverse (a s / a (s * y)) = a (s * y) / a s" for s
by (simp add: inverse_eq_divide)
moreover have "inverse (μ powr γ) = y powr γ"
using ypowr by (simp add: μpowr)
ultimately show ?thesis
by simp
qed
qed
have res: "((λs. (U (s * x) - U s) / a s)
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
proof (cases "1 < x")
case True
thus ?thesis
by (rule Q)
next
case notgt: False
show ?thesis
proof (cases "x = 1")
case True
thus ?thesis
by simp
next
case ne: False
have xlt: "x < 1"
using notgt ne by simp
define μ where "μ = 1 / x"
have μ1: "1 < μ"
using x xlt by (simp add: μ_def)
have "((λr. (U (r * μ) - U r) / a r)
⤏ (if γ = 0 then ln μ else (μ powr γ - 1) / γ)) at_top"
by (rule Q[OF μ1])
from filterlim_compose[OF this shift[OF x]]
have "((λs. (U (s * x * μ) - U (s * x)) / a (s * x))
⤏ (if γ = 0 then ln μ else (μ powr γ - 1) / γ)) at_top"
by (simp add: comp_def)
moreover have "s * x * μ = s" for s
using x by (simp add: μ_def)
ultimately have A: "((λs. (U s - U (s * x)) / a (s * x))
⤏ (if γ = 0 then ln μ else (μ powr γ - 1) / γ)) at_top"
by simp
note B = RVall[OF x]
from tendsto_mult[OF A B]
have "((λs. ((U s - U (s * x)) / a (s * x)) * (a (s * x) / a s))
⤏ (if γ = 0 then ln μ else (μ powr γ - 1) / γ) * x powr γ) at_top" .
moreover have "((U s - U (s * x)) / a (s * x)) * (a (s * x) / a s)
= - ((U (s * x) - U s) / a s)" for s
using anz by (simp add: field_simps)
ultimately have "((λs. - ((U (s * x) - U s) / a s))
⤏ (if γ = 0 then ln μ else (μ powr γ - 1) / γ) * x powr γ) at_top"
by simp
from tendsto_minus[OF this]
have "((λs. (U (s * x) - U s) / a s)
⤏ - ((if γ = 0 then ln μ else (μ powr γ - 1) / γ) * x powr γ)) at_top"
by simp
moreover have "- ((if γ = 0 then ln μ else (μ powr γ - 1) / γ) * x powr γ)
= (if γ = 0 then ln x else (x powr γ - 1) / γ)"
unfolding μ_def by (rule GPD_level_inverse[OF x])
ultimately show ?thesis
by simp
qed
qed
thus ?thesis
by (simp add: U_def a_def)
qed
theorem Pickands_Balkema_de_Haan_converse:
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and hyp: "∃β. (∀u. 0 < β u) ∧
uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x)
(λx. 0) (endpoint_filter F)"
shows "domain_of_attraction F (EVD_cdf γ 0 1)"
proof -
obtain β where βpos: "⋀u. 0 < β u"
and ul0: "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0)
(endpoint_filter F)"
using hyp by blast
have iff: "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0)
(endpoint_filter F)
⟷ uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
by (intro excess_uniform_scaled_iff βpos)
have ul: "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(endpoint_filter F)"
using iff ul0 by simp
have "∃a. (∀t. 0 < a t) ∧
(∀x>0. ((λt. (tail_quantile F (t * x) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top)"
proof (intro exI[of _ "λs. β (tail_quantile F s)"] conjI allI impI)
show "⋀t. 0 < β (tail_quantile F t)"
by (rule βpos)
next
fix x :: real
assume xpos: "0 < x"
show "((λt. (tail_quantile F (t * x) - tail_quantile F t) / β (tail_quantile F t))
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
by (rule tail_quantile_gap_of_excess_all[OF F βpos ul xpos])
qed
thus ?thesis
using MDA_iff_tail_quantile'[OF F, of γ] by simp
qed
theorem Pickands_Balkema_de_Haan:
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
shows "domain_of_attraction F (EVD_cdf γ 0 1)
⟷ (∃β. (∀u. 0 < β u) ∧
uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x)
(λx. 0) (endpoint_filter F))"
using Pickands_Balkema_de_Haan_forward[OF F] Pickands_Balkema_de_Haan_converse[OF F]
by blast
subsubsection ‹Explicit Choice of $\beta$›
lemma excess_uniform_beta_cong:
fixes F :: "real ⇒ real" and β β' :: "real ⇒ real" and FF :: "real filter"
assumes ul: "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0) FF"
and ev: "∀⇩F u in FF. β' u = β u"
shows "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β' u) x) (λx. 0) FF"
proof (rule uniform_limitI)
fix ε :: real
assume ε: "0 < ε"
show "∀⇩F u in FF. ∀x∈{0..}. dist (excess_cdf F u x - GPD_cdf γ 0 (β' u) x) 0 < ε"
using uniform_limitD[OF ul ε] ev by eventually_elim simp
qed
text ‹Case: $\gamma > 0$›
theorem Pickands_Balkema_de_Haan_pos:
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1" and γ: "0 < γ"
and dom: "domain_of_attraction F (EVD_cdf γ 0 1)"
shows "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (γ * u) x) (λx. 0)
(endpoint_filter F)"
proof -
have unbdd: "∀x. F x < 1" and rv: "regularly_varying (λx. 1 - F x) (- 1 / γ)"
using MDA_regularly_varying_pos[OF F γ] dom by auto
have nbdd: "¬ bdd_support F"
by (rule not_bdd_supportI') (use unbdd in simp)
note ef = endpoint_filter(2)[OF nbdd]
define β where "β = (λu::real. γ * max u 1)"
have βpos: "0 < β u" for u
using γ by (simp add: β_def)
have βeq: "∀⇩F u in at_top. β u = γ * u"
using eventually_ge_at_top[of "1::real"] by eventually_elim (simp add: β_def)
have pconv: "((λu. excess_cdf F u (β u * x)) ⤏ GPD_cdf γ 0 1 x) at_top" if x: "0 ≤ x" for x
proof -
have xnn: "0 ≤ γ * x"
using γ x by simp
have cpos: "0 < 1 + γ * x"
using xnn by simp
have "((λu. (1 - F (u * (1 + γ * x))) / (1 - F u)) ⤏ (1 + γ * x) powr (- 1 / γ)) at_top"
by (rule regularly_varying_lim[OF rv cpos])
from tendsto_diff[OF tendsto_const[of 1] this]
have lim: "((λu. 1 - (1 - F (u * (1 + γ * x))) / (1 - F u))
⤏ 1 - (1 + γ * x) powr (- 1 / γ)) at_top" .
have eq: "∀⇩F u in at_top. 1 - (1 - F (u * (1 + γ * x))) / (1 - F u)
= excess_cdf F u (β u * x)"
using βeq by eventually_elim (simp add: excess_cdf_def field_simps)
have m1: "- 1 ≤ γ * x"
using xnn by simp
have target: "GPD_cdf γ 0 1 x = 1 - (1 + γ * x) powr (- 1 / γ)"
using x γ m1 by (simp add: GPD_cdf_def)
show ?thesis
using Lim_transform_eventually[OF lim eq] target by simp
qed
have "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1) at_top"
by (intro excess_pointwise_imp_uniform[OF F βpos] pconv)
hence "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0) at_top"
using excess_uniform_scaled_iff[OF βpos] by simp
moreover have βeq': "∀⇩F u in at_top. γ * u = β u"
using βeq by eventually_elim simp
ultimately show ?thesis
using excess_uniform_beta_cong by (simp add: ef)
qed
text ‹Case: $\gamma < 0$›
theorem Pickands_Balkema_de_Haan_neg:
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1" and γ: "γ < 0"
and dom: "domain_of_attraction F (EVD_cdf γ 0 1)"
shows "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (- γ * (x_star F - u)) x)
(λx. 0) (endpoint_filter F)"
proof -
have bdd: "bdd_support F" and rv: "regularly_varying (λs. 1 - F (x_star F - 1 / s)) (1 / γ)"
using MDA_regularly_varying_neg[OF F γ] dom by auto
note ef = endpoint_filter(1)[OF bdd]
have evlt: "∀⇩F u in at_left (x_star F). u < x_star F"
by (auto simp: eventually_at_filter)
define β where "β = (λu::real. if u < x_star F then - γ * (x_star F - u) else 1)"
have βpos: "0 < β u" for u
using γ by (auto simp: β_def intro!: mult_neg_pos)
have βeq: "∀⇩F u in at_left (x_star F). β u = - γ * (x_star F - u)"
using evlt by eventually_elim (simp add: β_def)
have stop: "filterlim (λu. 1 / (x_star F - u)) at_top (at_left (x_star F))"
proof -
have tend: "((λu::real. x_star F - u) ⤏ 0) (at_left (x_star F))"
by (auto intro!: tendsto_eq_intros)
have "filterlim (λu. inverse (x_star F - u)) at_top (at_left (x_star F))"
by (intro filterlim_inverse_at_top[OF tend] eventually_mono[OF evlt]) simp
thus ?thesis
by (simp add: inverse_eq_divide)
qed
have pconv: "((λu. excess_cdf F u (β u * x)) ⤏ GPD_cdf γ 0 1 x) (at_left (x_star F))"
if x: "0 ≤ x" for x
proof (cases "0 < 1 + γ * x")
case supp: True
hence m1: "- 1 ≤ γ * x"
by simp
have cpos: "0 < 1 / (1 + γ * x)"
using supp by simp
have "((λs. (1 - F (x_star F - 1 / (s * (1 / (1 + γ * x)))))
/ (1 - F (x_star F - 1 / s))) ⤏ (1 / (1 + γ * x)) powr (1 / γ)) at_top"
by (rule regularly_varying_lim[OF rv cpos])
from filterlim_compose[OF this stop]
have lim0: "((λu. (1 - F (x_star F - 1 / (1 / (x_star F - u) * (1 / (1 + γ * x)))))
/ (1 - F (x_star F - 1 / (1 / (x_star F - u)))))
⤏ (1 / (1 + γ * x)) powr (1 / γ)) (at_left (x_star F))"
by simp
have eq0: "∀⇩F u in at_left (x_star F).
(1 - F (x_star F - 1 / (1 / (x_star F - u) * (1 / (1 + γ * x)))))
/ (1 - F (x_star F - 1 / (1 / (x_star F - u))))
= (1 - F (u + β u * x)) / (1 - F u)"
using evlt βeq
proof eventually_elim
case (elim u)
hence gap: "0 < x_star F - u"
by simp
have "1 / (1 / (x_star F - u) * (1 / (1 + γ * x))) = (x_star F - u) * (1 + γ * x)"
using gap supp by (simp add: field_simps)
moreover have "x_star F - (x_star F - u) * (1 + γ * x) = u + β u * x"
unfolding elim(2) by (simp add: algebra_simps)
moreover have "x_star F - 1 / (1 / (x_star F - u)) = u"
using gap by simp
ultimately show ?case
by simp
qed
have lim: "((λu. (1 - F (u + β u * x)) / (1 - F u))
⤏ (1 / (1 + γ * x)) powr (1 / γ)) (at_left (x_star F))"
by (rule Lim_transform_eventually[OF lim0 eq0])
have powr_eq: "(1 / (1 + γ * x)) powr (1 / γ) = (1 + γ * x) powr (- 1 / γ)"
using supp by (simp add: powr_divide powr_minus divide_inverse inverse_powr)
from tendsto_diff[OF tendsto_const[of 1] lim]
have "((λu. 1 - (1 - F (u + β u * x)) / (1 - F u))
⤏ 1 - (1 + γ * x) powr (- 1 / γ)) (at_left (x_star F))"
by (simp add: powr_eq)
moreover have "GPD_cdf γ 0 1 x = 1 - (1 + γ * x) powr (- 1 / γ)"
using x γ m1 by (simp add: GPD_cdf_def)
ultimately show ?thesis
by (simp add: excess_cdf_def)
next
case False
hence supp: "1 + γ * x ≤ 0"
by simp
have "∀⇩F u in at_left (x_star F). excess_cdf F u (β u * x) = 1"
using evlt βeq
proof eventually_elim
case (elim u)
hence gap: "0 < x_star F - u"
by simp
have "(x_star F - u) * (1 + γ * x) ≤ 0"
using gap supp by (simp add: mult_nonneg_nonpos less_imp_le)
hence "x_star F ≤ u + - γ * (x_star F - u) * x"
by (simp add: algebra_simps)
hence "x_star F ≤ u + β u * x"
unfolding elim(2) by simp
thus ?case
by (rule excess_cdf_eq_1_beyond_support[OF F bdd])
qed
moreover have "GPD_cdf γ 0 1 x = 1"
using x γ supp by (auto simp: GPD_cdf_def)
ultimately show ?thesis
by (simp add: tendsto_eventually)
qed
have "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1)
(at_left (x_star F))"
by (intro excess_pointwise_imp_uniform[OF F βpos] pconv)
hence "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (β u) x) (λx. 0)
(at_left (x_star F))"
using excess_uniform_scaled_iff[OF βpos] by simp
moreover have "∀⇩F u in at_left (x_star F). - γ * (x_star F - u) = β u"
using βeq by eventually_elim simp
ultimately show ?thesis
using excess_uniform_beta_cong by (simp add: ef)
qed
text ‹Case: arbitrary $\gamma$›
lemma isCont_GPD_level:
fixes γ y :: real
assumes y: "0 < y"
shows "isCont (λz. if γ = 0 then ln z else (z powr γ - 1) / γ) y"
using y by (cases "γ = 0") (auto intro!: isCont_ln isCont_divide isCont_diff continuous_powr)
lemma tail_quantile_witness_of_gap:
fixes F a :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and apos: "⋀t. 0 < a t"
and quant: "⋀y. 0 < y ⟹ ((λt. (tail_quantile F (t * y) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln y else (y powr γ - 1) / γ)) at_top"
shows "(λn. F (a (real n) * x + tail_quantile F (real n)) ^ n) ⇢ EVD_cdf γ 0 1 x"
proof (rule MDA_tail_quantile_witness[where b = "tail_quantile F", OF F apos zero_less_one])
fix y :: real
assume y: "0 < y"
show "((λt. (tail_quantile F (t * y) - tail_quantile F t) / a t)
⤏ (if γ = 0 then 1 * ln y + 0 else 1 * (y powr γ - 1) / γ + 0)) at_top"
using quant[OF y] by (cases "γ = 0") simp_all
qed
lemma t_div_a_tendsto_zero_endpoint:
fixes F a :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and apos: "⋀t. 0 < a t"
and quant: "⋀y. 0 < y ⟹ ((λt. (tail_quantile F (t * y) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln y else (y powr γ - 1) / γ)) at_top"
shows "((λt. (t - tail_quantile F (1 / (1 - F t))) / a (1 / (1 - F t))) ⤏ 0)
(endpoint_filter F)"
proof -
define s where "s = (λt::real. 1 / (1 - F t))"
have goal_eq: "(λt. (t - tail_quantile F (1 / (1 - F t))) / a (1 / (1 - F t)))
= (λt. (t - tail_quantile F (s t)) / a (s t))"
by (simp add: s_def)
have stop: "filterlim s at_top (endpoint_filter F)"
unfolding s_def
by (rule s_tendsto_at_top_endpoint[where a = "λn. a (real n)"
and b = "λn. tail_quantile F (real n)", OF F _ zero_less_one
tail_quantile_witness_of_gap[OF F apos quant]])
(use apos in simp)
note Flt1 = F_lt_1_endpoint[OF F]
have spos: "∀⇩F t in endpoint_filter F. 0 < s t"
using stop[unfolded filterlim_at_top_dense, rule_format, of 0] by simp
have conv: "((λt. (tail_quantile F (s t * y') - tail_quantile F (s t)) / a (s t))
⤏ (if γ = 0 then ln y' else (y' powr γ - 1) / γ))
(endpoint_filter F)" if y': "¦y' - 1¦ < 1" for y'
by (rule filterlim_compose[OF quant stop]) (use y' in simp)
have low: "∀⇩F t in endpoint_filter F.
(tail_quantile F (s t * y') - tail_quantile F (s t)) / a (s t)
≤ (t - tail_quantile F (s t)) / a (s t)"
if y': "(1::real) - 1 < y'" "y' < 1" for y'
using stop[unfolded filterlim_at_top_dense, rule_format, of "1 / y'"] spos Flt1
proof eventually_elim
case (elim t)
hence s_gt: "1 / y' < s t" and s_pos: "0 < s t" and Ft: "F t < 1"
by auto
have u1: "1 < s t * y'"
using mult_strict_right_mono[OF s_gt] y' by force
have u2: "s t * y' < 1 / (1 - F t)"
using mult_strict_left_mono[OF y'(2) s_pos] by (simp add: s_def)
show ?case
using apos[of "s t"] Ft u1 u2
by (auto intro!: divide_right_mono tail_quantile_le_of_lt_inv[OF F])
qed
have up: "∀⇩F t in endpoint_filter F. (t - tail_quantile F (s t)) / a (s t)
≤ (tail_quantile F (s t * y') - tail_quantile F (s t)) / a (s t)"
if y': "(1::real) < y'" "y' < 1 + 1" for y'
using spos Flt1
proof eventually_elim
case (elim t)
hence s_pos: "0 < s t" and Ft: "F t < 1"
by auto
have u: "1 / (1 - F t) < s t * y'"
using mult_strict_left_mono[OF _ s_pos] y' by (simp add: s_def)
show ?case
using apos[of "s t"]
by (auto intro!: divide_right_mono
less_imp_le[OF t_lt_tail_quantile_of_gt_inv[OF F Ft u]])
qed
have one: "(if γ = 0 then ln 1 else (1 powr γ - 1) / γ) = 0"
by simp
show ?thesis
using squeeze_tendsto_local[OF zero_less_one isCont_GPD_level[OF zero_less_one] conv low up]
unfolding goal_eq one .
qed
lemma divide_tail_of_gap:
fixes F a :: "real ⇒ real" and γ x :: real
assumes F: "right_continuous_mono F 0 1"
and apos: "⋀t. 0 < a t"
and quant: "⋀y. 0 < y ⟹ ((λt. (tail_quantile F (t * y) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln y else (y powr γ - 1) / γ)) at_top"
and x: "0 < 1 + γ * x"
shows "((λt. (1 - F (t + x * a (1 / (1 - F t)))) / (1 - F t))
⤏ - ln (EVD_cdf γ 0 1 x)) (endpoint_filter F)"
proof -
define s where "s = (λt::real. 1 / (1 - F t))"
define U where "U = tail_quantile F"
have goal_eq: "(λt. (1 - F (t + x * a (1 / (1 - F t)))) / (1 - F t))
= (λt. (1 - F (t + x * a (s t))) / (1 - F t))"
by (simp add: s_def)
have stop: "filterlim s at_top (endpoint_filter F)"
unfolding s_def
by (rule s_tendsto_at_top_endpoint[where a = "λn. a (real n)"
and b = "λn. tail_quantile F (real n)", OF F _ zero_less_one
tail_quantile_witness_of_gap[OF F apos quant]])
(use apos in simp)
note Flt1 = F_lt_1_endpoint[OF F]
have delta_tendsto: "((λt. (t - U (s t)) / a (s t)) ⤏ 0) (endpoint_filter F)"
using t_div_a_tendsto_zero_endpoint[OF F apos quant] by (simp add: s_def U_def)
have op: "open {x'. 0 < 1 + γ * x'}"
by (auto intro!: open_Collect_less continuous_on_add continuous_on_mult)
have "∀⇩F x' in nhds x. x' ∈ {x'. 0 < 1 + γ * x'}"
using x op by (intro eventually_nhds_in_open) auto
hence ev: "∀⇩F x' in nhds x. 0 < 1 + γ * x'"
by eventually_elim simp
then obtain η where eta: "0 < η"
and eta_supp: "⋀x'. ¦x' - x¦ < η ⟹ 0 < 1 + γ * x'"
using eventually_nhds_metric[of "λx'. 0 < 1 + γ * x'" x] by (auto simp: dist_real_def)
have Dcont: "isCont (λx'. ln (EVD_cdf γ 0 1 x')) x"
using EVD_cdf_supp_bounds[OF _ zero_less_one, of γ x 0] x
by (auto intro!: isCont_ln' isCont_EVD_cdf)
have conv: "((λt. - ((1 - F (a (s t) * x' + U (s t))) / (1 - F t)))
⤏ ln (EVD_cdf γ 0 1 x')) (endpoint_filter F)"
if x': "¦x' - x¦ < η" for x'
proof -
have supp': "0 < 1 + γ * x'"
using x' eta_supp by simp
have quant': "((λt. (tail_quantile F (t * y) - tail_quantile F t) / a t)
⤏ (if γ = 0 then 1 * ln y + 0 else 1 * (y powr γ - 1) / γ + 0)) at_top"
if y: "0 < y" for y
using quant[OF y] by (cases "γ = 0") simp_all
have base: "((λt. t * (1 - F (a t * x' + U t))) ⤏ - ln (EVD_cdf γ 0 1 x')) at_top"
unfolding U_def
by (intro MDA_tail_quantile_to_tail_probability[where b = "tail_quantile F",
OF F apos zero_less_one quant']) (use supp' in auto)
show ?thesis
using tendsto_minus[OF filterlim_compose[OF base stop]] by (simp add: s_def)
qed
have low: "∀⇩F t in endpoint_filter F. - ((1 - F (a (s t) * x' + U (s t))) / (1 - F t))
≤ - ((1 - F (t + x * a (s t))) / (1 - F t))"
if x': "x - η < x'" "x' < x" for x'
proof -
have dlt: "x' - x < 0"
using x' by simp
have ev1: "∀⇩F t in endpoint_filter F. x' - x < (t - U (s t)) / a (s t)"
using order_tendstoD(1)[OF delta_tendsto dlt] .
show ?thesis
using ev1 Flt1
proof eventually_elim
case (elim t)
hence d: "x' - x < (t - U (s t)) / a (s t)" and Ft: "F t < 1"
by auto
have apos': "0 < a (s t)"
using apos by simp
have "(x' - x) * a (s t) < ((t - U (s t)) / a (s t)) * a (s t)"
using mult_strict_right_mono[OF d apos'] .
also have "… = t - U (s t)"
using apos' by simp
finally have ineq: "(x' - x) * a (s t) < t - U (s t)" .
have "a (s t) * x' + U (s t) < t + x * a (s t)"
using ineq by (simp add: field_simps)
hence fmono: "F (a (s t) * x' + U (s t)) ≤ F (t + x * a (s t))"
by (intro monoD[OF right_continuous_mono.mono[OF F]]) simp
have "(1 - F (t + x * a (s t))) / (1 - F t)
≤ (1 - F (a (s t) * x' + U (s t))) / (1 - F t)"
using fmono Ft by (intro divide_right_mono) auto
thus ?case
by simp
qed
qed
have up: "∀⇩F t in endpoint_filter F. - ((1 - F (t + x * a (s t))) / (1 - F t))
≤ - ((1 - F (a (s t) * x' + U (s t))) / (1 - F t))"
if x': "x < x'" "x' < x + η" for x'
proof -
have dpos: "0 < x' - x"
using x' by simp
have ev1: "∀⇩F t in endpoint_filter F. (t - U (s t)) / a (s t) < x' - x"
using order_tendstoD(2)[OF delta_tendsto dpos] .
show ?thesis
using ev1 Flt1
proof eventually_elim
case (elim t)
hence d: "(t - U (s t)) / a (s t) < x' - x" and Ft: "F t < 1"
by auto
have apos': "0 < a (s t)"
using apos by simp
have "((t - U (s t)) / a (s t)) * a (s t) < (x' - x) * a (s t)"
using mult_strict_right_mono[OF d apos'] .
moreover have "((t - U (s t)) / a (s t)) * a (s t) = t - U (s t)"
using apos' by simp
ultimately have ineq: "t - U (s t) < (x' - x) * a (s t)"
by simp
have "t + x * a (s t) < a (s t) * x' + U (s t)"
using ineq by (simp add: field_simps)
hence fmono: "F (t + x * a (s t)) ≤ F (a (s t) * x' + U (s t))"
by (intro monoD[OF right_continuous_mono.mono[OF F]]) simp
have "(1 - F (a (s t) * x' + U (s t))) / (1 - F t)
≤ (1 - F (t + x * a (s t))) / (1 - F t)"
using fmono Ft by (intro divide_right_mono) auto
thus ?case
by simp
qed
qed
show ?thesis
unfolding goal_eq
using tendsto_minus[OF squeeze_tendsto_local[OF eta Dcont conv low up]] by simp
qed
theorem Pickands_Balkema_de_Haan_normalization:
fixes F a :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and apos: "⋀t. 0 < a t"
and quant: "⋀x. 0 < x ⟹ ((λt. (tail_quantile F (t * x) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
shows "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (a (1 / (1 - F u))) x)
(λx. 0) (endpoint_filter F)"
proof -
define β where "β = (λu. a (1 / (1 - F u)))"
have βpos: "0 < β u" for u
using apos by (simp add: β_def)
have pconv: "((λu. excess_cdf F u (β u * x)) ⤏ GPD_cdf γ 0 1 x) (endpoint_filter F)"
if x: "0 ≤ x" for x
by (rule excess_tendsto_of_divide_tail[OF F βpos _ x])
(use divide_tail_of_gap[OF F apos quant] in "simp add: β_def")
have "uniform_limit {0..} (λu x. excess_cdf F u (β u * x)) (GPD_cdf γ 0 1) (endpoint_filter F)"
by (intro excess_pointwise_imp_uniform[OF F βpos] pconv)
thus ?thesis
using excess_uniform_scaled_iff[OF βpos] by (simp add: β_def)
qed
corollary Pickands_Balkema_de_Haan_normalization':
fixes F :: "real ⇒ real" and γ :: real
assumes F: "right_continuous_mono F 0 1"
and dom: "domain_of_attraction F (EVD_cdf γ 0 1)"
obtains a :: "real ⇒ real"
where "⋀t. 0 < a t"
and "⋀x. 0 < x ⟹ ((λt. (tail_quantile F (t * x) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
and "⋀x. (λn. F (a (real n) * x + tail_quantile F (real n)) ^ n) ⇢ EVD_cdf γ 0 1 x"
and "uniform_limit {0..} (λu x. excess_cdf F u x - GPD_cdf γ 0 (a (1 / (1 - F u))) x)
(λx. 0) (endpoint_filter F)"
proof -
obtain a where apos: "⋀t. 0 < a t"
and quant0: "⋀x. 0 < x ⟹
((λt. (tail_quantile F (t * x) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
using dom MDA_iff_tail_quantile'[OF F, of γ] by auto
have quant: "⋀x. 0 < x ⟹ ((λt. (tail_quantile F (t * x) - tail_quantile F t) / a t)
⤏ (if γ = 0 then ln x else (x powr γ - 1) / γ)) at_top"
using quant0 by simp
show thesis
by (rule that[of a])
(use apos quant tail_quantile_witness_of_gap[OF F apos quant]
Pickands_Balkema_de_Haan_normalization[OF F apos quant] in blast)+
qed
end