Theory Survival_Model
theory Survival_Model
imports "HOL-Library.Rewrite" "HOL-Library.Extended_Nonnegative_Real" "HOL-Library.Extended_Real"
"HOL-Probability.Probability" Preliminaries
begin
section ‹Survival Model›
text ‹
The survival model is built on the probability space ‹𝔐›.
Additionally, the random variable ‹X : space 𝔐 → ℝ› is introduced,
which represents the age at death.
›
locale prob_space_actuary = MM_PS: prob_space 𝔐 for 𝔐
locale survival_model = prob_space_actuary +
fixes X :: "'a ⇒ real"
assumes X_RV[simp]: "MM_PS.random_variable (borel :: real measure) X"
and X_pos_AE[simp]: "AE ξ in 𝔐. X ξ > 0"
begin
subsection ‹General Theory of Survival Model›
interpretation distrX_RD: real_distribution "distr 𝔐 borel X"
using MM_PS.real_distribution_distr by simp
lemma X_le_event[simp]: "{ξ ∈ space 𝔐. X ξ ≤ x} ∈ MM_PS.events"
by measurable simp
lemma X_gt_event[simp]: "{ξ ∈ space 𝔐. X ξ > x} ∈ MM_PS.events"
by measurable simp
lemma X_compl_le_gt: "space 𝔐 - {ξ ∈ space 𝔐. X ξ ≤ x} = {ξ ∈ space 𝔐. X ξ > x}" for x::real
proof -
have "space 𝔐 - {ξ ∈ space 𝔐. X ξ ≤ x} = space 𝔐 - (X -` {..x})" by blast
also have "… = (X -` {x<..}) ∩ space 𝔐" using vimage_compl_atMost by fastforce
also have "… = {ξ ∈ space 𝔐. X ξ > x}" by blast
finally show ?thesis .
qed
lemma X_compl_gt_le: "space 𝔐 - {ξ ∈ space 𝔐. X ξ > x} = {ξ ∈ space 𝔐. X ξ ≤ x}" for x::real
using X_compl_le_gt by blast
subsubsection ‹Introduction of Survival Function for ‹X››
text ‹
Note that ‹ccdf (distr 𝔐 borel X)› is the survival (distributive) function for ‹X›.
›
lemma ccdfX_0_1: "ccdf (distr 𝔐 borel X) 0 = 1"
apply (rewrite MM_PS.ccdf_distr_P, simp)
using X_pos_AE MM_PS.prob_space
using MM_PS.prob_Collect_eq_1 X_gt_event by presburger
lemma ccdfX_unborn_1: "ccdf (distr 𝔐 borel X) x = 1" if "x ≤ 0"
proof (rule antisym)
show "ccdf (distr 𝔐 borel X) x ≤ 1" using MM_PS.ccdf_distr_P by simp
show "ccdf (distr 𝔐 borel X) x ≥ 1"
proof -
have "ccdf (distr 𝔐 borel X) x ≥ ccdf (distr 𝔐 borel X) 0"
using finite_borel_measure.ccdf_nonincreasing distrX_RD.finite_borel_measure_M that by simp
also have "ccdf (distr 𝔐 borel X) 0 = 1" using ccdfX_0_1 that by simp
finally show ?thesis .
qed
qed
definition death_pt :: ereal (‹$ψ›)
where "$ψ ≡ Inf (ereal ` {x ∈ ℝ. ccdf (distr 𝔐 borel X) x = 0})"
lemma psi_nonneg: "$ψ ≥ 0"
unfolding death_pt_def
proof (rule Inf_greatest)
fix x'::ereal
assume "x' ∈ ereal ` {x ∈ ℝ. ccdf (distr 𝔐 borel X) x = 0}"
then obtain x::real where "x' = ereal x" and "ccdf (distr 𝔐 borel X) x = 0" by blast
hence "ccdf (distr 𝔐 borel X) 0 > ccdf (distr 𝔐 borel X) x" using ccdfX_0_1 X_pos_AE by simp
hence "x ≥ 0"
using mono_invE finite_borel_measure.ccdf_nonincreasing distrX_RD.finite_borel_measure_M X_RV
by (smt(verit))
thus "x' ≥ 0" using ‹x' = ereal x› by simp
qed
lemma ccdfX_beyond_0: "ccdf (distr 𝔐 borel X) x = 0" if "x > $ψ" for x::real
proof -
have "ereal ` {y ∈ ℝ. ccdf (distr 𝔐 borel X) y = 0} ≠ {}" using death_pt_def that by force
hence "∃y'∈(ereal ` {y ∈ ℝ. ccdf (distr 𝔐 borel X) y = 0}). y' < ereal x"
using that unfolding death_pt_def by (rule cInf_lessD)
then obtain "y'"
where "y' ∈ (ereal ` {y ∈ ℝ. ccdf (distr 𝔐 borel X) y = 0})" and "y' < ereal x" by blast
then obtain y::real
where "y' = ereal y" and "ccdf (distr 𝔐 borel X) y = 0" and "ereal y < ereal x" by blast
hence "ccdf (distr 𝔐 borel X) y = 0" and "y < x" by simp_all
hence "ccdf (distr 𝔐 borel X) x ≤ 0"
using finite_borel_measure.ccdf_nonincreasing distrX_RD.finite_borel_measure_M X_RV
by (metis order_less_le)
thus ?thesis using finite_borel_measure.ccdf_nonneg distrX_RD.finite_borel_measure_M X_RV by smt
qed
lemma ccdfX_psi_0: "ccdf (distr 𝔐 borel X) (real_of_ereal $ψ) = 0" if "$ψ < ∞"
proof -
have "¦$ψ¦ ≠ ∞" using that psi_nonneg by simp
then obtain u::real where "$ψ = ereal u" using ereal_real' by blast
hence "real_of_ereal $ψ = u" by simp
moreover have "ccdf (distr 𝔐 borel X) u = 0"
proof -
have "⋀x::real. x ≠ u ⟹ x ∈ {u<..} ⟹ ccdf (distr 𝔐 borel X) x = 0"
by (rule ccdfX_beyond_0, simp add: ‹$ψ = ereal u›)
hence "(ccdf (distr 𝔐 borel X) ⤏ 0) (at_right u)"
apply -
by (rule iffD2[OF Lim_cong_within[where ?g="(λx.0)"]], simp_all+)
moreover have "(ccdf (distr 𝔐 borel X) ⤏ ccdf (distr 𝔐 borel X) u) (at_right u)"
using finite_borel_measure.ccdf_is_right_cont distrX_RD.finite_borel_measure_M
continuous_within X_RV by blast
ultimately show ?thesis using tendsto_unique trivial_limit_at_right_real by blast
qed
ultimately show ?thesis by simp
qed
lemma ccdfX_0_equiv: "ccdf (distr 𝔐 borel X) x = 0 ⟷ x ≥ $ψ" for x::real
proof
assume "ccdf (distr 𝔐 borel X) x = 0"
thus "ereal x ≥ $ψ" unfolding death_pt_def by (simp add: INF_lower)
next
assume "$ψ ≤ ereal x"
hence "$ψ = ereal x ∨ $ψ < ereal x" unfolding less_eq_ereal_def by auto
thus "ccdf (distr 𝔐 borel X) x = 0"
proof
assume ⋆: "$ψ = ereal x"
hence "$ψ < ∞" by simp
moreover have "real_of_ereal $ψ = x" using ⋆ by simp
ultimately show "ccdf (distr 𝔐 borel X) x = 0" using ccdfX_psi_0 by simp
next
assume "$ψ < ereal x"
thus "ccdf (distr 𝔐 borel X) x = 0" by (rule ccdfX_beyond_0)
qed
qed
lemma psi_pos[simp]: "$ψ > 0"
proof (rule not_le_imp_less, rule notI)
show "$ψ ≤ (0::ereal) ⟹ False"
proof -
assume "$ψ ≤ (0::ereal)"
hence "ccdf (distr 𝔐 borel X) 0 = 0" using ccdfX_0_equiv by (simp add: zero_ereal_def)
moreover have "ccdf (distr 𝔐 borel X) 0 = 1" using ccdfX_0_1 by simp
ultimately show "False" by simp
qed
qed
corollary psi_pos'[simp]: "$ψ > ereal 0"
using psi_pos zero_ereal_def by presburger
subsubsection ‹Introdution of Future-Lifetime Random Variable ‹T(x)››
definition alive :: "real ⇒ 'a set"
where "alive x ≡ {ξ ∈ space 𝔐. X ξ > x}"
lemma alive_event[simp]: "alive x ∈ MM_PS.events" for x::real
unfolding alive_def by simp
lemma X_alivex_measurable[measurable, simp]: "X ∈ borel_measurable (𝔐 ⇂ alive x)" for x::real
unfolding cond_prob_space_def by (measurable; simp add: measurable_restrict_space1)
definition futr_life :: "real ⇒ ('a ⇒ real)" (‹T›)
where "T x ≡ (λξ. X ξ - x)"
lemma T0_eq_X[simp]: "T 0 = X"
unfolding futr_life_def by simp
lemma Tx_measurable[measurable, simp]: "T x ∈ borel_measurable 𝔐" for x::real
unfolding futr_life_def by (simp add: borel_measurable_diff)
lemma Tx_alivex_measurable[measurable, simp]: "T x ∈ borel_measurable (𝔐 ⇂ alive x)" for x::real
unfolding futr_life_def by (simp add: borel_measurable_diff)
lemma alive_T: "alive x = {ξ ∈ space 𝔐. T x ξ > 0}" for x::real
unfolding alive_def futr_life_def by force
lemma alivex_Tx_pos[simp]: "0 < T x ξ" if "ξ ∈ space (𝔐 ⇂ alive x)" for x::real
using MM_PS.space_cond_prob_space alive_T that by simp
lemma PT0_eq_PX_lborel: "𝒫(ξ in 𝔐. T 0 ξ ∈ A ¦ T 0 ξ > 0) = 𝒫(ξ in 𝔐. X ξ ∈ A)"
if "A ∈ sets lborel" for A :: "real set"
apply (rewrite MM_PS.cond_prob_AE_prob, simp_all)
using that X_RV measurable_lborel1 predE pred_sets2 by blast
subsubsection ‹Actuarial Notations on the Survival Model›
definition survive :: "real ⇒ real ⇒ real" (‹$p'_{_&_}› [0,0] 200)
where "$p_{t&x} ≡ ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t"
abbreviation survive_1 :: "real ⇒ real" (‹$p'__› [101] 200)
where "$p_x ≡ $p_{1&x}"
definition die :: "real ⇒ real ⇒ real" (‹$q'_{_&_}› [0,0] 200)
where "$q_{t&x} ≡ cdf (distr (𝔐 ⇂ alive x) borel (T x)) t"
abbreviation die_1 :: "real ⇒ real" (‹$q'__› [101] 200)
where "$q_x ≡ $q_{1&x}"
definition die_defer :: "real ⇒ real ⇒ real ⇒ real" (‹$q'_{_¦_&_}› [0,0,0] 200)
where "$q_{f¦t&x} = ¦$q_{f+t&x} - $q_{f&x}¦"
abbreviation die_defer_1 :: "real ⇒ real ⇒ real" (‹$q'_{_¦&_}› [0,0] 200)
where "$q_{f¦&x} ≡ $q_{f¦1&x}"
definition life_expect :: "real ⇒ real" (‹$e`∘'__› [101] 200)
where "$e`∘_x ≡ integral⇧L (𝔐 ⇂ alive x) (T x)"
definition temp_life_expect :: "real ⇒ real ⇒real" (‹$e`∘'_{_:_}› [0,0] 200)
where "$e`∘_{x:n} ≡ integral⇧L (𝔐 ⇂ alive x) (λξ. min (T x ξ) n)"
definition curt_life_expect :: "real ⇒ real" (‹$e'__› [101] 200)
where "$e_x ≡ integral⇧L (𝔐 ⇂ alive x) (λξ. ⌊T x ξ⌋)"
definition temp_curt_life_expect :: "real ⇒ real ⇒ real" (‹$e'_{_:_}› [0,0] 200)
where "$e_{x:n} ≡ integral⇧L (𝔐 ⇂ alive x) (λξ. ⌊min (T x ξ) n⌋)"
subsubsection ‹Properties of Survival Function for ‹T(x)››
context
fixes x::real
assumes x_lt_psi[simp]: "x < $ψ"
begin
lemma PXx_pos[simp]: "𝒫(ξ in 𝔐. X ξ > x) > 0"
proof -
have "𝒫(ξ in 𝔐. X ξ > x) = ccdf (distr 𝔐 borel X) x"
unfolding alive_def using MM_PS.ccdf_distr_P by simp
also have "… > 0"
using ccdfX_0_equiv distrX_RD.ccdf_nonneg x_lt_psi by (smt (verit) linorder_not_le)
finally show ?thesis .
qed
lemma PTx_pos[simp]: "𝒫(ξ in 𝔐. T x ξ > 0) > 0"
apply (rewrite alive_T[THEN sym])
unfolding alive_def by simp
interpretation alivex_PS: prob_space "𝔐 ⇂ alive x"
by (rule MM_PS.cond_prob_space_correct, simp_all add: alive_def)
interpretation distrTx_RD: real_distribution "distr (𝔐 ⇂ alive x) borel (T x)" by simp
lemma ccdfTx_cond_prob:
"ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 𝒫(ξ in 𝔐. T x ξ > t ¦ T x ξ > 0)" for t::real
apply (rewrite alivex_PS.ccdf_distr_P, simp)
unfolding alive_def
apply (rewrite MM_PS.cond_prob_space_cond_prob[THEN sym], simp_all add: pred_def)
unfolding futr_life_def by simp
lemma ccdfTx_0_1: "ccdf (distr (𝔐 ⇂ alive x) borel (T x)) 0 = 1"
apply (rewrite ccdfTx_cond_prob)
unfolding futr_life_def cond_prob_def
by (smt (verit, best) Collect_cong PXx_pos divide_eq_1_iff)
lemma ccdfTx_nonpos_1: "ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 1" if "t ≤ 0" for t :: real
using antisym ccdfTx_0_1 that
by (metis distrTx_RD.ccdf_bounded_prob distrTx_RD.ccdf_nonincreasing)
lemma ccdfTx_0_equiv: "ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 0 ⟷ x+t ≥ $ψ" for t::real
proof -
have "ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t =
𝒫(ξ in 𝔐. X ξ > x+t ∧ X ξ > x) / 𝒫(ξ in 𝔐. X ξ > x)"
apply (rewrite ccdfTx_cond_prob)
unfolding cond_prob_def futr_life_def by (smt (verit) Collect_cong)
hence "ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 0 ⟷
𝒫(ξ in 𝔐. X ξ > x+t ∧ X ξ > x) / 𝒫(ξ in 𝔐. X ξ > x) = 0"
by simp
also have "… ⟷ 𝒫(ξ in 𝔐. X ξ > x+t ∧ X ξ > x) = 0"
using x_lt_psi PXx_pos by (smt (verit) divide_eq_0_iff)
also have "… ⟷ x+t ≥ $ψ"
using ccdfX_0_equiv MM_PS.ccdf_distr_P
by (smt (verit) Collect_cong X_RV le_ereal_le linorder_not_le x_lt_psi)
finally show ?thesis .
qed
lemma ccdfTx_continuous_on_nonpos[simp]:
"continuous_on {..0} (ccdf (distr (𝔐 ⇂ alive x) borel (T x)))"
by (metis atMost_iff ccdfTx_nonpos_1 continuous_on_cong continuous_on_const)
lemma ccdfTx_differentiable_on_nonpos[simp]:
"(ccdf (distr (𝔐 ⇂ alive x) borel (T x))) differentiable_on {..0}"
by (rewrite differentiable_on_cong[where f="λ_. 1"]; simp add: ccdfTx_nonpos_1)
lemma ccdfTx_has_real_derivative_0_at_neg:
"(ccdf (distr (𝔐 ⇂ alive x) borel (T x)) has_real_derivative 0) (at t)" if "t < 0" for t::real
apply (rewrite has_real_derivative_iff_has_vector_derivative)
apply (rule has_vector_derivative_transform_within_open[of "λ_. 1" _ _ "{..<0}"])
using ccdfTx_nonpos_1 that by simp_all
lemma ccdfTx_integrable_Icc:
"set_integrable lborel {a..b} (ccdf (distr (𝔐 ⇂ alive x) borel (T x)))" for a b :: real
proof -
have "(∫⇧+t. ennreal (indicat_real {a..b} t * ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t) ∂lborel)
< ⊤"
proof -
have "(∫⇧+t. ennreal (indicat_real {a..b} t * ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t) ∂lborel)
≤ (∫⇧+t. ennreal (indicat_real {a..b} t) ∂lborel)"
apply (rule nn_integral_mono)
using distrTx_RD.ccdf_bounded
by (simp add: distrTx_RD.ccdf_bounded_prob indicator_times_eq_if(1))
also have "… = nn_integral lborel (indicator {a..b})" by (meson ennreal_indicator)
also have "… = emeasure lborel {a..b}" by (rewrite nn_integral_indicator; simp)
also have "… < ⊤"
using emeasure_lborel_Icc_eq ennreal_less_top infinity_ennreal_def by presburger
finally show ?thesis .
qed
thus ?thesis
unfolding set_integrable_def
apply (intro integrableI_nonneg, simp_all)
using distrTx_RD.ccdf_nonneg by (intro always_eventually) auto
qed
corollary ccdfTx_integrable_on_Icc:
"ccdf (distr (𝔐 ⇂ alive x) borel (T x)) integrable_on {a..b}" for a b :: real
using set_borel_integral_eq_integral ccdfTx_integrable_Icc by force
lemma ccdfTx_PX:
"ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 𝒫(ξ in 𝔐. X ξ > x+t) / 𝒫(ξ in 𝔐. X ξ > x)"
if "t ≥ 0" for t::real
apply (rewrite ccdfTx_cond_prob)
unfolding cond_prob_def futr_life_def PXx_pos by (smt (verit) Collect_cong that)
lemma ccdfTx_ccdfX: "ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t =
ccdf (distr 𝔐 borel X) (x + t) / ccdf (distr 𝔐 borel X) x"
if "t ≥ 0" for t::real
using ccdfTx_PX that MM_PS.ccdf_distr_P X_RV by presburger
lemma ccdfT0_eq_ccdfX: "ccdf (distr (𝔐 ⇂ alive 0) borel (T 0)) = ccdf (distr 𝔐 borel X)"
proof
fix x
show "ccdf (distr (𝔐 ⇂ alive 0) borel (T 0)) x = ccdf (distr 𝔐 borel X) x"
proof (cases ‹x ≥ 0›)
case True
thus ?thesis
using survival_model.ccdfTx_ccdfX[where x=0] ccdfX_0_1 survival_model_axioms by fastforce
next
case False
hence "x ≤ 0" by simp
thus ?thesis
apply (rewrite ccdfX_unborn_1, simp)
by (rewrite survival_model.ccdfTx_nonpos_1; simp add: survival_model_axioms)
qed
qed
lemma continuous_ccdfX_ccdfTx:
"continuous (at (x+t) within {x..}) (ccdf (distr 𝔐 borel X)) ⟷
continuous (at t within {0..}) (ccdf (distr (𝔐 ⇂ alive x) borel (T x)))"
if "t ≥ 0" for t::real
proof -
let ?srvl = "ccdf (distr 𝔐 borel X)"
have [simp]: "𝒫(ξ in 𝔐. X ξ > x) ≠ 0" using PXx_pos by force
have ⋆: "⋀u. u ≥ 0 ⟹ ccdf (distr (𝔐 ⇂ alive x) borel (T x)) u =
?srvl (x + u) / 𝒫(ξ in 𝔐. X ξ > x)"
using survive_def MM_PS.ccdf_distr_P ccdfTx_PX that by simp
have "continuous (at t within {0..}) (ccdf (distr (𝔐 ⇂ alive x) borel (T x))) ⟷
continuous (at t within {0..}) (λu. ?srvl (x+u) / 𝒫(ξ in 𝔐. x < X ξ))"
proof -
have "∀⇩F u in at t within {0..}. ccdf (distr (𝔐 ⇂ alive x) borel (T x)) u =
?srvl (x+u) / 𝒫(ξ in 𝔐. X ξ > x)"
using ⋆ by (rewrite eventually_at_topological, simp_all) blast
thus ?thesis
by (intro continuous_at_within_cong, simp_all add: ⋆ that)
qed
also have "… ⟷ continuous (at t within {0..}) (λu. ?srvl (x+u))"
by (rewrite at "_ = ⌑" continuous_cdivide_iff[of "𝒫(ξ in 𝔐. X ξ > x)"], simp_all)
also have "… ⟷ continuous (at (x+t) within {x..}) ?srvl"
proof
let ?subx = "λv. v-x"
assume LHS: "continuous (at t within {0..}) (λu. ?srvl (x+u))"
hence "continuous (at (?subx (x+t)) within ?subx ` {x..}) (λu. ?srvl (x+u))"
proof -
have "?subx ` {x..} = {0..}"
by (metis (no_types, lifting) add.commute add_uminus_conv_diff diff_self
image_add_atLeast image_cong)
thus ?thesis using LHS by simp
qed
moreover have "continuous (at (x+t) within {x..}) ?subx" by (simp add: continuous_diff)
ultimately have "continuous (at (x+t) within {x..}) (λu. ?srvl (x + (?subx u)))"
using continuous_within_compose2 by force
thus "continuous (at (x+t) within {x..}) ?srvl" by simp
next
assume RHS: "continuous (at (x+t) within {x..}) ?srvl"
hence "continuous (at ((plus x) t) within (plus x) ` {0..}) ?srvl" by simp
moreover have "continuous (at t within {0..}) (plus x)" by (simp add: continuous_add)
ultimately show "continuous (at t within {0..}) (λu. ?srvl (x+u))"
using continuous_within_compose2 by force
qed
finally show ?thesis by simp
qed
lemma isCont_ccdfX_ccdfTx:
"isCont (ccdf (distr 𝔐 borel X)) (x+t) ⟷
isCont (ccdf (distr (𝔐 ⇂ alive x) borel (T x))) t"
if "t > 0" for t::real
proof -
have "isCont (ccdf (distr 𝔐 borel X)) (x+t) ⟷
continuous (at (x+t) within {x<..}) (ccdf (distr 𝔐 borel X))"
by (smt (verit) at_within_open greaterThan_iff open_greaterThan that)
also have "… ⟷ continuous (at (x+t) within {x..}) (ccdf (distr 𝔐 borel X))"
by (meson Ioi_le_Ico calculation continuous_within_subset top_greatest)
also have "… ⟷ continuous (at t within {0..}) (ccdf (distr (𝔐 ⇂ alive x) borel (T x)))"
using that continuous_ccdfX_ccdfTx by force
also have "… ⟷ continuous (at t within {0<..}) (ccdf (distr (𝔐 ⇂ alive x) borel (T x)))"
by (metis Ioi_le_Ico at_within_open continuous_at_imp_continuous_at_within
continuous_within_subset greaterThan_iff open_greaterThan that)
also have "… ⟷ isCont (ccdf (distr (𝔐 ⇂ alive x) borel (T x))) t"
by (metis at_within_open greaterThan_iff open_greaterThan that)
finally show ?thesis .
qed
lemma has_real_derivative_ccdfX_ccdfTx:
"((ccdf (distr 𝔐 borel X)) has_real_derivative D) (at (x+t)) ⟷
((ccdf (distr (𝔐 ⇂ alive x) borel (T x))) has_real_derivative (D / 𝒫(ξ in 𝔐. X ξ > x))) (at t)"
if "t > 0" for t D :: real
proof -
have "((ccdf (distr (𝔐 ⇂ alive x) borel (T x))) has_real_derivative
(D / 𝒫(ξ in 𝔐. X ξ > x))) (at t) ⟷
((λt. (ccdf (distr 𝔐 borel X)) (x+t) / 𝒫(ξ in 𝔐. X ξ > x)) has_real_derivative
(D / 𝒫(ξ in 𝔐. X ξ > x))) (at t)"
proof -
let ?d = "t/2"
{ fix u::real assume "dist u t < ?d"
hence "u > 0" by (smt (verit) dist_real_def dist_triangle_half_r)
hence "ccdf (distr (𝔐 ⇂ alive x) borel (T x)) u =
ccdf (distr 𝔐 borel X) (x + u) / MM_PS.prob {ξ::'a ∈ space 𝔐. x < X ξ}"
using survive_def MM_PS.ccdf_distr_P ccdfTx_PX that by simp }
moreover have "?d > 0" using that by simp
ultimately show ?thesis
apply -
apply (rule DERIV_cong_ev, simp)
apply (rewrite eventually_nhds_metric, blast)
by simp
qed
also have "… ⟷ ((λt. (ccdf (distr 𝔐 borel X)) (x+t)) has_real_derivative D) (at t)"
using PXx_pos by (rewrite DERIV_cdivide_iff[of "𝒫(ξ in 𝔐. X ξ > x)", THEN sym]; force)
also have "… ⟷ (ccdf (distr 𝔐 borel X) has_real_derivative D) (at (x+t))"
by (simp add: DERIV_shift add.commute)
finally show ?thesis by simp
qed
lemma differentiable_ccdfX_ccdfTx:
"(ccdf (distr 𝔐 borel X)) differentiable at (x+t) ⟷
(ccdf (distr (𝔐 ⇂ alive x) borel (T x))) differentiable at t"
if "t > 0" for t::real
apply (rewrite differentiable_eq_field_differentiable_real)+
unfolding field_differentiable_def using has_real_derivative_ccdfX_ccdfTx that
by (smt (verit, del_insts) PXx_pos nonzero_mult_div_cancel_left)
subsubsection ‹Properties of ‹$p_{t&x}››
lemma p_0_1: "$p_{0&x} = 1"
unfolding survive_def using ccdfTx_0_1 by simp
lemma p_nonneg[simp]: "$p_{t&x} ≥ 0" for t::real
unfolding survive_def using distrTx_RD.ccdf_nonneg by simp
lemma p_le_1[simp]: "$p_{t&x} ≤ 1" for t::real
unfolding survive_def using distrTx_RD.ccdf_bounded_prob by auto
lemma p_0_equiv: "$p_{t&x} = 0 ⟷ x+t ≥ $ψ" for t::real
unfolding survive_def by (rule ccdfTx_0_equiv)
lemma p_PTx: "$p_{t&x} = 𝒫(ξ in 𝔐. T x ξ > t ¦ T x ξ > 0)" for t::real
unfolding survive_def using ccdfTx_cond_prob by simp
lemma p_PX: "$p_{t&x} = 𝒫(ξ in 𝔐. X ξ > x + t) / 𝒫(ξ in 𝔐. X ξ > x)" if "t ≥ 0" for t::real
unfolding survive_def using ccdfTx_PX that by simp
lemma p_mult: "$p_{t+t' & x} = $p_{t&x} * $p_{t' & x+t}"
if "t ≥ 0" "t' ≥ 0" "x+t < $ψ" for t t' :: real
proof -
have "$p_{t+t' & x} = 𝒫(ξ in 𝔐. X ξ > x+t+t') / 𝒫(ξ in 𝔐. X ξ > x)"
apply (rewrite p_PX; (simp add: that)?)
by (rule disjI2, smt (verit, best) Collect_cong)
also have "… = (𝒫(ξ in 𝔐. X ξ > x+t+t') / 𝒫(ξ in 𝔐. X ξ > x+t)) *
(𝒫(ξ in 𝔐. X ξ > x+t) / 𝒫(ξ in 𝔐. X ξ > x))"
using that survival_model.PXx_pos survival_model_axioms by fastforce
also have "… = $p_{t&x} * $p_{t' & x+t}"
apply (rewrite p_PX, simp add: that)
by (rewrite survival_model.p_PX, simp_all add: that survival_model_axioms)
finally show ?thesis .
qed
lemma p_PTx_ge_ccdf_isCont: "$p_{t&x} = 𝒫(ξ in 𝔐. T x ξ ≥ t ¦ T x ξ > 0)"
if "isCont (ccdf (distr 𝔐 borel X)) (x+t)" "t > 0" for t::real
unfolding survive_def using that isCont_ccdfX_ccdfTx
apply (rewrite alivex_PS.ccdf_continuous_distr_P_ge, simp_all)
by (rewrite MM_PS.cond_prob_space_cond_prob, simp_all add: alive_T)
end
subsubsection ‹Properties of Survival Function for ‹X››
lemma ccdfX_continuous_unborn[simp]: "continuous_on {..0} (ccdf (distr 𝔐 borel X))"
using ccdfTx_continuous_on_nonpos by (metis ccdfT0_eq_ccdfX psi_pos')
lemma ccdfX_differentiable_unborn[simp]: "(ccdf (distr 𝔐 borel X)) differentiable_on {..0}"
using ccdfTx_differentiable_on_nonpos by (metis ccdfT0_eq_ccdfX psi_pos')
lemma ccdfX_has_real_derivative_0_unborn:
"(ccdf (distr 𝔐 borel X) has_real_derivative 0) (at x)" if "x < 0" for x::real
using ccdfTx_has_real_derivative_0_at_neg by (metis ccdfT0_eq_ccdfX psi_pos' that)
lemma ccdfX_integrable_Icc:
"set_integrable lborel {a..b} (ccdf (distr 𝔐 borel X))" for a b :: real
using ccdfTx_integrable_Icc by (metis ccdfT0_eq_ccdfX psi_pos')
corollary ccdfX_integrable_on_Icc:
"ccdf (distr 𝔐 borel X) integrable_on {a..b}" for a b :: real
using set_borel_integral_eq_integral ccdfX_integrable_Icc by force
lemma ccdfX_p: "ccdf (distr 𝔐 borel X) x = $p_{x&0}" for x::real
by (metis ccdfT0_eq_ccdfX survive_def psi_pos')
subsubsection ‹Introduction of Cumulative Distributive Function for ‹X››
lemma cdfX_0_0: "cdf (distr 𝔐 borel X) 0 = 0"
using ccdfX_0_1 distrX_RD.ccdf_cdf distrX_RD.prob_space by fastforce
lemma cdfX_unborn_0: "cdf (distr 𝔐 borel X) x = 0" if "x ≤ 0"
using ccdfX_unborn_1 cdfX_0_0 distrX_RD.cdf_ccdf that by fastforce
lemma cdfX_beyond_1: "cdf (distr 𝔐 borel X) x = 1" if "x > $ψ" for x::real
using ccdfX_beyond_0 distrX_RD.cdf_ccdf that distrX_RD.prob_space by force
lemma cdfX_psi_1: "cdf (distr 𝔐 borel X) (real_of_ereal $ψ) = 1" if "$ψ < ∞"
using ccdfX_psi_0 distrX_RD.cdf_ccdf distrX_RD.prob_space that by fastforce
lemma cdfX_1_equiv: "cdf (distr 𝔐 borel X) x = 1 ⟷ x ≥ $ψ" for x::real
using ccdfX_0_equiv distrX_RD.cdf_ccdf distrX_RD.prob_space by force
subsubsection ‹Properties of Cumulative Distributive Function for ‹T(x)››
context
fixes x::real
assumes x_lt_psi[simp]: "x < $ψ"
begin
interpretation alivex_PS: prob_space "𝔐 ⇂ alive x"
by (rule MM_PS.cond_prob_space_correct, simp_all add: alive_def)
interpretation distrTx_RD: real_distribution "distr (𝔐 ⇂ alive x) borel (T x)" by simp
lemma cdfTx_cond_prob:
"cdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 𝒫(ξ in 𝔐. T x ξ ≤ t ¦ T x ξ > 0)" for t::real
apply (rewrite distrTx_RD.cdf_ccdf, rewrite distrTx_RD.prob_space)
apply (rewrite ccdfTx_cond_prob, simp)
by (rewrite not_less[THEN sym], rewrite MM_PS.cond_prob_neg; simp)
lemma cdfTx_0_0: "cdf (distr (𝔐 ⇂ alive x) borel (T x)) 0 = 0"
using ccdfTx_0_1 distrTx_RD.cdf_ccdf distrTx_RD.prob_space by force
lemma cdfTx_nonpos_0: "cdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 0" if "t ≤ 0" for t :: real
using ccdfTx_nonpos_1 distrTx_RD.cdf_ccdf distrTx_RD.prob_space that by force
lemma cdfTx_1_equiv: "cdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 1 ⟷ x+t ≥ $ψ" for t::real
using ccdfTx_0_equiv distrTx_RD.cdf_ccdf distrTx_RD.prob_space by force
lemma cdfTx_continuous_on_nonpos[simp]:
"continuous_on {..0} (cdf (distr (𝔐 ⇂ alive x) borel (T x)))"
by (rewrite continuous_on_cong[where g="λt. 0"]) (simp_all add: cdfTx_nonpos_0)+
lemma cdfTx_differentiable_on_nonpos[simp]:
"(cdf (distr (𝔐 ⇂ alive x) borel (T x))) differentiable_on {..0}"
by (rewrite differentiable_on_cong[where f="λt. 0"]; simp add: cdfTx_nonpos_0)
lemma cdfTx_has_real_derivative_0_at_neg:
"(cdf (distr (𝔐 ⇂ alive x) borel (T x)) has_real_derivative 0) (at t)" if "t < 0" for t::real
apply (rewrite has_real_derivative_iff_has_vector_derivative)
apply (rule has_vector_derivative_transform_within_open[of "λ_. 0" _ _ "{..<0}"])
using cdfTx_nonpos_0 that by simp_all
lemma cdfTx_integrable_Icc:
"set_integrable lborel {a..b} (cdf (distr (𝔐 ⇂ alive x) borel (T x)))" for a b :: real
proof -
have "set_integrable lborel {a..b} (λ_. 1::real)"
unfolding set_integrable_def
using emeasure_compact_finite by (simp, intro integrable_real_indicator; force)
thus ?thesis
apply (rewrite distrTx_RD.cdf_ccdf, rewrite distrTx_RD.prob_space)
using ccdfTx_integrable_Icc by (rewrite set_integral_diff; simp)
qed
corollary cdfTx_integrable_on_Icc:
"cdf (distr (𝔐 ⇂ alive x) borel (T x)) integrable_on {a..b}" for a b :: real
using cdfTx_integrable_Icc set_borel_integral_eq_integral by force
lemma cdfTx_PX:
"cdf (distr (𝔐 ⇂ alive x) borel (T x)) t = 𝒫(ξ in 𝔐. x < X ξ ∧ X ξ ≤ x+t) / 𝒫(ξ in 𝔐. X ξ > x)"
for t::real
apply (rewrite cdfTx_cond_prob)
unfolding cond_prob_def futr_life_def PXx_pos by (smt (verit) Collect_cong)
lemma cdfT0_eq_cdfX: "cdf (distr (𝔐 ⇂ alive 0) borel (T 0)) = cdf (distr 𝔐 borel X)"
proof
interpret alive0_PS: prob_space "𝔐 ⇂ alive 0"
apply (rule MM_PS.cond_prob_space_correct, simp)
using PXx_pos alive_def psi_pos' by presburger
interpret distrT0_RD: real_distribution "distr (𝔐 ⇂ alive 0) borel (T 0)" by simp
show "⋀x. cdf (distr (𝔐 ⇂ alive 0) borel (T 0)) x = cdf (distr 𝔐 borel X) x"
using ccdfT0_eq_ccdfX distrX_RD.ccdf_cdf distrT0_RD.ccdf_cdf
by (smt (verit, best) distrT0_RD.prob_space distrX_RD.prob_space psi_pos')
qed
lemma continuous_cdfX_cdfTx:
"continuous (at (x+t) within {x..}) (cdf (distr 𝔐 borel X)) ⟷
continuous (at t within {0..}) (cdf (distr (𝔐 ⇂ alive x) borel (T x)))"
if "t ≥ 0" for t::real
proof -
have "continuous (at (x+t) within {x..}) (cdf (distr 𝔐 borel X)) ⟷
continuous (at (x+t) within {x..}) (ccdf (distr 𝔐 borel X))"
by (rule distrX_RD.continuous_cdf_ccdf)
also have "… ⟷ continuous (at t within {0..}) (ccdf (distr (𝔐 ⇂ alive x) borel (T x)))"
using continuous_ccdfX_ccdfTx that by simp
also have "… ⟷ continuous (at t within {0..}) (cdf (distr (𝔐 ⇂ alive x) borel (T x)))"
using distrTx_RD.continuous_cdf_ccdf by simp
finally show ?thesis .
qed
lemma isCont_cdfX_cdfTx:
"isCont (cdf (distr 𝔐 borel X)) (x+t) ⟷
isCont (cdf (distr (𝔐 ⇂ alive x) borel (T x))) t"
if "t > 0" for t::real
apply (rewrite distrX_RD.isCont_cdf_ccdf)
apply (rewrite isCont_ccdfX_ccdfTx, simp_all add: that)
by (rule distrTx_RD.isCont_cdf_ccdf[THEN sym])
lemma has_real_derivative_cdfX_cdfTx:
"((cdf (distr 𝔐 borel X)) has_real_derivative D) (at (x+t)) ⟷
((cdf (distr (𝔐 ⇂ alive x) borel (T x))) has_real_derivative (D / 𝒫(ξ in 𝔐. X ξ > x))) (at t)"
if "t > 0" for t D :: real
proof -
have "((cdf (distr 𝔐 borel X)) has_real_derivative D) (at (x+t)) ⟷
(ccdf (distr 𝔐 borel X) has_real_derivative -D) (at (x+t))"
using distrX_RD.has_real_derivative_cdf_ccdf by force
also have "… ⟷
((ccdf (distr (𝔐 ⇂ alive x) borel (T x))) has_real_derivative (-D / 𝒫(ξ in 𝔐. X ξ > x))) (at t)"
using has_real_derivative_ccdfX_ccdfTx that by simp
also have "… ⟷
((cdf (distr (𝔐 ⇂ alive x) borel (T x))) has_real_derivative (D / 𝒫(ξ in 𝔐. X ξ > x))) (at t)"
by (simp add: distrTx_RD.has_real_derivative_cdf_ccdf)
finally show ?thesis .
qed
lemma differentiable_cdfX_cdfTx:
"(cdf (distr 𝔐 borel X)) differentiable at (x+t) ⟷
(cdf (distr (𝔐 ⇂ alive x) borel (T x))) differentiable at t"
if "t > 0" for t::real
apply (rewrite differentiable_eq_field_differentiable_real)+
unfolding field_differentiable_def using has_real_derivative_cdfX_cdfTx that
by (meson differentiable_ccdfX_ccdfTx distrTx_RD.finite_borel_measure_axioms
distrX_RD.finite_borel_measure_axioms finite_borel_measure.differentiable_cdf_ccdf
real_differentiable_def x_lt_psi)
subsubsection ‹Properties of ‹$q_{t&x}››
lemma q_nonpos_0: "$q_{t&x} = 0" if "t ≤ 0" for t::real
unfolding die_def using that cdfTx_nonpos_0 by simp
corollary q_0_0: "$q_{0&x} = 0"
using q_nonpos_0 by simp
lemma q_nonneg[simp]: "$q_{t&x} ≥ 0" for t::real
unfolding die_def using distrTx_RD.cdf_nonneg by simp
lemma q_le_1[simp]: "$q_{t&x} ≤ 1" for t::real
unfolding die_def using distrTx_RD.cdf_bounded_prob by force
lemma q_1_equiv: "$q_{t&x} = 1 ⟷ x+t ≥ $ψ" for t::real
unfolding die_def using cdfTx_1_equiv by simp
lemma q_PTx: "$q_{t&x} = 𝒫(ξ in 𝔐. T x ξ ≤ t ¦ T x ξ > 0)" for t::real
unfolding die_def using cdfTx_cond_prob by simp
lemma q_PX: "$q_{t&x} = 𝒫(ξ in 𝔐. x < X ξ ∧ X ξ ≤ x + t) / 𝒫(ξ in 𝔐. X ξ > x)"
unfolding die_def using cdfTx_PX by simp
lemma q_defer_0_q[simp]: "$q_{0¦t&x} = $q_{t&x}" for t::real
unfolding die_defer_def using q_0_0 by simp
lemma q_defer_0_0: "$q_{f¦0&x} = 0" for f::real
unfolding die_defer_def by simp
lemma q_defer_nonneg[simp]: "$q_{f¦t&x} ≥ 0" for f t :: real
unfolding die_defer_def by simp
lemma q_defer_q: "$q_{f¦t&x} = $q_{f+t & x} - $q_{f&x}" if "t ≥ 0" for f t :: real
unfolding die_defer_def die_def using distrTx_RD.cdf_nondecreasing that by simp
corollary q_defer_le_1[simp]: "$q_{f¦t&x} ≤ 1" if "t ≥ 0" for f t :: real
by (smt (verit, ccfv_SIG) q_defer_q q_le_1 q_nonneg that)
lemma q_defer_PTx: "$q_{f¦t&x} = 𝒫(ξ in 𝔐. f < T x ξ ∧ T x ξ ≤ f + t ¦ T x ξ > 0)"
if "t ≥ 0" for f t :: real
proof -
have "$q_{f¦t&x} = $q_{f+t & x} - $q_{f&x}" using q_defer_q that by simp
also have "… = 𝒫(ξ in 𝔐. T x ξ ≤ f + t ¦ T x ξ > 0) - 𝒫(ξ in 𝔐. T x ξ ≤ f ¦ T x ξ > 0)"
using q_PTx by simp
also have "… = 𝒫(ξ in (𝔐 ⇂ alive x). T x ξ ≤ f + t) - 𝒫(ξ in (𝔐 ⇂ alive x). T x ξ ≤ f)"
using MM_PS.cond_prob_space_cond_prob alive_T by simp
also have "… = 𝒫(ξ in (𝔐 ⇂ alive x). f < T x ξ ∧ T x ξ ≤ f + t)"
proof -
have "{ξ ∈ space (𝔐 ⇂ alive x). T x ξ ≤ f + t} - {ξ ∈ space (𝔐 ⇂ alive x). T x ξ ≤ f} =
{ξ ∈ space (𝔐 ⇂ alive x). f < T x ξ ∧ T x ξ ≤ f + t}"
using that by force
hence "alivex_PS.prob
({ξ ∈ space (𝔐 ⇂ alive x). T x ξ ≤ f + t} - {ξ ∈ space (𝔐 ⇂ alive x). T x ξ ≤ f}) =
𝒫(ξ in (𝔐 ⇂ alive x). f < T x ξ ∧ T x ξ ≤ f + t)"
by simp
moreover have "{ξ ∈ space (𝔐 ⇂ alive x). T x ξ ≤ f} ⊆ {ξ ∈ space (𝔐 ⇂ alive x). T x ξ ≤ f + t}"
using that by force
ultimately show ?thesis by (rewrite alivex_PS.finite_measure_Diff[THEN sym]; simp)
qed
also have "… = 𝒫(ξ in 𝔐. f < T x ξ ∧ T x ξ ≤ f + t ¦ T x ξ > 0)"
using MM_PS.cond_prob_space_cond_prob alive_T by simp
finally show ?thesis .
qed
lemma q_defer_PX: "$q_{f¦t&x} = 𝒫(ξ in 𝔐. x + f < X ξ ∧ X ξ ≤ x + f + t) / 𝒫(ξ in 𝔐. X ξ > x)"
if "f ≥ 0" "t ≥ 0" for f t :: real
proof -
have "$q_{f¦t&x} = 𝒫(ξ in 𝔐. f < T x ξ ∧ T x ξ ≤ f + t ∧ T x ξ > 0) / 𝒫(ξ in 𝔐. T x ξ > 0)"
apply (rewrite q_defer_PTx; (simp add: that)?)
unfolding cond_prob_def by simp
also have "… = 𝒫(ξ in 𝔐. f < T x ξ ∧ T x ξ ≤ f + t) / 𝒫(ξ in 𝔐. T x ξ > 0)"
proof -
have "⋀ξ. ξ ∈ space 𝔐 ⟹ f < T x ξ ∧ T x ξ ≤ f + t ∧ T x ξ > 0 ⟷ f < T x ξ ∧ T x ξ ≤ f + t"
using that by auto
hence "{ξ ∈ space 𝔐. f < T x ξ ∧ T x ξ ≤ f + t ∧ T x ξ > 0} =
{ξ ∈ space 𝔐. f < T x ξ ∧ T x ξ ≤ f + t}" by blast
thus ?thesis by simp
qed
also have "… = 𝒫(ξ in 𝔐. x + f < X ξ ∧ X ξ ≤ x + f + t) / 𝒫(ξ in 𝔐. X ξ > x)"
unfolding futr_life_def by (smt (verit) Collect_cong)
finally show ?thesis .
qed
lemma q_defer_old_0: "$q_{f¦t&x} = 0" if "x+f ≥ $ψ" "t ≥ 0" for f t :: real
proof -
have "$q_{f¦t&x} = $q_{f+t & x} - $q_{f&x}" using q_defer_q that by simp
moreover have "$q_{f+t & x} = 1" using q_1_equiv that le_ereal_le by auto
moreover have "$q_{f&x} = 1" using q_1_equiv that by simp
ultimately show ?thesis by simp
qed
end
subsubsection ‹Properties of Cumulative Distributive Function for ‹X››
lemma cdfX_continuous_unborn[simp]: "continuous_on {..0} (cdf (distr 𝔐 borel X))"
using cdfTx_continuous_on_nonpos by (metis cdfT0_eq_cdfX psi_pos')
lemma cdfX_differentiable_unborn[simp]: "(cdf (distr 𝔐 borel X)) differentiable_on {..0}"
using cdfTx_differentiable_on_nonpos by (metis cdfT0_eq_cdfX psi_pos')
lemma cdfX_has_real_derivative_0_unborn:
"(cdf (distr 𝔐 borel X) has_real_derivative 0) (at x)" if "x < 0" for x::real
using cdfTx_has_real_derivative_0_at_neg by (metis cdfT0_eq_cdfX psi_pos' that)
lemma cdfX_integrable_Icc:
"set_integrable lborel {a..b} (cdf (distr 𝔐 borel X))" for a b :: real
using cdfTx_integrable_Icc by (metis cdfT0_eq_cdfX psi_pos')
corollary cdfX_integrable_on_Icc:
"cdf (distr 𝔐 borel X) integrable_on {a..b}" for a b :: real
using cdfX_integrable_Icc set_borel_integral_eq_integral by force
lemma cdfX_q: "cdf (distr 𝔐 borel X) x = $q_{x&0}" if "x ≥ 0" for x::real
by (metis cdfT0_eq_cdfX die_def psi_pos')
subsubsection ‹Relations between ‹$p_{t&x}› and ‹$q_{t&x}››
context
fixes x::real
assumes x_lt_psi[simp]: "x < $ψ"
begin
interpretation alivex_PS: prob_space "𝔐 ⇂ alive x"
by (rule MM_PS.cond_prob_space_correct, simp_all add: alive_def)
interpretation distrTx_RD: real_distribution "distr (𝔐 ⇂ alive x) borel (T x)" by simp
lemma p_q_1: "$p_{t&x} + $q_{t&x} = 1" for t::real
unfolding survive_def die_def using distrTx_RD.add_cdf_ccdf
by (smt (verit) distrTx_RD.prob_space x_lt_psi)
lemma q_defer_p: "$q_{f¦t&x} = $p_{f&x} - $p_{f+t & x}" if "t ≥ 0" for f t :: real
using q_defer_q p_q_1 that x_lt_psi by smt
lemma q_defer_p_q_defer: "$p_{f&x} * $q_{f'¦t & x+f} = $q_{f+f'¦t & x}"
if "x+f < $ψ" "f ≥ 0" "f' ≥ 0" "t ≥ 0" for f f' t :: real
proof -
have "$p_{f&x} * $q_{f'¦t & x+f} =
𝒫(ξ in 𝔐. X ξ > x+f) / 𝒫(ξ in 𝔐. X ξ > x) *
𝒫(ξ in 𝔐. x+f+f' < X ξ ∧ X ξ ≤ x+f+f'+t) / 𝒫(ξ in 𝔐. X ξ > x+f)"
apply (rewrite p_PX, (simp_all add: that)[2])
by (rewrite survival_model.q_defer_PX, simp_all add: that survival_model_axioms)
also have "… = 𝒫(ξ in 𝔐. x+f+f' < X ξ ∧ X ξ ≤ x+f+f'+t) / 𝒫(ξ in 𝔐. X ξ > x)"
using survival_model.PXx_pos[of 𝔐 X "x+f"] nonzero_mult_div_cancel_left that
by (smt (verit, ccfv_SIG) survival_model_axioms times_divide_eq_left times_divide_eq_right)
also have "… = $q_{f+f'¦t & x}"
by (rewrite q_defer_PX; simp add: that group_cancel.add1)
finally show ?thesis .
qed
lemma q_defer_pq: "$q_{f¦t&x} = $p_{f&x} * $q_{t & x+f}"
if "x+f < $ψ" "t ≥ 0" "f ≥ 0" for f t :: real
using q_defer_p_q_defer[where f'=0] that
by (simp add: survival_model.q_defer_0_q survival_model_axioms)
subsubsection ‹Properties of Life Expectation›
lemma e_nonneg: "$e`∘_x ≥ 0"
unfolding life_expect_def
by (rule Bochner_Integration.integral_nonneg, simp add: less_eq_real_def)
lemma e_P: "$e`∘_x =
MM_PS.expectation (λξ. indicator (alive x) ξ * T x ξ) / 𝒫(ξ in 𝔐. T x ξ > 0)"
unfolding life_expect_def
by (rewrite MM_PS.integral_cond_prob_space_nn, auto simp add: alive_T)
proposition nn_integral_T_p:
"(∫⇧+ξ. ennreal (T x ξ) ∂(𝔐 ⇂ alive x)) = (∫⇧+t∈{0..}. ennreal ($p_{t&x}) ∂lborel)"
apply (rewrite alivex_PS.expectation_nonneg_tail, simp_all add: less_imp_le)
apply (rule nn_integral_cong)
unfolding survive_def using distrTx_RD.prob_space distrTx_RD.ccdf_cdf by presburger
lemma nn_integral_T_pos: "(∫⇧+ξ. ennreal (T x ξ) ∂(𝔐 ⇂ alive x)) > 0"
proof -
let ?f = "λt. - ccdf (distr (𝔐 ⇂ alive x) borel (T x)) t"
have "⋀t u. t ≤ u ⟹ ?f t ≤ ?f u" using distrTx_RD.ccdf_nonincreasing by simp
moreover have "continuous (at_right 0) ?f"
using distrTx_RD.ccdf_is_right_cont by (intro continuous_intros)
ultimately have "∀e>0. ∃d>0. ?f (0 + d) - ?f 0 < e"
using continuous_at_right_real_increasing by simp
hence "∃d>0. ?f (0 + d) - ?f 0 < 1/2" by (smt (verit, del_insts) field_sum_of_halves)
from this obtain d where d_pos: "d > 0" and "$p_{d&x} ≥ 1/2"
using p_0_1 unfolding survive_def by auto
hence "⋀t. t∈{0..d} ⟹ $p_{t&x} ≥ 1/2"
unfolding survive_def using distrTx_RD.ccdf_nonincreasing by force
hence "(∫⇧+t∈{0..d}. ennreal ($p_{t&x}) ∂lborel) ≥ (∫⇧+t∈{0..d}. ennreal (1/2) ∂lborel)"
apply (intro nn_set_integral_mono, simp_all)
unfolding survive_def using Tx_alivex_measurable apply force
by (rule AE_I2) (smt (verit) ennreal_half ennreal_leI half_bounded_equal)
moreover have "(∫⇧+t∈{0..}. ennreal ($p_{t&x}) ∂lborel) ≥ (∫⇧+t∈{0..d}. ennreal ($p_{t&x}) ∂lborel)"
by (rule nn_set_integral_set_mono) simp
moreover have "(∫⇧+t∈{0..d}. ennreal (1/2) ∂lborel) > 0"
apply (rewrite nn_integral_cmult_indicator, simp_all)
using d_pos emeasure_lborel_Icc ennreal_zero_less_mult_iff by fastforce
ultimately show ?thesis using nn_integral_T_p by simp
qed
lemma e_pos_Tx: "$e`∘_x > 0" if "integrable (𝔐 ⇂ alive x) (T x)"
unfolding life_expect_def
apply (rewrite integral_eq_nn_integral, simp_all)
apply (smt (verit, ccfv_SIG) AE_I2 alivex_Tx_pos)
using nn_integral_T_pos that
by (smt (verit) AE_I2 alivex_Tx_pos enn2real_ennreal ennreal_less_zero_iff
nn_integral_cong nn_integral_eq_integral)
proposition e_LBINT_p: "$e`∘_x = (LBINT t:{0..}. $p_{t&x})"
unfolding life_expect_def apply (rewrite integral_eq_nn_integral, simp_all add: less_imp_le)
unfolding set_lebesgue_integral_def apply (rewrite integral_eq_nn_integral, simp_all)
apply (measurable, simp add: survive_def)
by (rewrite nn_integral_T_p) (simp add: indicator_mult_ennreal mult.commute)
corollary e_integral_p: "$e`∘_x = integral {0..} (λt. $p_{t&x})"
proof -
have "$e`∘_x = (LBINT t:{0..}. $p_{t&x})" using e_LBINT_p by simp
also have "… = integral {0..} (λt. $p_{t&x})"
apply (rule set_borel_integral_eq_integral_nonneg, simp_all)
unfolding survive_def by simp
finally show ?thesis .
qed
lemma e_pos: "$e`∘_x > 0" if "set_integrable lborel {0..} (λt. $p_{t&x})"
proof -
have "(∫⇧+t∈{0..}. ennreal ($p_{t&x}) ∂lborel) = ennreal (∫t∈{0..}. $p_{t&x} ∂lborel)"
by (intro set_nn_integral_eq_set_integral; simp add: that)
also have "… < ∞" using that by simp
finally have "(∫⇧+ξ. ennreal (T x ξ) ∂(𝔐 ⇂ alive x)) < ∞" using nn_integral_T_p by simp
hence "integrable (𝔐 ⇂ alive x) (T x)"
by (smt (verit) alivex_Tx_pos integrableI_bounded nn_integral_cong real_norm_def
survival_model.Tx_alivex_measurable survival_model_axioms)
thus ?thesis by (rule e_pos_Tx)
qed
corollary e_pos': "$e`∘_x > 0" if "(λt. $p_{t&x}) integrable_on {0..}"
apply (rule e_pos)
using that apply (rewrite integrable_on_iff_set_integrable_nonneg; simp)
unfolding survive_def by simp
lemma e_LBINT_p_Icc: "$e`∘_x = (LBINT t:{0..n}. $p_{t&x})" if "x+n ≥ $ψ" for n::real
proof -
have [simp]: "{0..n} ∩ {n<..} = {}" using ivl_disj_int_one(7) by blast
have [simp]: "{0..n} ∪ {n<..} = {0..}"
by (smt (verit) ereal_less_le ivl_disj_un_one(7) leD that x_lt_psi)
have [simp]: "⋀t. n < t ⟹ 0 ≤ t" using that x_lt_psi by (smt (verit) ereal_less_le leD)
have [simp]: "⋀t. n < t ⟹ $ψ ≤ ereal (x+t)" using that by (simp add: le_ereal_le)
have gt_n_0: "has_bochner_integral lborel (λt. indicat_real {n<..} t * $p_{t&x}) 0"
apply (rewrite has_bochner_integral_cong[where N=lborel and g="λt.0" and y=0], simp_all)
using p_0_equiv that x_lt_psi
apply (smt (verit, ccfv_SIG) greaterThan_iff indicator_simps le_ereal_le linorder_not_le)
by (rule has_bochner_integral_zero)
hence gt_n: "set_integrable lborel {n<..} (λt. $p_{t&x})"
unfolding set_integrable_def using integrable.simps by auto
moreover have le_n: "set_integrable lborel {0..n} (λt. $p_{t&x})"
unfolding survive_def by (intro ccdfTx_integrable_Icc) simp
ultimately have "set_integrable lborel ({0..n} ∪ {n<..}) (λt. $p_{t&x})"
using set_integrable_Un by force
hence "set_integrable lborel {0..} (λt. $p_{t&x})" by force
thus ?thesis
apply (rewrite e_LBINT_p, simp)
apply (rewrite set_integral_Un[of "{0..n}" "{n<..}", simplified], simp_all add: gt_n le_n)
unfolding set_lebesgue_integral_def using gt_n_0 has_bochner_integral_integral_eq by fastforce
qed
lemma e_integral_p_Icc: "$e`∘_x = integral {0..n} (λt. $p_{t&x})" if "x+n ≥ $ψ" for n::real
using that apply (rewrite e_LBINT_p_Icc, simp_all)
using ccdfTx_integrable_Icc unfolding survive_def
by (rewrite set_borel_integral_eq_integral; simp)
lemma temp_e_le_n: "$e`∘_{x:n} ≤ n" if "n ≥ 0" for n::real
proof -
have nni_n: "(∫⇧+_. ennreal n ∂(𝔐 ⇂ alive x)) = ennreal n"
by (rewrite nn_integral_const, rewrite alivex_PS.emeasure_space_1) simp
hence hbi_n: "has_bochner_integral (𝔐 ⇂ alive x) (λ_. n) n"
by (intro has_bochner_integral_nn_integral; simp add: that)
hence "integrable (𝔐 ⇂ alive x) (λ_. n)" by simp
moreover have "integrable (𝔐 ⇂ alive x) (λξ. min (T x ξ) n)"
proof -
have "(∫⇧+ξ. ennreal (norm (min (T x ξ) n)) ∂(𝔐 ⇂ alive x)) ≤ ∫⇧+_. ennreal n ∂(𝔐 ⇂ alive x)"
apply (rule nn_integral_mono, rule ennreal_leI)
apply (rewrite real_norm_def, rewrite abs_of_nonneg; simp add: that)
by (smt (verit) alivex_Tx_pos)
also have "… < ∞" using nni_n by simp
finally have "(∫⇧+ξ. ennreal (norm (min (T x ξ) n)) ∂(𝔐 ⇂ alive x)) < ∞" .
thus ?thesis by (intro integrableI_bounded; simp)
qed
ultimately have "$e`∘_{x:n} ≤ integral⇧L (𝔐 ⇂ alive x) (λ_. n)"
unfolding temp_life_expect_def by (intro integral_mono; simp)
also have "… = n" using hbi_n has_bochner_integral_iff by blast
finally show ?thesis .
qed
lemma temp_e_P: "$e`∘_{x:n} =
MM_PS.expectation (λξ. indicator (alive x) ξ * min (T x ξ) n) / 𝒫(ξ in 𝔐. T x ξ > 0)"
if "n ≥ 0" for n::real
unfolding temp_life_expect_def
by (rewrite MM_PS.integral_cond_prob_space_nn; simp add: alive_T that)
lemma temp_e_LBINT_p: "$e`∘_{x:n} = (LBINT t:{0..n}. $p_{t&x})" if "n ≥ 0" for n::real
proof -
let ?minTxn = "λξ. min (T x ξ) n"
let ?F = "cdf (distr (𝔐 ⇂ alive x) borel (T x))"
let ?Fn = "cdf (distr (𝔐 ⇂ alive x) borel ?minTxn)"
interpret distrTxn_RD: real_distribution "distr (𝔐 ⇂ alive x) borel ?minTxn" by (simp add: that)
have [simp]: "⋀ξ. ξ ∈ space (𝔐 ⇂ alive x) ⟹ 0 ≤ T x ξ" by (smt (verit) alivex_Tx_pos)
have "(∫⇧+ξ. ennreal (min (T x ξ) n) ∂(𝔐 ⇂ alive x)) = (∫⇧+t∈{0..}. ennreal (1 - ?Fn t) ∂lborel)"
by (rewrite alivex_PS.expectation_nonneg_tail; simp add: that)
also have "… = (∫⇧+t∈{0..}. (ennreal (1 - ?F t) * indicator {..<n} t) ∂lborel)"
apply (rule nn_integral_cong)
by (rewrite alivex_PS.cdf_distr_min; simp add: indicator_mult_ennreal mult.commute)
also have "… = (∫⇧+t∈{0..<n}. ennreal (1 - ?F t) ∂lborel)"
apply (rule nn_integral_cong) using nn_integral_set_ennreal
by (smt (verit, best) Int_def atLeastLessThan_def ennreal_mult_right_cong
indicator_simps mem_Collect_eq mult.commute mult_1)
also have "… = (∫⇧+t∈{0..n}. ennreal (1 - ?F t) ∂lborel)"
proof -
have "sym_diff {0..<n} {0..n} = {n}" using that by force
thus ?thesis by (intro nn_integral_null_delta; force)
qed
also have "… = ennreal (LBINT t:{0..n}. $p_{t&x})"
proof -
have "set_integrable lborel {0..n} (λt. $p_{t&x})"
unfolding survive_def by (intro ccdfTx_integrable_Icc) simp
thus ?thesis
unfolding set_lebesgue_integral_def unfolding set_integrable_def
apply (rewrite nn_integral_eq_integral[THEN sym]; simp)
apply (rule nn_integral_cong, simp)
unfolding survive_def using distrTx_RD.ccdf_cdf distrTx_RD.prob_space nn_integral_set_ennreal
by (simp add: indicator_mult_ennreal mult.commute)
qed
finally have "(∫⇧+ξ. ennreal (min (T x ξ) n) ∂(𝔐 ⇂ alive x)) =
ennreal (LBINT t:{0..n}. $p_{t&x})" .
thus ?thesis
unfolding temp_life_expect_def by (rewrite integral_eq_nn_integral; simp add: that)
qed
lemma temp_e_integral_p: "$e`∘_{x:n} = integral {0..n} (λt. $p_{t&x})" if "n ≥ 0" for n::real
using that apply (rewrite temp_e_LBINT_p, simp_all)
using ccdfTx_integrable_Icc unfolding survive_def
by (rewrite set_borel_integral_eq_integral; simp)
lemma e_eq_temp: "$e`∘_x = $e`∘_{x:n}" if "n ≥ 0" "x+n ≥ $ψ" for n::real
using that e_LBINT_p_Icc temp_e_LBINT_p by simp
lemma curt_e_P: "$e_x =
MM_PS.expectation (λξ. indicator (alive x) ξ * ⌊T x ξ⌋) / 𝒫(ξ in 𝔐. T x ξ > 0)"
unfolding curt_life_expect_def
apply (rewrite MM_PS.integral_cond_prob_space_nn; simp add: alive_T)