Theory Extreme_Value_Distribution
section ‹Distributions›
subsection ‹Generalized Extreme Value Distribution›
theory Extreme_Value_Distribution
imports
Lemmas_EVT
begin
text ‹We define the generalized extreme value (GEV) density and cdf.
Our definition includes a location parameter $\mu$ and
a scale parameter $\sigma$.›
definition EVD_density :: "[real, real, real, real] ⇒ real" where
"EVD_density ξ μ σ x ≡ let y = (x - μ) / σ in
if ξ = 0 then
exp (- y) * exp (- exp (- y)) / σ
else
if ξ * y > - 1 then
(1 + ξ * y) powr (- 1 / ξ - 1)
* exp (- ((1 + ξ * y) powr (- 1 / ξ))) / σ
else 0"
lemma EVD_density_nonneg[simp]:
"0 ≤ σ ⟹ 0 ≤ EVD_density ξ μ σ x"
by(simp add: EVD_density_def Let_def)
lemma EVD_density_xi_0:
"EVD_density 0 μ σ x = exp (- ((x - μ) / σ)) * exp (- exp (- ((x - μ) / σ))) / σ"
by(simp add: EVD_density_def Let_def)
lemma
assumes "ξ ≠ 0"
shows EVD_density_xi_non0_1:
"ξ * (x - μ) / σ ≥ - 1
⟹ EVD_density ξ μ σ x = (1 + ξ * (x - μ) / σ) powr (- 1 / ξ - 1)
* exp (- ((1 + ξ * (x - μ) / σ) powr (- 1 / ξ))) / σ"
and EVD_density_xi_non0_2:
"ξ * (x - μ) / σ ≤ - 1 ⟹ EVD_density ξ μ σ x = 0"
using assms by(auto simp: EVD_density_def order.order_iff_strict)
lemma EVD_density_measurable[measurable]:
"EVD_density ξ μ σ ∈ borel_measurable borel"
unfolding EVD_density_def Let_def by simp
lemma
assumes sigma[arith]:"0 < σ"
shows EVD_density_set_integrable0:"set_integrable lborel {..a} (EVD_density 0 μ σ)"
and EVD_density_set_integral0:
"(∫x∈{..a}. EVD_density 0 μ σ x ∂lborel) = exp (- exp (- (a - μ) / σ))"
and EVD_density_set_nn_integral0:
"(∫⇧+x∈{..a}. EVD_density 0 μ σ x ∂lborel) = ennreal (exp (- exp (- (a - μ) / σ)))"
proof -
define G where "G = (λx::real. exp (- exp (- (x - μ) / σ)))"
have deriv: "(G has_real_derivative EVD_density 0 μ σ x) (at x)" for x
unfolding G_def EVD_density_def Let_def
using sigma by (auto intro!: derivative_eq_intros
simp: field_simps simp del: minus_diff_eq)
have tendsto_bot: "(G ⤏ 0) at_bot"
unfolding G_def using sigma
by(intro filterlim_compose[OF exp_at_bot filterlim_compose
[OF filterlim_uminus_at_bot_at_top]]
filterlim_compose[OF exp_at_top])
real_asymp
have cont: "continuous (at_left a) G"
using continuous_at_imp_continuous_at_within[OF DERIV_isCont[OF deriv]] by simp
show "set_integrable lborel {..a} (EVD_density 0 μ σ)"
and "(∫x∈{..a}. EVD_density 0 μ σ x ∂lborel) = exp (- exp (- (a - μ) / σ))"
and "(∫⇧+x∈{..a}. EVD_density 0 μ σ x ∂lborel) = ennreal (exp (- exp (- (a - μ) / σ)))"
using set_integrable_FTC_atMost[OF _ cont deriv _ tendsto_bot]
set_integral_FTC_atMost[OF _ cont deriv _ tendsto_bot]
nn_integral_FTC_lessThan[OF _ cont deriv _ tendsto_bot]
by(simp_all add: G_def set_nn_integral_atMost_eq)
qed
lemma
fixes a μ σ
defines "y ≡ (a - μ) / σ"
assumes sigma[arith]:"0 < σ"
and xi:"ξ ≠ 0"
and xiy:"ξ * y ≥ - 1"
and xiy_pos:"0 < ξ ⟹ - 1 < ξ * y"
shows EVD_density_set_integrable1:"set_integrable lborel {..a} (EVD_density ξ μ σ)"
and EVD_density_set_integral1:
"(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel) = exp (- ((1 + ξ * y) powr (- 1 / ξ)))"
and EVD_density_set_nn_integral1:
"(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel) = ennreal (exp (- ((1 + ξ * y) powr (- 1 / ξ))))"
proof -
have deriv_raw: "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) has_real_derivative
EVD_density ξ μ σ x) (at x)"
if pos: "0 < 1 + ξ * ((x - μ) / σ)" for x
proof -
have cond: "- 1 < ξ * ((x - μ) / σ)"
using pos by linarith
have dens: "EVD_density ξ μ σ x
= (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ - 1)
* exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ))) / σ"
using cond xi by(simp add: EVD_density_def Let_def)
show ?thesis
unfolding dens
using pos xi by(auto intro!: derivative_eq_intros simp: field_simps)
qed
show nn: "(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel)
= ennreal (exp (- ((1 + ξ * y) powr (- 1 / ξ))))"
proof(cases "0 < ξ")
case False
with xi have xi_neg: "ξ < 0"
by simp
have p_pos: "0 < - 1 / ξ"
using xi_neg by (simp add: divide_pos_neg)
define F where "F ≡ λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))"
have pos: "0 < 1 + ξ * ((x - μ) / σ)" if "x < a" for x
proof -
have "(x - μ) / σ < (a - μ) / σ"
using that sigma by (intro divide_strict_right_mono) auto
hence "ξ * ((a - μ) / σ) < ξ * ((x - μ) / σ)"
by (rule mult_strict_left_mono_neg[OF _ xi_neg])
with xiy show ?thesis
unfolding y_def by linarith
qed
have deriv: "(F has_real_derivative EVD_density ξ μ σ x) (at x)" if "x < a" for x
unfolding F_def by (rule deriv_raw[OF pos[OF that]])
have nonneg: "0 ≤ EVD_density ξ μ σ x" for x
by simp
have cont: "continuous (at_left a) F"
proof (cases "ξ * y = - 1")
case False
with xiy have pos_a: "0 < 1 + ξ * y"
by linarith
have "isCont F a"
unfolding F_def using pos_a
by (intro continuous_intros) (simp_all add: y_def)
thus ?thesis
using continuous_at_imp_continuous_at_within by blast
next
case True
have Fa: "F a = 1"
using True unfolding F_def y_def by simp
have "((λx. 1 + ξ * ((x - μ) / σ)) ⤏ 1 + ξ * ((a - μ) / σ)) (at_left a)"
by (intro tendsto_intros) arith
with True have base0: "((λx. 1 + ξ * ((x - μ) / σ)) ⤏ 0) (at_left a)"
by (simp add: y_def)
have ev_pos: "∀⇩F x in at_left a. 0 ≤ 1 + ξ * ((x - μ) / σ)"
by (intro eventually_at_leftI[of "a - 1"]) (use pos[THEN less_imp_le] in auto)
have "((λx. (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)) ⤏ 0) (at_left a)"
by (rule tendsto_zero_powrI[OF base0 tendsto_const ev_pos p_pos])
hence "(F ⤏ exp (- 0)) (at_left a)"
unfolding F_def by (intro tendsto_intros)
thus ?thesis
by (simp add: continuous_within Fa)
qed
have lim: "(F ⤏ 0) at_bot"
unfolding F_def
using filterlim_compose[OF real_powr_at_top[OF p_pos]
filterlim_shift_scale_at_bot[OF sigma xi_neg]]
by (intro filterlim_compose[OF exp_at_bot
filterlim_compose[OF filterlim_uminus_at_bot_at_top]])
have "(∫⇧+x∈{..<a}. EVD_density ξ μ σ x ∂lborel)
= ennreal (exp (- ((1 + ξ * y) powr (- 1 / ξ))))"
using nn_integral_FTC_lessThan[OF EVD_density_measurable cont deriv nonneg lim]
by (simp add: F_def y_def)
thus ?thesis
by (simp add: set_nn_integral_atMost_eq[symmetric])
next
case True
have p_neg: "- 1 / ξ < 0"
using True by (simp add: divide_neg_pos)
define c where "c ≡ μ - σ / ξ"
define F where "F ≡ λx. if - 1 < ξ * ((x - μ) / σ)
then exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ))) else 0"
have cond_iff: "(- 1 < ξ * ((x - μ) / σ)) ⟷ c < x" for x
using True sigma unfolding c_def by (auto simp: field_simps)
have ca: "c < a"
using xiy_pos[OF True] cond_iff[of a] by (simp add: y_def)
have dens0: "EVD_density ξ μ σ x = 0" if "¬ c < x" for x
using cond_iff[of x] that xi by (auto simp: EVD_density_def Let_def)
have pos: "0 < 1 + ξ * ((x - μ) / σ)" if "c < x" for x
using cond_iff[THEN iffD2, OF that] by linarith
have F_eq: "F x = exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))" if "c < x" for x
using cond_iff that by (simp add: F_def)
have deriv: "(F has_real_derivative EVD_density ξ μ σ x) (at x)" if "c < x" for x
proof -
have "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) has_real_derivative
EVD_density ξ μ σ x) (at x)"
by (rule deriv_raw[OF pos[OF that]])
thus ?thesis
by (rule has_field_derivative_transform_within_open[where S="{c<..}"])
(auto simp: F_eq that)
qed
have deriv': "(F has_real_derivative EVD_density ξ μ σ x) (at x)" if "a < x" for x
by (rule deriv[OF less_trans[OF ca that]])
have nonneg: "0 ≤ EVD_density ξ μ σ x" for x
by simp
have Fc: "F c = 0"
using cond_iff[of c] by (simp add: F_def)
have contc: "continuous (at_right c) F"
proof -
have "((λx. 1 + ξ * ((x - μ) / σ)) ⤏ 1 + ξ * ((c - μ) / σ)) (at_right c)"
by (intro tendsto_intros) arith
moreover have "1 + ξ * ((c - μ) / σ) = 0"
using True sigma by (simp add: c_def)
ultimately have base0: "((λx. 1 + ξ * ((x - μ) / σ)) ⤏ 0) (at_right c)"
by simp
have ev_pos: "∀⇩F x in at_right c. 0 < 1 + ξ * ((x - μ) / σ)"
by (intro eventually_at_rightI[of c "c + 1"]) (use pos in auto)
have small: "((λx. (1 + ξ * ((x - μ) / σ)) powr (1 / ξ)) ⤏ 0) (at_right c)"
by (rule tendsto_zero_powrI[OF base0 tendsto_const])
(use ev_pos True in ‹auto elim: eventually_mono›)
have ev_pos': "∀⇩F x in at_right c. 0 < (1 + ξ * ((x - μ) / σ)) powr (1 / ξ)"
using ev_pos by (auto elim!: eventually_mono)
have top: "LIM x (at_right c). (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ) :> at_top"
using filterlim_inverse_at_top[OF small ev_pos'] by (simp add: powr_minus)
have *: "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) ⤏ 0) (at_right c)"
by (rule filterlim_compose[OF exp_at_bot
filterlim_compose[OF filterlim_uminus_at_bot_at_top top]])
have "(F ⤏ 0) (at_right c)"
by (rule Lim_transform_eventually[OF *])
(auto intro!: eventually_at_rightI[of c "c + 1"] simp: F_eq)
thus ?thesis
by (simp add: continuous_within Fc)
qed
have conta: "continuous (at_right a) F"
proof -
have "isCont (λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) a"
using pos[OF ca] by (intro continuous_intros) auto
hence "continuous (at_right a) (λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ))))"
by (rule continuous_at_imp_continuous_at_within)
hence "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ))))
⤏ exp (- ((1 + ξ * ((a - μ) / σ)) powr (- 1 / ξ)))) (at_right a)"
by (simp add: continuous_within)
hence "(F ⤏ exp (- ((1 + ξ * ((a - μ) / σ)) powr (- 1 / ξ)))) (at_right a)"
by (rule Lim_transform_eventually)
(auto intro!: eventually_at_rightI[of a "a + 1"] simp: F_eq less_trans[OF ca])
thus ?thesis
by (simp add: continuous_within F_eq[OF ca])
qed
have limtop: "(F ⤏ 1) at_top"
proof -
have powr0: "((λx. (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)) ⤏ 0) at_top"
by (rule tendsto_neg_powr[OF p_neg filterlim_shift_scale_at_top[OF sigma True]])
have "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) ⤏ exp (- 0)) at_top"
by (intro tendsto_intros powr0)
hence *: "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) ⤏ 1) at_top"
by simp
have ev: "∀⇩F x in at_top. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ))) = F x"
using eventually_gt_at_top[of c] by eventually_elim (simp add: F_eq)
show ?thesis
by (rule Lim_transform_eventually[OF * ev])
qed
have Fa: "F a = exp (- ((1 + ξ * y) powr (- 1 / ξ)))"
by (simp add: F_eq[OF ca] y_def)
have Fa01: "0 ≤ F a" "F a ≤ 1"
by (auto simp: Fa)
have I1: "(∫⇧+x∈{c<..}. EVD_density ξ μ σ x ∂lborel) = 1"
using nn_integral_FTC_greaterThan[OF EVD_density_measurable contc deriv nonneg limtop]
by (simp add: Fc)
have I2: "(∫⇧+x∈{a<..}. EVD_density ξ μ σ x ∂lborel) = 1 - ennreal (F a)"
using nn_integral_FTC_greaterThan[OF EVD_density_measurable conta deriv' nonneg limtop]
by (metis ennreal_1 ennreal_minus Fa01(1))
have "(∫⇧+x∈{c<..a}. EVD_density ξ μ σ x ∂lborel) + (∫⇧+x∈{a<..}. EVD_density ξ μ σ x ∂lborel)
= (∫⇧+x. ennreal (EVD_density ξ μ σ x) * indicator {c<..a} x
+ ennreal (EVD_density ξ μ σ x) * indicator {a<..} x ∂lborel)"
by (rule nn_integral_add[symmetric]) auto
also have "... = (∫⇧+x∈{c<..}. EVD_density ξ μ σ x ∂lborel)"
using ca by (auto intro!: nn_integral_cong simp: indicator_def)
finally have split: "(∫⇧+x∈{c<..a}. EVD_density ξ μ σ x ∂lborel) + (1 - ennreal (F a)) = 1"
by (simp add: I1 I2)
have X: "(∫⇧+x∈{c<..a}. EVD_density ξ μ σ x ∂lborel) = ennreal (F a)"
proof -
have le1: "ennreal (F a) ≤ 1"
using Fa01 by (simp add: ennreal_leI)
have c_ne: "1 - ennreal (F a) ≠ ⊤"
by simp
have "(∫⇧+x∈{c<..a}. EVD_density ξ μ σ x ∂lborel)
= ((∫⇧+x∈{c<..a}. EVD_density ξ μ σ x ∂lborel) + (1 - ennreal (F a)))
- (1 - ennreal (F a))"
by (simp add: c_ne)
also have "... = 1 - (1 - ennreal (F a))"
by (simp add: split)
also have "... = ennreal (F a)"
using le1 diff_diff_ennreal'' by auto
finally show ?thesis .
qed
have "(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel) = (∫⇧+x∈{c<..a}. EVD_density ξ μ σ x ∂lborel)"
by (auto intro!: nn_integral_cong simp: indicator_def dens0)
thus ?thesis
by (simp add: X Fa)
qed
have 1: "(∫⇧+x∈{..a}. ennreal (EVD_density ξ μ σ x) ∂lborel)
= (∫⇧+ x. ennreal ¦indicat_real {..a} x * EVD_density ξ μ σ x¦ ∂lborel)"
by(auto intro!: nn_integral_cong simp: indicator_def)
show "set_integrable lborel {..a} (EVD_density ξ μ σ)"
using nn by(simp add: set_integrable_def integrable_iff_bounded 1)
have "(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel)
= enn2real (∫⇧+x∈{..a}. ennreal (EVD_density ξ μ σ x) ∂lborel)"
unfolding set_lebesgue_integral_def
by(subst integral_eq_nn_integral)
(auto simp: indicator_def intro!: arg_cong[where f=enn2real] nn_integral_cong)
thus "(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel) = exp (- ((1 + ξ * y) powr (- 1 / ξ)))"
by(simp add: nn)
qed
lemma
fixes a μ σ
defines "y ≡ (a - μ) / σ"
assumes sigma[arith]:"0 < σ"
and xiy:"ξ * y ≤ - 1"
and xi:"ξ > 0"
shows EVD_density_set_integrable2: "set_integrable lborel {..a} (EVD_density ξ μ σ)"
and EVD_density_set_integral2:
"(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel) = 0"
and EVD_density_set_nn_integral2:
"(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel) = 0"
proof -
have eq0[simp]:"⋀x. x ≤ a ⟹ EVD_density ξ μ σ x = 0"
by (smt (verit, ccfv_SIG) EVD_density_def y_def sigma
xi xiy divide_right_mono mult_le_cancel_left_pos)
show "set_integrable lborel {..a} (EVD_density ξ μ σ)"
by(subst set_integrable_cong[where f'="λx. 0",OF refl refl]) simp_all
show "(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel) = 0"
by(subst set_integral_cong[where g="λx. 0"]) simp_all
show "(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel) = 0"
by(subst set_nn_integral_cong[where g="λx. 0"]) simp_all
qed
lemma
fixes a μ σ
defines "y ≡ (a - μ) / σ"
assumes sigma[arith]:"0 < σ"
and xiy:"ξ * y ≤ - 1"
and xi:"ξ < 0"
shows EVD_density_set_integrable3: "set_integrable lborel {..a} (EVD_density ξ μ σ)"
and EVD_density_set_integral3:
"(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel) = 1"
and EVD_density_set_nn_integral3:
"(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel) = 1"
proof -
define b where "b ≡ μ - σ / ξ"
have ba:"b ≤ a"
using xiy xi unfolding b_def y_def by (simp add: field_simps)
have [simp]:"⋀x. b ≤ x ⟹ EVD_density ξ μ σ x = 0"
by (smt (verit, ccfv_SIG) EVD_density_def sigma xi b_def divide_le_eq
le_divide_eq_1 minus_divide_left mult.commute
times_divide_eq_right)
have b:"ξ * ((b - μ) / σ) ≥ - 1"
using xi by(simp add: b_def)
have b':"0 < ξ ⟹ - 1 < ξ * ((b - μ) / σ)"
using xi by linarith
have h1[simp]:"set_integrable lborel {..b} (EVD_density ξ μ σ)"
and h2:"(∫x∈{..b}. EVD_density ξ μ σ x ∂lborel) = 1"
and h3:"(∫⇧+x∈{..b}. EVD_density ξ μ σ x ∂lborel) = 1"
using EVD_density_set_integrable1[OF sigma less_imp_neq[OF xi] b b']
EVD_density_set_integral1[OF sigma less_imp_neq[OF xi] b b']
EVD_density_set_nn_integral1[OF sigma less_imp_neq[OF xi] b b'] xi
by(simp_all add: b_def)
have [simp]:"set_integrable lborel {b<..a} (EVD_density ξ μ σ)"
by(subst set_integrable_cong[where f'="λx. 0",OF refl refl]) simp_all
have eq0:"(∫x∈{b<..a}. EVD_density ξ μ σ x ∂lborel) = 0"
by(subst set_integral_cong[where g="λx. 0"]) auto
have eq0':"(∫⇧+x∈{b<..a}. EVD_density ξ μ σ x ∂lborel) = 0"
by(subst set_nn_integral_cong[where g="λx. 0",OF refl refl]) auto
show "set_integrable lborel {..a} (EVD_density ξ μ σ)"
using ba
by(subst set_integrable_cong[where A'="{..b} ∪ {b<..a}"])
(auto intro!: set_integrable_Un h1)
have "(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel) =
(∫x∈{..b}. EVD_density ξ μ σ x ∂lborel) + (∫x∈{b<..a}. EVD_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}. EVD_density ξ μ σ x ∂lborel) = 1" .
have "(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel) =
(∫⇧+x. ennreal (EVD_density ξ μ σ x) * indicator {..b} x
+ ennreal (EVD_density ξ μ σ x) * indicator {b<..a} x ∂lborel)"
using ba by(auto intro!: nn_integral_cong simp: indicator_def)
also have "... = (∫⇧+x∈{..b}. EVD_density ξ μ σ x ∂lborel)"
using ba by(auto intro!: nn_integral_cong simp: indicator_def)
finally show "(∫⇧+x∈{..a}. EVD_density ξ μ σ x ∂lborel) = 1"
by(simp add: h3)
qed
lemma EVD_density_set_integrable:
assumes sigma[arith]:"0 < σ"
shows "set_integrable lborel {..a} (EVD_density ξ μ σ)"
proof -
consider "ξ = 0" | "ξ ≠ 0" "- 1 < ξ * ((a - μ) / σ)"
| "ξ * ((a - μ) / σ) ≤ -1" "ξ > 0" | "ξ * ((a - μ) / σ) ≤ -1" "ξ < 0"
by argo
thus ?thesis
by cases
(use EVD_density_set_integrable0[OF sigma]
EVD_density_set_integrable1[OF sigma _ less_imp_le]
EVD_density_set_integrable2[OF sigma]
EVD_density_set_integrable3[OF sigma] in auto)
qed
abbreviation EVD_cdf where "EVD_cdf ≡ λξ μ σ x. cdf (density lborel (EVD_density ξ μ σ)) x"
lemma EVD_cdf_set_integral:
assumes sigma[arith]:"0 < σ"
shows "EVD_cdf ξ μ σ a = (∫x∈{..a}. EVD_density ξ μ σ x ∂lborel)"
proof -
consider "ξ = 0" | "ξ ≠ 0" "- 1 < ξ * ((a - μ) / σ)"
| "ξ > 0" "ξ * ((a - μ) / σ) ≤ - 1"
| "ξ < 0" "ξ * ((a - μ) / σ) ≤ - 1"
by linarith
thus ?thesis
unfolding cdf_def
using EVD_density_set_integrable3[OF sigma]
EVD_density_set_integrable2[OF sigma]
EVD_density_set_integrable1[OF sigma]
EVD_density_set_integrable0[OF sigma]
by (cases; subst measure_density_on) auto
qed
corollary EVD_cdf_def:
assumes sigma[arith]:"0 < σ"
shows "EVD_cdf ξ μ σ x =
(let y = (x - μ) / σ in
if ξ = 0 then exp (- exp (- y))
else if ξ * y > - 1 then exp (- ((1 + ξ * y) powr (- 1 / ξ)))
else if ξ > 0 then 0 else 1)"
proof -
note cdf_simps = cdf_def measure_def emeasure_density
consider "ξ = 0" | "ξ ≠ 0" "- 1 < ξ * ((x - μ) / σ)"
| "ξ * ((x - μ) / σ) ≤ -1" "ξ > 0" | "ξ * ((x - μ) / σ) ≤ -1" "ξ < 0"
by argo
thus ?thesis
proof cases
assume 2:"ξ ≠ 0" "- 1 < ξ * ((x - μ) / σ)"
thus ?thesis
by(simp add: cdf_simps
EVD_density_set_nn_integral1[OF sigma 2(1) less_imp_le[OF 2(2)] 2(2)])
qed(simp_all add: cdf_simps minus_divide_left
EVD_density_set_nn_integral0
EVD_density_set_nn_integral2
EVD_density_set_nn_integral3)
qed
lemma EVD_cdf_supp_bounds:
fixes x γ :: real
assumes [arith]:"1 + γ * (x - μ) / σ > 0" "0 < σ"
shows "0 < EVD_cdf γ μ σ x" "EVD_cdf γ μ σ x ≤ 1"
using assms by (auto simp add: EVD_cdf_def Let_def)
lemma EVD_cdf_supp_bounds01:
fixes x γ :: real
assumes [arith]:"1 + γ * x > 0"
shows "0 < EVD_cdf γ 0 1 x" "EVD_cdf γ 0 1 x ≤ 1"
by(auto intro!: EVD_cdf_supp_bounds)
lemma ln_EVD_cdf_0:
assumes "0 < σ"
shows "- ln (EVD_cdf 0 μ σ x) = exp (- ((x - μ) / σ))"
using assms by(simp add: EVD_cdf_def[of σ])
lemma ln_EVD_cdf_1:
assumes "0 < σ" "1 + γ * (x - μ) / σ > 0" "γ ≠ 0"
shows "- ln (EVD_cdf γ μ σ x) = (1 + γ * (x - μ) / σ) powr (- 1 / γ)"
using assms by(auto simp add: EVD_cdf_def[of σ])
lemma EVD_cdf_location_scale:
assumes [arith]:"0 < σ"
shows "EVD_cdf ξ 0 1 ((x - μ) / σ) = EVD_cdf ξ μ σ x"
by(simp add: EVD_cdf_def)
lemma EVD_cdf_at_bot_0:
assumes sigma:"0 < σ"
shows "(EVD_cdf ξ μ σ ⤏ 0) at_bot"
proof -
consider "ξ = 0" | "ξ > 0" | "ξ < 0"
by linarith
thus ?thesis
proof cases
assume xi:"ξ = 0"
have *: "((λx. exp (- exp (- ((x - μ) / σ)))) ⤏ 0) at_bot"
using sigma
by(intro filterlim_compose[OF exp_at_bot
filterlim_compose[OF filterlim_uminus_at_bot_at_top]]
filterlim_compose[OF exp_at_top])
real_asymp
show ?thesis
by(rule Lim_transform_eventually[OF *])
(use xi in ‹simp add: EVD_cdf_def[OF sigma] Let_def›)
next
assume xi:"ξ > 0"
have ev: "∀⇩F x in at_bot. EVD_cdf ξ μ σ x = 0"
using xi sigma
by (auto intro!: eventually_mono[OF eventually_le_at_bot[of "μ - σ / ξ"]]
simp: EVD_cdf_def[OF sigma] Let_def field_simps)
thus ?thesis
by (rule tendsto_eventually)
next
assume xi:"ξ < 0"
have p_pos: "0 < - 1 / ξ"
using xi by (simp add: divide_pos_neg)
note base = filterlim_shift_scale_at_bot[OF sigma xi]
have *: "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) ⤏ 0) at_bot"
by (rule filterlim_compose[OF exp_at_bot
filterlim_compose[OF filterlim_uminus_at_bot_at_top
filterlim_compose[OF real_powr_at_top[OF p_pos] base]]])
have evlt: "∀⇩F x in at_bot. x < μ - σ / ξ"
using eventually_le_at_bot[of "μ - σ / ξ - 1"] by eventually_elim simp
have ev:
"∀⇩F x in at_bot. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ))) = EVD_cdf ξ μ σ x"
using evlt
proof eventually_elim
case (elim x)
have "(x - μ) / σ < ((μ - σ / ξ) - μ) / σ"
using elim sigma by (intro divide_strict_right_mono) auto
hence "ξ * (((μ - σ / ξ) - μ) / σ) < ξ * ((x - μ) / σ)"
by (rule mult_strict_left_mono_neg[OF _ xi])
moreover have "ξ * (((μ - σ / ξ) - μ) / σ) = - 1"
using xi sigma by (simp add: field_simps)
ultimately have "- 1 < ξ * ((x - μ) / σ)"
by simp
thus ?case
using xi by (simp add: EVD_cdf_def[OF sigma] Let_def)
qed
show ?thesis
by (rule Lim_transform_eventually[OF * ev])
qed
qed
lemma EVD_cdf_at_top_1:
assumes sigma:"0 < σ"
shows "(EVD_cdf ξ μ σ ⤏ 1) at_top"
proof -
consider "ξ = 0" | "ξ > 0" | "ξ < 0"
by linarith
thus ?thesis
proof cases
assume xi:"ξ = 0"
have 1: "((λx. exp (- ((x - μ) / σ))) ⤏ 0) at_top"
using sigma
by (intro filterlim_compose[OF exp_at_bot]) real_asymp
have "((λx. exp (- exp (- ((x - μ) / σ)))) ⤏ exp (- 0)) at_top"
by (intro tendsto_intros 1)
hence *: "((λx. exp (- exp (- ((x - μ) / σ)))) ⤏ 1) at_top"
by simp
show ?thesis
by(rule Lim_transform_eventually[OF *])
(use xi in ‹simp add: EVD_cdf_def[OF sigma] Let_def›)
next
assume xi:"ξ > 0"
have p_neg: "- 1 / ξ < 0"
using xi by (simp add: divide_neg_pos)
have powr0: "((λx. (1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)) ⤏ 0) at_top"
by (rule tendsto_neg_powr[OF p_neg filterlim_shift_scale_at_top[OF sigma xi]])
have "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) ⤏ exp (- 0)) at_top"
by (intro tendsto_intros powr0)
hence *: "((λx. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ)))) ⤏ 1) at_top"
by simp
have ev:
"∀⇩F x in at_top. exp (- ((1 + ξ * ((x - μ) / σ)) powr (- 1 / ξ))) = EVD_cdf ξ μ σ x"
using eventually_gt_at_top[of "μ - σ / ξ"]
proof eventually_elim
case (elim x)
have "((μ - σ / ξ) - μ) / σ < (x - μ) / σ"
using elim sigma by (intro divide_strict_right_mono) auto
hence "ξ * (((μ - σ / ξ) - μ) / σ) < ξ * ((x - μ) / σ)"
by (rule mult_strict_left_mono[OF _ xi])
moreover have "ξ * (((μ - σ / ξ) - μ) / σ) = - 1"
using xi sigma by (simp add: field_simps)
ultimately have "- 1 < ξ * ((x - μ) / σ)"
by simp
thus ?case
using xi by (simp add: EVD_cdf_def[OF sigma] Let_def)
qed
show ?thesis
by (rule Lim_transform_eventually[OF * ev])
next
assume xi:"ξ < 0"
have ev: "∀⇩F x in at_top. EVD_cdf ξ μ σ x = 1"
using eventually_ge_at_top[of "μ - σ / ξ"]
proof eventually_elim
case (elim x)
have "((μ - σ / ξ) - μ) / σ ≤ (x - μ) / σ"
using elim sigma by (intro divide_right_mono) auto
hence "ξ * ((x - μ) / σ) ≤ ξ * (((μ - σ / ξ) - μ) / σ)"
by (rule mult_left_mono_neg[OF _ less_imp_le[OF xi]])
moreover have "ξ * (((μ - σ / ξ) - μ) / σ) = - 1"
using xi sigma by (simp add: field_simps)
ultimately have "ξ * ((x - μ) / σ) ≤ - 1"
by simp
thus ?case
using xi by (simp add: EVD_cdf_def[OF sigma] Let_def)
qed
thus ?thesis
by (rule tendsto_eventually)
qed
qed
lemma
assumes sigma[arith]:"0 < σ"
shows EVD_density_integrable:"integrable lborel (EVD_density ξ μ σ)"
and EVD_density_integral:"(∫x. EVD_density ξ μ σ x ∂lborel) = 1"
and EVD_density_nn_integral:"(∫⇧+x. EVD_density ξ μ σ x ∂lborel) = 1"
proof -
have lim:"((λa. (∫x∈{..a}. EVD_density ξ μ σ x ∂lborel)) ⤏ 1) at_top"
proof -
have *:"(∫x∈{..a}. EVD_density ξ μ σ x ∂lborel) = EVD_cdf ξ μ σ a" for a
unfolding cdf_def
by(subst measure_density_on)
(auto simp: EVD_density_set_integrable)
show ?thesis
unfolding * by(rule EVD_cdf_at_top_1[OF sigma])
qed
show integ:"integrable lborel (EVD_density ξ μ σ)"
and eq2:"(∫x. EVD_density ξ μ σ x ∂lborel) = 1"
using lim EVD_density_set_integrable[OF sigma]
integrable_monotone_convergence_at_top[where f="EVD_density ξ μ σ" and x=1,
OF _ AE_I2[OF EVD_density_nonneg[OF less_imp_le[OF sigma]]]]
integral_monotone_convergence_at_top[where f="EVD_density ξ μ σ" and x=1,
OF _ AE_I2[OF EVD_density_nonneg[OF less_imp_le[OF sigma]]]]
by(auto simp: set_integrable_def set_lebesgue_integral_def mult.commute)
thus "(∫⇧+x. EVD_density ξ μ σ x ∂lborel) = 1"
by(subst nn_integral_eq_integral) auto
qed
lemma prob_space_EVD:
assumes sigma[arith]:"0 < σ"
shows "prob_space (density lborel (EVD_density ξ μ σ))"
by(auto intro!: prob_spaceI simp: emeasure_density EVD_density_nn_integral)
corollary real_distribution_EVD:
"0 < σ ⟹ real_distribution (density lborel (EVD_density ξ μ σ))"
by(simp add: real_distribution_def real_distribution_axioms_def prob_space_EVD)
corollary right_continuous_mono_EVD_cdf:
"0 < σ ⟹ right_continuous_mono (EVD_cdf ξ μ σ) 0 1"
by(auto intro!: right_continuous_mono_cdf real_distribution_EVD)
corollary EVD_cdf_nonneg:"0 < σ ⟹ 0 ≤ EVD_cdf ξ μ σ x"
and EVD_cdf_le_1:"0 < σ ⟹ EVD_cdf ξ μ σ x ≤ 1"
using right_continuous_mono_EVD_cdf right_continuous_mono.a_le_f[of _ 0 1]
right_continuous_mono.f_le_b[of _ 0 1]
by fastforce+
lemma isCont_EVD_cdf:
assumes sigma[arith]: "0 < σ"
shows "isCont (EVD_cdf ξ μ σ) x"
using continuous_on_LBINT_com[OF EVD_density_integrable[OF sigma]]
EVD_cdf_set_integral[OF sigma]
by simp
corollary weak_conv_EVD_cdf_iff:
assumes sigma:"0 < σ"
shows "weak_conv F (EVD_cdf ξ μ σ) ⟷ (∀x. (λn. F n x) ⇢ EVD_cdf ξ μ σ x)"
using isCont_EVD_cdf[OF sigma] by(simp add: weak_conv_def)
text ‹Max-stability of the GEV distribution (Exercise~1.2 of the book~\<^cite>‹deHaanFerreira›).
The book's argument is
$G_\xi^n(a_n x + b_n) = G_\xi(x)$ for $a_n = n^\xi$ and $b_n = (n^\xi - 1)/\xi$,
whereas we state the equivalent solved form
$G_\xi^n(x) = G_\xi((x - b_n)/a_n)$, in which
$(x - b_n)/a_n = n^{-\xi}x + (n^{-\xi} - 1)/\xi$.›
lemma EVD_cdf_max_stable:
assumes "0 < n"
shows "EVD_cdf ξ 0 1 x ^ n
= EVD_cdf ξ 0 1 (if ξ = 0 then x - ln n
else n powr (- ξ) * x + (real n powr (- ξ) - 1) / ξ)"
proof -
have [arith]: "(0::real) < 1"
by simp
consider "ξ = 0" | "ξ ≠ 0" "- 1 < ξ * x" | "ξ ≠ 0" "ξ * x ≤ - 1" by argo
thus ?thesis
proof cases
case 1
have "EVD_cdf ξ 0 1 x ^ n = exp (real n * (- exp (- x)))"
by (simp add: EVD_cdf_def Let_def 1 exp_of_nat_mult[symmetric])
also have "real n * (- exp (- x)) = - exp (- (x - ln (real n)))"
using assms by (simp add: exp_diff exp_minus field_simps)
finally show ?thesis
using 1 by (simp add: EVD_cdf_def Let_def)
next
case 2
define c where "c = real n powr (- ξ)"
have c_pos: "0 < c"
using assms by (simp add: c_def)
have arg: "1 + ξ * (c * x + (c - 1) / ξ) = c * (1 + ξ * x)"
using 2(1) by (simp add: field_simps)
have p1: "0 < c * (1 + ξ * x)"
using c_pos 2(2) by (intro mult_pos_pos) auto
have argpos: "- 1 < ξ * (c * x + (c - 1) / ξ)"
using arg p1 by linarith
have "(c * (1 + ξ * x)) powr (- 1 / ξ) = c powr (- 1 / ξ) * (1 + ξ * x) powr (- 1 / ξ)"
by (rule powr_mult)
also have "c powr (- 1 / ξ) = real n powr ((- ξ) * (- 1 / ξ))"
by (simp add: c_def powr_powr)
also have "(- ξ) * (- 1 / ξ) = 1"
using 2(1) by simp
also have "real n powr 1 = real n"
by simp
finally have *: "(c * (1 + ξ * x)) powr (- 1 / ξ) = real n * (1 + ξ * x) powr (- 1 / ξ)" .
have "EVD_cdf ξ 0 1 x ^ n = exp (real n * (- ((1 + ξ * x) powr (- 1 / ξ))))"
using 2 by (simp add: EVD_cdf_def Let_def exp_of_nat_mult[symmetric])
also have "… = exp (- ((c * (1 + ξ * x)) powr (- 1 / ξ)))"
using * by simp
also have "… = EVD_cdf ξ 0 1 (c * x + (c - 1) / ξ)"
using 2(1) argpos by (simp add: EVD_cdf_def Let_def arg)
finally show ?thesis
using 2(1) by (simp add: c_def)
next
case 3
define c where "c = real n powr (- ξ)"
have c_pos: "0 < c"
using assms by (simp add: c_def)
have le0: "c * (1 + ξ * x) ≤ 0"
using 3(2) by (intro mult_nonneg_nonpos) (use c_pos in auto)
have arg: "ξ * (c * x + (c - 1) / ξ) = c * (1 + ξ * x) - 1"
using 3(1) by (simp add: field_simps)
have argneg: "ξ * (c * x + (c - 1) / ξ) ≤ - 1"
using le0 by (simp add: arg)
consider "0 < ξ" | "ξ < 0" using 3(1) by argo
thus ?thesis
proof cases
case pos: 1
hence "EVD_cdf ξ 0 1 x = 0"
using 3 by (simp add: EVD_cdf_def Let_def)
moreover have "EVD_cdf ξ 0 1 (c * x + (c - 1) / ξ) = 0"
using pos argneg by (simp add: EVD_cdf_def Let_def not_less)
ultimately show ?thesis
using assms 3(1) by (simp add: c_def)
next
case neg: 2
hence "EVD_cdf ξ 0 1 x = 1"
using 3 by (simp add: EVD_cdf_def Let_def)
moreover have "EVD_cdf ξ 0 1 (c * x + (c - 1) / ξ) = 1"
using neg argneg by (simp add: EVD_cdf_def Let_def not_less)
ultimately show ?thesis
using 3(1) by (simp add: c_def)
qed
qed
qed
end