Theory Pareto_Distribution
subsection ‹Generalized Pareto Distribution›
theory Pareto_Distribution
imports
Lemmas_EVT
Extreme_Value_Distribution
begin
text ‹We define the generalized Pareto distribution (GPD) density and cdf.›
definition GPD_density :: "[real, real, real, real] ⇒ real" where
"GPD_density ξ μ σ x ≡ if ξ = 0 then
if μ ≤ x then exp (- (x - μ) / σ) / σ else 0
else if ξ > 0 then
if μ ≤ x then ((1 + ξ * (x - μ) / σ) powr (- 1 - 1 / ξ)) / σ
else 0
else
if μ ≤ x ∧ x ≤ μ - σ / ξ then
((1 + ξ * (x - μ) / σ) powr (- 1 - 1 / ξ)) / σ
else 0"
lemma GPD_density_nonneg[simp]:"0 ≤ σ ⟹ 0 ≤ GPD_density ξ μ σ x"
by(simp add: GPD_density_def)
lemma GPD_density_measurable[measurable]:
"GPD_density ξ μ σ ∈ borel_measurable borel"
unfolding GPD_density_def by measurable
lemma GPD_density_eq_exponential_density:
"GPD_density 0 μ σ = (λx. exponential_density (1 / σ) (x - μ))"
by(auto simp: exponential_density_def GPD_density_def)
lemma GPD_density_xi_pos:
"0 < ξ ⟹ μ ≤ x
⟹ GPD_density ξ μ σ x = (1 + ξ * (x - μ) / σ) powr (- 1 - 1 / ξ) / σ"
by(simp add: GPD_density_def)
lemma GPD_density_xi_neg:
"ξ < 0 ⟹ μ ≤ x ⟹ x ≤ μ - σ / ξ
⟹ GPD_density ξ μ σ x = (1 + ξ * (x - μ) / σ) powr (- 1 - 1 / ξ) / σ"
by(simp add: GPD_density_def)
lemma GPD_density_eq_0:
"x < μ ⟹ GPD_density ξ μ σ x = 0"
by(simp add: GPD_density_def)
lemma GPD_density_xi_neg_eq_0:
"ξ < 0 ⟹ μ - σ / ξ < x ⟹ GPD_density ξ μ σ x = 0"
by(simp add: GPD_density_def)
lemma
fixes a μ σ :: real
assumes sigma[arith]:"0 < σ"
shows GPD_density_set_integrable0:"set_integrable lborel {..a} (GPD_density 0 μ σ)"
and GPD_density_set_integral0:
"(∫x∈{..a}. GPD_density 0 μ σ x ∂lborel) = (if a < μ then 0 else 1 - exp (- (a - μ) / σ))"
and GPD_density_set_nn_integral0:
"(∫⇧+x∈{..a}. GPD_density 0 μ σ x ∂lborel)
= ennreal (if a < μ then 0 else 1 - exp (- (a - μ) / σ))"
proof -
have *:" indicator {..a} (μ + x) = indicator {..a-μ} x" for x
by(auto simp: indicator_def)
have "(∫⇧+x∈{..a}. GPD_density 0 μ σ x ∂lborel)
= (∫⇧+x∈{..a - μ}. exponential_density (1 / σ) x ∂lborel)"
by(subst nn_integral_real_affine
[where t=μ and c=1 and f="λx. ennreal (GPD_density 0 μ σ x) * indicator {..a} x"])
(auto simp add: GPD_density_eq_exponential_density *)
also have "... = ennreal (if a < μ then 0 else 1 - exp (- (a - μ) / σ))"
by(simp add: nn_integral_erlang_density erlang_CDF_def minus_divide_left
del: minus_divide_left[symmetric])
finally show nn_eq: "(∫⇧+x∈{..a}. GPD_density 0 μ σ x ∂lborel)
= ennreal (if a < μ then 0 else 1 - exp (- (a - μ) / σ))" .
show integ0: "set_integrable lborel {..a} (GPD_density 0 μ σ)"
unfolding set_integrable_def
using nn_eq
by(auto intro!: integrableI_nn_integral_finite
[where x="if a < μ then 0 else 1 - exp (- (a - μ) / σ)"]
simp: ennreal_indicator ennreal_mult' mult.commute)
have nonneg: "0 ≤ (∫x∈{..a}. GPD_density 0 μ σ x ∂lborel)"
unfolding set_lebesgue_integral_def
by (rule Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
have "ennreal (∫x∈{..a}. GPD_density 0 μ σ x ∂lborel)
= (∫⇧+x. ennreal (indicat_real {..a} x *⇩R GPD_density 0 μ σ x) ∂lborel)"
unfolding set_lebesgue_integral_def
by (rule nn_integral_eq_integral[symmetric])
(use integ0[unfolded set_integrable_def] in ‹auto simp: indicator_def›)
also have "... = (∫⇧+x∈{..a}. GPD_density 0 μ σ x ∂lborel)"
by (simp add: ennreal_indicator ennreal_mult' mult.commute)
also have "... = ennreal (if a < μ then 0 else 1 - exp (- (a - μ) / σ))"
using nn_eq .
finally have eq: "ennreal (∫x∈{..a}. GPD_density 0 μ σ x ∂lborel)
= ennreal (if a < μ then 0 else 1 - exp (- (a - μ) / σ))" .
show "(∫x∈{..a}. GPD_density 0 μ σ x ∂lborel)
= (if a < μ then 0 else 1 - exp (- (a - μ) / σ))"
by(intro ennreal_inj[THEN iffD1,OF _ _ eq] nonneg)
(auto simp: divide_nonpos_pos)
qed
lemma
fixes a μ σ :: real
defines "y ≡ (a - μ) / σ"
assumes sigma[arith]:"0 < σ"
and amu:"a ≤ μ"
shows GPD_density_set_integrable2:"set_integrable lborel {..a} (GPD_density ξ μ σ)"
and GPD_density_set_integral2:"(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 0"
and GPD_density_set_nn_integral2:"(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 0"
proof -
have ae: "AE x in lborel. x ∈ {..a} ⟶ GPD_density ξ μ σ x = 0"
using amu by(intro AE_I[where N="{μ}"]) (auto intro!: GPD_density_eq_0)
show "set_integrable lborel {..a} (GPD_density ξ μ σ)"
unfolding set_integrable_def
by(rule integrable_cong_AE[where g="λx. 0", THEN iffD2])
(use ae in ‹auto elim!: eventually_mono simp: indicator_def›)
show "(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 0"
unfolding set_lebesgue_integral_def
by(subst integral_cong_AE[where g="λx. 0"])
(use ae in ‹auto elim!: eventually_mono simp: indicator_def›)
show "(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 0"
by(intro nn_integral_zero')
(use ae in ‹auto elim!: eventually_mono simp: indicator_def›)
qed
lemma
fixes a μ σ :: real
defines "y ≡ (a - μ) / σ"
assumes sigma[arith]:"0 < σ"
and xi:"ξ ≠ 0"
and mua:"μ ≤ a"
and xiy:"- 1 ≤ ξ * y"
shows GPD_density_set_integrable1:"set_integrable lborel {..a} (GPD_density ξ μ σ)"
and GPD_density_set_integral1:
"(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1 - (1 + ξ * y) powr (- 1 / ξ)"
and GPD_density_set_nn_integral1:
"(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel) = ennreal (1 - (1 + ξ * y) powr (- 1 / ξ))"
proof -
have main: "set_integrable lborel {..a} (GPD_density ξ μ σ) ∧
(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1 - (1 + ξ * y) powr (- 1 / ξ) ∧
(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel)
= ennreal (1 - (1 + ξ * y) powr (- 1 / ξ))"
proof(cases "μ < a")
assume "¬ μ < a"
with mua
have y0: "y = 0" and amu:"a ≤ μ"
by (simp_all add: y_def)
from GPD_density_set_integrable2[OF sigma amu] GPD_density_set_integral2[OF sigma amu]
GPD_density_set_nn_integral2[OF sigma amu]
show ?thesis
by (simp add: y0)
next
assume mua': "μ < a"
define g where "g ≡ λt. (1 + ξ * (t - μ) / σ) powr (- 1 - 1 / ξ) / σ"
define F where "F ≡ λt. - ((1 + ξ * (t - μ) / σ) powr (- 1 / ξ))"
have g_nonneg: "0 ≤ g t" for t
by (simp add: g_def)
have g_meas[measurable]: "g ∈ borel_measurable borel"
unfolding g_def by measurable
have Fmu: "F μ = - 1"
by (simp add: F_def)
have Fa: "F a = - ((1 + ξ * y) powr (- 1 / ξ))"
by (simp add: F_def y_def)
have pos: "0 < 1 + ξ * (t - μ) / σ" if t: "μ < t" "t < a" for t
proof(cases "0 < ξ")
case True
have "0 < ξ * (t - μ) / σ"
using t True by (intro divide_pos_pos mult_pos_pos) auto
thus ?thesis
by linarith
next
case False
with xi have xi_neg: "ξ < 0"
by simp
have "- σ ≤ ξ * (a - μ)"
using xiy sigma unfolding y_def by (simp add: pos_le_divide_eq)
moreover have "ξ * (a - μ) < ξ * (t - μ)"
using t xi_neg by (intro mult_strict_left_mono_neg) auto
ultimately have "- σ < ξ * (t - μ)"
by linarith
hence "- 1 < ξ * (t - μ) / σ"
using sigma by (simp add: pos_less_divide_eq)
thus ?thesis
by linarith
qed
have deriv: "(F has_real_derivative g t) (at t)" if t: "μ < t" "t < a" for t
using pos[OF t] xi sigma unfolding F_def g_def
by(auto intro!: derivative_eq_intros simp: field_simps) argo
have isCont_g: "isCont g t" if t: "μ < t" "t < a" for t
using pos[OF t] sigma unfolding g_def
by(intro continuous_intros) auto
have A: "(F ⤏ - 1) (at_right μ)"
proof -
have "isCont F μ"
unfolding F_def by(intro continuous_intros) auto
from continuous_at_imp_continuous_at_within[OF this]
show ?thesis
by (simp add: continuous_within Fmu)
qed
have B: "(F ⤏ F a) (at_left a)"
proof(cases "ξ * y = - 1")
case False
with xiy have "- 1 < ξ * ((a - μ) / σ)"
unfolding y_def by (auto simp: le_less)
hence pos_a: "0 < 1 + ξ * (a - μ) / σ"
by simp
have "isCont F a"
unfolding F_def using pos_a by(intro continuous_intros) auto
from continuous_at_imp_continuous_at_within[OF this]
show ?thesis
by (simp add: continuous_within)
next
case True
have xi_neg: "ξ < 0"
proof(rule ccontr)
assume "¬ ξ < 0"
with xi have "0 < ξ"
by simp
hence "0 ≤ ξ * y"
using mua by (auto intro: mult_nonneg_nonneg simp: y_def)
with True show False
by simp
qed
have p_pos: "0 < - 1 / ξ"
using xi_neg by (simp add: divide_pos_neg)
have base_a: "1 + ξ * (a - μ) / σ = 0"
using True by (simp add: y_def)
have Fa0: "F a = 0"
using xi by (simp add: F_def base_a)
have base0: "((λt. 1 + ξ * (t - μ) / σ) ⤏ 0) (at_left a)"
unfolding base_a[symmetric]
by (intro tendsto_intros) auto
have ev_nonneg: "∀⇩F t in at_left a. 0 ≤ 1 + ξ * (t - μ) / σ"
by (intro eventually_at_leftI[of μ]) (use pos[THEN less_imp_le] mua' in auto)
have "((λt. (1 + ξ * (t - μ) / σ) powr (- 1 / ξ)) ⤏ 0) (at_left a)"
by (rule tendsto_zero_powrI[OF base0 tendsto_const ev_nonneg p_pos])
hence "(F ⤏ - 0) (at_left a)"
unfolding F_def by (rule tendsto_minus)
thus ?thesis
by (simp add: Fa0)
qed
have FTC1: "set_integrable lborel (einterval (ereal μ) (ereal a)) g"
by (rule interval_integral_FTC_nonneg[where F=F and A="- 1" and B="F a"])
(use mua' deriv isCont_g g_nonneg A B in
‹auto simp: ereal_tendsto_simps›)
have FTC2: "interval_lebesgue_integral lborel (ereal μ) (ereal a) g = F a - (- 1)"
by (rule interval_integral_FTC_nonneg[where F=F])
(use mua' deriv isCont_g g_nonneg A B in
‹auto simp: ereal_tendsto_simps›)
have intg_oo: "set_integrable lborel {μ<..<a} g"
using FTC1 by simp
have int_oo: "(∫x∈{μ<..<a}. g x ∂lborel) = 1 - (1 + ξ * y) powr (- 1 / ξ)"
using FTC2 mua' by (simp add: interval_lebesgue_integral_def Fa)
have dens_eq: "GPD_density ξ μ σ t = g t" if t: "μ < t" "t < a" for t
proof(cases "0 < ξ")
case True
thus ?thesis
using t by (simp add: GPD_density_xi_pos g_def)
next
case False
with xi have xi_neg: "ξ < 0"
by simp
have "- σ ≤ ξ * (a - μ)"
using xiy sigma unfolding y_def by (simp add: pos_le_divide_eq)
moreover have "ξ * (a - μ) ≤ ξ * (t - μ)"
using t xi_neg by (intro mult_left_mono_neg) auto
ultimately have "- σ ≤ ξ * (t - μ)"
by linarith
from divide_right_mono_neg[OF this, of ξ] xi_neg xi
have "t - μ ≤ - σ / ξ"
by simp
thus ?thesis
using t xi_neg by (simp add: GPD_density_xi_neg g_def)
qed
have ae_eq: "AE x in lborel. indicat_real {..a} x *⇩R GPD_density ξ μ σ x
= indicat_real {μ<..<a} x *⇩R g x"
using AE_lborel_singleton[of μ] AE_lborel_singleton[of a]
proof eventually_elim
case (elim x)
consider "x < μ" | "μ < x" "x < a" | "a < x"
using elim mua' by argo
thus ?case
by cases (simp_all add: indicator_def GPD_density_eq_0 mua' less_le_not_le dens_eq)
qed
have intg: "set_integrable lborel {..a} (GPD_density ξ μ σ)"
proof -
have "integrable lborel (λx. indicat_real {..a} x *⇩R GPD_density ξ μ σ x)
⟷ integrable lborel (λx. indicat_real {μ<..<a} x *⇩R g x)"
using ae_eq by (intro integrable_cong_AE) auto
thus ?thesis
using intg_oo by (simp add: set_integrable_def)
qed
have integral_eq: "(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1 - (1 + ξ * y) powr (- 1 / ξ)"
proof -
have "(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel)
= (∫x. indicat_real {μ<..<a} x *⇩R g x ∂lborel)"
unfolding set_lebesgue_integral_def
using ae_eq by (intro integral_cong_AE) auto
also have "... = 1 - (1 + ξ * y) powr (- 1 / ξ)"
using int_oo by (simp add: set_lebesgue_integral_def)
finally show ?thesis .
qed
have nn_eq: "(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel)
= ennreal (1 - (1 + ξ * y) powr (- 1 / ξ))"
proof -
have "(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel)
= (∫⇧+x. ennreal (indicat_real {μ<..<a} x *⇩R g x) ∂lborel)"
using ae_eq by (intro nn_integral_cong_AE)
(auto elim!: eventually_mono simp: indicator_def)
also have "... = ennreal (∫x. indicat_real {μ<..<a} x *⇩R g x ∂lborel)"
by (intro nn_integral_eq_integral)
(use intg_oo g_nonneg in ‹auto simp: set_integrable_def indicator_def›)
also have "... = ennreal (1 - (1 + ξ * y) powr (- 1 / ξ))"
using int_oo by (simp add: set_lebesgue_integral_def)
finally show ?thesis .
qed
show ?thesis
using intg integral_eq nn_eq by blast
qed
from main show "set_integrable lborel {..a} (GPD_density ξ μ σ)"
and "(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1 - (1 + ξ * y) powr (- 1 / ξ)"
and "(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel)
= ennreal (1 - (1 + ξ * y) powr (- 1 / ξ))"
by blast+
qed
lemma
fixes a μ σ :: real
defines "y ≡ (a - μ) / σ"
assumes sigma[arith]:"0 < σ"
and xi:"ξ < 0"
and xiy:"ξ * y ≤ - 1"
shows GPD_density_set_integrable3:"set_integrable lborel {..a} (GPD_density ξ μ σ)"
and GPD_density_set_integral3:"(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1"
and GPD_density_set_nn_integral3:"(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1"
proof -
define b where "b ≡ μ - σ / ξ"
have ba: "b ≤ a"
using xiy xi sigma unfolding b_def y_def by (simp add: field_simps)
have yb1: "(b - μ) / σ = - 1 / ξ"
using xi sigma by (simp add: b_def field_simps)
have mub:"μ ≤ b"
using xi by(simp add: b_def divide_nonneg_neg)
have yb3: "- 1 ≤ ξ * ((b - μ) / σ)"
using xi by (simp add: yb1)
have base0: "1 + ξ * (b - μ) / σ = 0"
using xi sigma by (simp add: b_def field_simps)
have dens_b: "GPD_density ξ μ σ x = 0" if "b ≤ x" for x
proof(cases "x = b")
case True
have "b ≤ μ - σ / ξ"
by (simp add: b_def)
hence "GPD_density ξ μ σ b = (1 + ξ * (b - μ) / σ) powr (- 1 - 1 / ξ) / σ"
by (intro GPD_density_xi_neg[OF xi mub])
thus ?thesis
by (simp add: True base0)
next
case False
with that
have "b < x"
by simp
hence "μ - σ / ξ < x"
unfolding b_def by argo
thus ?thesis
by (intro GPD_density_xi_neg_eq_0[OF xi])
qed
have h1[simp]: "set_integrable lborel {..b} (GPD_density ξ μ σ)"
and h2: "(∫x∈{..b}. GPD_density ξ μ σ x ∂lborel) = 1"
and h3: "(∫⇧+x∈{..b}. GPD_density ξ μ σ x ∂lborel) = 1"
using GPD_density_set_integrable1[OF sigma less_imp_neq[OF xi] mub yb3]
GPD_density_set_integral1[OF sigma less_imp_neq[OF xi] mub yb3]
GPD_density_set_nn_integral1[OF sigma less_imp_neq[OF xi] mub yb3] xi
by (simp_all add: yb1)
have i2[simp]: "set_integrable lborel {b<..a} (GPD_density ξ μ σ)"
by(subst set_integrable_cong[where f'="λx. 0", OF refl refl]) (simp_all add: dens_b)
have eq0: "(∫x∈{b<..a}. GPD_density ξ μ σ x ∂lborel) = 0"
by(subst set_integral_cong[where g="λx. 0"]) (auto simp: dens_b)
have eq0': "(∫⇧+x∈{b<..a}. GPD_density ξ μ σ x ∂lborel) = 0"
by(subst set_nn_integral_cong[where g="λx. 0", OF refl refl]) (auto simp: dens_b)
show "set_integrable lborel {..a} (GPD_density ξ μ σ)"
using ba
by(subst set_integrable_cong[where A'="{..b} ∪ {b<..a}"])
(auto intro!: set_integrable_Un)
have "(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) =
(∫x∈{..b}. GPD_density ξ μ σ x ∂lborel) + (∫x∈{b<..a}. GPD_density ξ μ σ x ∂lborel)"
using ba
by(subst set_integral_Un[symmetric])
(auto intro!: arg_cong[where f="λB. set_lebesgue_integral lborel B _"])
also have "... = 1"
by (auto simp: h2 eq0)
finally show "(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1" .
have "(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel) =
(∫⇧+x. ennreal (GPD_density ξ μ σ x) * indicator {..b} x
+ ennreal (GPD_density ξ μ σ x) * indicator {b<..a} x ∂lborel)"
using ba by(auto intro!: nn_integral_cong simp: indicator_def)
also have "... = (∫⇧+x∈{..b}. GPD_density ξ μ σ x ∂lborel)"
using ba by(auto intro!: nn_integral_cong simp: indicator_def dens_b)
finally show "(∫⇧+x∈{..a}. GPD_density ξ μ σ x ∂lborel) = 1"
by(simp add: h3)
qed
lemma GPD_density_set_integrable:
assumes sigma[arith]:"0 < σ"
shows "set_integrable lborel {..a} (GPD_density ξ μ σ)"
proof -
consider "ξ = 0"
| "¬ ξ = 0" "a ≤ μ"
| "¬ ξ = 0" "μ ≤ a" "- 1 ≤ ξ * ((a - μ) / σ)"
| "¬ ξ = 0" "μ ≤ a" "ξ * ((a - μ) / σ) < - 1"
by argo
thus ?thesis
proof cases
case 1
thus ?thesis
using GPD_density_set_integrable0
by simp
next
case 2
thus ?thesis
by (intro GPD_density_set_integrable2[OF sigma])
thm GPD_density_set_integrable2[OF sigma]
next
case 3
thus ?thesis
by (intro GPD_density_set_integrable1[OF sigma])
next
case 4
hence xi_neg: "ξ < 0"
by (smt (verit, best) assms divide_nonneg_pos mult_nonneg_nonneg)
show ?thesis
by (intro GPD_density_set_integrable3[OF sigma xi_neg] less_imp_le 4)
qed
qed
abbreviation GPD_cdf where "GPD_cdf ≡ λξ μ σ x. cdf (density lborel (GPD_density ξ μ σ)) x"
lemma GPD_cdf_set_integral:
assumes sigma[arith]:"0 < σ"
shows "GPD_cdf ξ μ σ x = (∫t∈{..x}. GPD_density ξ μ σ t ∂lborel)"
unfolding cdf_def
by (intro measure_density_on GPD_density_set_integrable[OF sigma])
(auto simp: less_imp_le)
corollary GPD_cdf_def:
assumes sigma[arith]:"0 < σ"
shows "GPD_cdf ξ μ σ x =
(let y = (x - μ) / σ in
if ξ = 0 then
if x < μ then 0 else 1 - exp (- y)
else
if x < μ then 0
else if - 1 ≤ ξ * y then 1 - (1 + ξ * y) powr (- 1 / ξ)
else 1)"
proof -
consider "ξ = 0"
| "ξ ≠ 0" "x < μ"
| "ξ ≠ 0" "μ ≤ x" "- 1 ≤ ξ * ((x - μ) / σ)"
| "ξ ≠ 0" "μ ≤ x" "ξ * ((x - μ) / σ) < - 1"
by argo
thus ?thesis
proof cases
case 1
thus ?thesis
unfolding GPD_cdf_set_integral[OF sigma]
by(simp add: GPD_density_set_integral0 del: minus_diff_eq)
next
case 2
thus ?thesis
using GPD_density_set_integral2[OF sigma less_imp_le]
by (auto simp add: GPD_cdf_set_integral Let_def)
next
case 3
thus ?thesis
using GPD_density_set_integral1[OF sigma]
by (simp add: GPD_cdf_set_integral Let_def)
next
case 4
hence xi_neg: "ξ < 0"
by (smt (verit, best) assms mult_nonneg_nonneg zero_le_divide_iff)
show ?thesis
using GPD_density_set_integral3[OF sigma xi_neg less_imp_le] 4
by (simp add: GPD_cdf_set_integral Let_def)
qed
qed
lemma GPD_cdf_location_scale:
assumes sigma: "0 < σ"
shows "GPD_cdf γ 0 σ x = GPD_cdf γ 0 1 (x / σ)"
using sigma
by (simp add: GPD_cdf_def[OF sigma] GPD_cdf_def[OF zero_less_one] Let_def divide_less_0_iff)
lemma EVD_tail_eq_GPD_cdf:
assumes supp: "1 + γ * x > 0" and x: "0 ≤ x"
shows "- ln (EVD_cdf γ 0 1 x) = 1 - GPD_cdf γ 0 1 x"
using x supp
by (simp add: EVD_cdf_def[of 1] GPD_cdf_def[OF zero_less_one] Let_def)
lemma GPD_cdf_eq0:
assumes "x ≤ μ"
shows "GPD_cdf ξ μ σ x = 0"
proof -
have "GPD_cdf ξ μ σ x = enn2real (set_nn_integral lborel {..x} (GPD_density ξ μ σ))"
by(simp add: emeasure_density cdf_def measure_def)
also have "... = enn2real (set_nn_integral lborel {..x} (λy. 0))"
using assms
by(intro arg_cong[where f=enn2real] nn_integral_cong_AE AE_I'[where N="{x}"])
(auto simp: GPD_density_def indicator_def)
finally show ?thesis
by simp
qed
lemma GPD_cdf_at_bot_0: "(GPD_cdf ξ μ σ ⤏ 0) at_bot"
proof -
have "∀⇩F x in at_bot. GPD_cdf ξ μ σ x = 0"
using eventually_le_at_bot[of μ]
by eventually_elim (intro GPD_cdf_eq0)
thus ?thesis
by (rule tendsto_eventually)
qed
lemma GPD_cdf_at_top_1:
assumes sigma:"0 < σ"
shows "(GPD_cdf ξ μ σ ⤏ 1) at_top"
proof (cases "ξ = 0")
case True
have ev: "∀⇩F x in at_top. 1 - exp (- (x - μ) / σ) = GPD_cdf ξ μ σ x"
using eventually_ge_at_top[of μ]
by eventually_elim
(use True in "simp add: GPD_cdf_def[OF sigma] Let_def field_simps minus_divide_left")
have lim: "((λx. 1 - exp (- (x - μ) / σ)) ⤏ 1) at_top"
proof -
have "((λx. exp (- (x - μ) / σ)) ⤏ 0) at_top"
using sigma by real_asymp
from tendsto_diff[OF tendsto_const this]
show ?thesis
by simp
qed
show ?thesis
by (rule Lim_transform_eventually[OF lim ev])
next
case False
show ?thesis
proof(cases "0 < ξ")
case True
have ev: "∀⇩F x in at_top. 1 - (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)
= GPD_cdf ξ μ σ x"
using eventually_ge_at_top[of μ]
proof eventually_elim
case (elim x)
hence y0: "0 ≤ (x - μ) / σ"
using sigma by (intro divide_nonneg_pos) auto
have "- 1 ≤ ξ * ((x - μ) / σ)"
using mult_nonneg_nonneg[OF less_imp_le[OF True] y0] by linarith
thus ?case
using True elim by (simp add: GPD_cdf_def[OF sigma] Let_def)
qed
have lim: "((λx. 1 - (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)) ⤏ 1) at_top"
proof -
have 1: "LIM x at_top. 1 + ξ * ((x - μ) / σ) :> at_top"
proof -
have "LIM x at_top. (x - μ) / σ :> at_top"
using sigma by real_asymp
hence "LIM x at_top. ξ * ((x - μ) / σ) :> at_top"
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const True])
thus ?thesis
by (intro filterlim_tendsto_add_at_top[OF tendsto_const])
qed
have "((λx. (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)) ⤏ 0) at_top"
by (intro tendsto_neg_powr[OF _ 1]) (use True in ‹auto simp: divide_neg_pos›)
from tendsto_diff[OF tendsto_const this]
show ?thesis
by simp
qed
show ?thesis
by (rule Lim_transform_eventually[OF lim ev])
next
case False
with ‹ξ ≠ 0› have xi_neg: "ξ < 0"
by simp
have ev: "∀⇩F x in at_top. GPD_cdf ξ μ σ x = 1"
using eventually_ge_at_top[of "μ - σ / ξ"]
proof eventually_elim
case (elim x)
note neg = divide_pos_neg[OF sigma xi_neg]
hence mux:"μ ≤ x"
using elim neg by linarith
have eq: "(- σ / ξ) / σ = - 1 / ξ"
using xi_neg sigma by (simp add: field_simps)
have "(- σ / ξ) / σ ≤ (x - μ) / σ"
using elim sigma by (intro divide_right_mono) auto
hence zb: "- 1 / ξ ≤ (x - μ) / σ"
using sigma by (simp add: eq)
have "ξ * ((x - μ) / σ) ≤ ξ * (- 1 / ξ)"
by (rule mult_left_mono_neg[OF zb less_imp_le[OF xi_neg]])
hence xiy_le: "ξ * ((x - μ) / σ) ≤ - 1"
using xi_neg by simp
consider "ξ * ((x - μ) / σ) = - 1" | "ξ * ((x - μ) / σ) < - 1"
using xiy_le by argo
thus ?case
proof cases
case 1
thus ?thesis
using mux xi_neg by (simp add: GPD_cdf_def[OF sigma] Let_def)
next
case 2
thus ?thesis
using mux xi_neg by (auto simp: GPD_cdf_def[OF sigma] Let_def)
qed
qed
thus ?thesis
by (rule tendsto_eventually)
qed
qed
lemma
assumes sigma[arith]:"0 < σ"
shows GPD_density_integrable:"integrable lborel (GPD_density ξ μ σ)"
and GPD_density_integral:"(∫x. GPD_density ξ μ σ x ∂lborel) = 1"
and GPD_density_nn_integral:"(∫⇧+x. GPD_density ξ μ σ x ∂lborel) = 1"
proof -
have lim: "((λa. (∫x∈{..a}. GPD_density ξ μ σ x ∂lborel)) ⤏ 1) at_top"
proof -
have *: "(∫x∈{..a}. GPD_density ξ μ σ x ∂lborel) = GPD_cdf ξ μ σ a" for a
unfolding cdf_def
by(subst measure_density_on)
(auto simp: GPD_density_set_integrable[OF sigma])
show ?thesis
unfolding * by(rule GPD_cdf_at_top_1[OF sigma])
qed
show integ: "integrable lborel (GPD_density ξ μ σ)"
and eq2: "(∫x. GPD_density ξ μ σ x ∂lborel) = 1"
using lim GPD_density_set_integrable[OF sigma]
integrable_monotone_convergence_at_top[where f="GPD_density ξ μ σ" and x=1,
OF _ AE_I2[OF GPD_density_nonneg[OF less_imp_le[OF sigma]]]]
integral_monotone_convergence_at_top[where f="GPD_density ξ μ σ" and x=1,
OF _ AE_I2[OF GPD_density_nonneg[OF less_imp_le[OF sigma]]]]
by(auto simp: set_integrable_def set_lebesgue_integral_def mult.commute)
thus "(∫⇧+x. GPD_density ξ μ σ x ∂lborel) = 1"
by(subst nn_integral_eq_integral) auto
qed
lemma prob_space_GPD:
assumes sigma[arith]:"0 < σ"
shows "prob_space (density lborel (GPD_density ξ μ σ))"
by(auto intro!: prob_spaceI simp: emeasure_density GPD_density_nn_integral[OF sigma])
corollary real_distribution_GPD:
"0 < σ ⟹ real_distribution (density lborel (GPD_density ξ μ σ))"
by(simp add: real_distribution_def real_distribution_axioms_def prob_space_GPD)
lemma isCont_GPD_cdf:
assumes sigma[arith]: "0 < σ"
shows "isCont (GPD_cdf ξ μ σ) x"
using continuous_on_LBINT_com[OF GPD_density_integrable[OF sigma]]
GPD_cdf_set_integral[OF sigma]
by simp
lemma right_continuous_mono_GPD_cdf:
assumes sigma[arith]: "0 < σ"
shows "right_continuous_mono (GPD_cdf ξ μ σ) 0 1"
by(auto intro!: right_continuous_mono_cdf real_distribution_GPD)
corollary GPD_cdf_nonneg:"0 < σ ⟹ 0 ≤ GPD_cdf ξ μ σ x"
and GPD_cdf_le_1:"0 < σ ⟹ GPD_cdf ξ μ σ x ≤ 1"
using right_continuous_mono_GPD_cdf right_continuous_mono.a_le_f[of _ 0 1]
right_continuous_mono.f_le_b[of _ 0 1]
by fastforce+
lemma GPD_normalization:
fixes γ μ σ x :: real
assumes sigma[arith]: "0 < σ"
defines "a ≡ (λn. σ * (if γ = 0 then 1 else real n powr γ))"
defines "b ≡ (λn. μ + σ * (if γ = 0 then ln (real n) else (real n powr γ - 1) / γ))"
shows "(λn. GPD_cdf γ μ σ (a n * x + b n) ^ n) ⇢ EVD_cdf γ 0 1 x"
proof(cases "γ = 0")
assume 0:"γ = 0"
have "∀⇩F n in sequentially. ¦x¦ < ln (real n)"
using filterlim_compose[OF ln_at_top filterlim_real_sequentially]
by(auto simp: filterlim_at_top_dense)
hence pos: "∀⇩F n in sequentially. σ * x + σ * ln (real n) > 0"
by eventually_elim (smt (verit, ccfv_SIG) sigma distrib_left mult_pos_pos)
moreover have "∀⇩F n in sequentially. μ ≤ a n * x + b n"
using pos by eventually_elim (simp add: 0 a_def b_def)
moreover have "∀⇩F n in sequentially. 0 < real n"
by simp
ultimately have "∀⇩F n in sequentially. (GPD_cdf γ μ σ (a n * x + b n))^n
= (1 - exp (- x) / real n)^n"
unfolding GPD_cdf_def[OF sigma]
by eventually_elim (auto simp: 0 b_def a_def add_divide_distrib exp_diff)
moreover have "(λn. (1 - exp (- x) / real n)^n) ⇢ exp (- exp (- x))"
using tendsto_exp_limit_sequentially[of "- exp (- x)"]
by simp
ultimately show ?thesis
using tendsto_cong by(fastforce simp: EVD_cdf_def 0)
next
assume 0:"γ ≠ 0"
define y where "y ≡ (λn::nat. (real n powr γ * (1 + γ * x) - 1) / γ)"
have arg: "a n * x + b n = μ + σ * y n" for n
using 0 by(simp add: a_def b_def y_def field_simps)
have gy: "γ * y n = real n powr γ * (1 + γ * x) - 1" for n
using 0 by(simp add: y_def)
have cdf_eq: "GPD_cdf γ μ σ (a n * x + b n)
= (if y n < 0 then 0
else if - 1 ≤ γ * y n then 1 - (1 + γ * y n) powr (- 1 / γ) else 1)" for n
unfolding arg using 0 by(simp add: GPD_cdf_def[OF sigma] Let_def mult_less_0_iff)
show ?thesis
proof(cases "0 < 1 + γ * x")
case c_pos: True
have ge: "- 1 ≤ γ * y n" for n
using c_pos by(simp add: gy)
have ev0: "∀⇩F n in sequentially. 0 ≤ y n"
proof(cases "0 < γ")
case True
have "filterlim (λn. real n powr γ) at_top sequentially"
by(rule filterlim_compose[OF real_powr_at_top[OF True] filterlim_real_sequentially])
hence "∀⇩F n in sequentially. 1 / (1 + γ * x) ≤ real n powr γ"
by(simp add: filterlim_at_top)
thus ?thesis
proof eventually_elim
case (elim n)
hence "1 ≤ real n powr γ * (1 + γ * x)"
using c_pos by(simp add: pos_divide_le_eq)
thus "0 ≤ y n"
unfolding y_def using True by(intro divide_nonneg_pos) auto
qed
next
case False
with 0 have neg: "γ < 0"
by simp
have "(λn. real n powr γ) ⇢ 0"
by(rule tendsto_neg_powr[OF neg filterlim_real_sequentially])
hence "∀⇩F n in sequentially. real n powr γ < 1 / (1 + γ * x)"
using c_pos by(intro order_tendstoD) auto
thus ?thesis
proof eventually_elim
case (elim n)
hence "real n powr γ * (1 + γ * x) ≤ 1"
using c_pos by(simp add: pos_less_divide_eq)
thus "0 ≤ y n"
unfolding y_def using neg by(intro divide_nonpos_neg) auto
qed
qed
have ev: "∀⇩F n in sequentially.
GPD_cdf γ μ σ (a n * x + b n) = 1 - (1 + γ * x) powr (- 1 / γ) / real n"
proof(safe intro!: eventually_mp[OF eventually_sequentiallyI[of 1] ev0])
fix n :: nat
assume n: "1 ≤ n" and yn: "0 ≤ y n"
have n0: "0 < real n"
using n by simp
have "(1 + γ * y n) powr (- 1 / γ) = (real n powr γ * (1 + γ * x)) powr (- 1 / γ)"
by(simp add: gy)
also have "... = (real n powr γ) powr (- 1 / γ) * (1 + γ * x) powr (- 1 / γ)"
using c_pos by(simp add: powr_mult)
also have "... = (1 + γ * x) powr (- 1 / γ) / real n"
using 0 n0 by(simp add: powr_powr powr_minus_divide)
finally show "GPD_cdf γ μ σ (a n * x + b n)
= 1 - (1 + γ * x) powr (- 1 / γ) / real n"
using yn ge by(simp add: cdf_eq)
qed
have ev2: "∀⇩F n in sequentially. GPD_cdf γ μ σ (a n * x + b n) ^ n
= (1 - (1 + γ * x) powr (- 1 / γ) / real n) ^ n"
using ev by eventually_elim simp
have lim: "(λn. (1 - (1 + γ * x) powr (- 1 / γ) / real n) ^ n)
⇢ exp (- ((1 + γ * x) powr (- 1 / γ)))"
using tendsto_exp_limit_sequentially[of "- ((1 + γ * x) powr (- 1 / γ))"]
by simp
have EVD: "EVD_cdf γ 0 1 x = exp (- ((1 + γ * x) powr (- 1 / γ)))"
using c_pos 0 by(simp add: EVD_cdf_def)
show ?thesis
unfolding EVD by(subst tendsto_cong[OF ev2]) (rule lim)
next
case c_nonpos: False
have ev: "∀⇩F n in sequentially.
GPD_cdf γ μ σ (a n * x + b n) ^ n = EVD_cdf γ 0 1 x"
proof(intro eventually_sequentiallyI[of 1])
fix n :: nat
assume n: "1 ≤ n"
hence "0 < real n powr γ"
by simp
hence le: "γ * y n ≤ - 1"
using c_nonpos by(simp add: gy mult_nonneg_nonpos)
show "GPD_cdf γ μ σ (a n * x + b n) ^ n = EVD_cdf γ 0 1 x"
proof(cases "0 < γ")
case True
hence "y n < 0"
using le by (smt (verit, best) mult_nonneg_nonneg)
hence "GPD_cdf γ μ σ (a n * x + b n) = 0"
by(simp add: cdf_eq)
thus ?thesis
using n True c_nonpos by(simp add: EVD_cdf_def)
next
case False
with 0 have neg: "γ < 0"
by simp
hence yn: "¬ y n < 0"
using le by (smt (verit, best) mult_less_0_iff)
have "GPD_cdf γ μ σ (a n * x + b n) = 1"
proof(cases "γ * y n = - 1")
case True
thus ?thesis
using yn 0 neg by(simp add: cdf_eq)
next
case False
with le have "γ * y n < - 1"
by simp
thus ?thesis
using yn by(simp add: cdf_eq)
qed
thus ?thesis
using neg c_nonpos by(simp add: EVD_cdf_def)
qed
qed
show ?thesis
using ev by(simp add: tendsto_eventually)
qed
qed
end