Theory Life_Table

theory Life_Table
  imports Survival_Model
begin

section ‹Life Table›

text ‹Define a life table axiomatically.›

locale life_table =
  fixes l :: "real  real" ($l'__› [101] 200)
  assumes l_0_pos: "0 < l 0"
    and l_neg_nil: "x. x  0  l x = l 0"
    and l_PInfty_0: "(l  0) at_top "
    and l_antimono: "antimono l"
    and l_right_continuous: "x. continuous (at_right x) l"
begin

subsection ‹Basic Properties of Life Table›

lemma l_0_neq_0[simp]: "$l_0  0"
  using l_0_pos by simp

lemma l_nonneg[simp]: "$l_x  0" for x::real
  using l_antimono l_PInfty_0 by (rule antimono_at_top_le)

lemma l_bounded[simp]: "$l_x  $l_0" for x::real
  using l_neg_nil l_antimono by (smt (verit) antimonoD)

lemma l_measurable[measurable, simp]: "l  borel_measurable borel"
  by (rule borel_measurable_antimono, rule l_antimono)

lemma l_left_continuous_nonpos: "continuous (at_left x) l" if "x  0" for x::real
proof -
  have "$l_x = $l_0" using l_neg_nil that by blast
  moreover have "continuous (at_left x) (λ_. $l_0)" by simp
  moreover have "eventually (λy. $l_y = $l_0) (at_left x)"
    apply (rule eventually_at_leftI[of "x-1"], simp_all)
    using that l_neg_nil by (smt (verit))
  ultimately show ?thesis by (rewrite continuous_at_within_cong[where g="λ_. $l_0"]; simp)
qed

lemma l_integrable_Icc: "set_integrable lborel {a..b} l" for a b :: real
  unfolding set_integrable_def
  apply (rule integrableI_bounded_set[where A="{a..b}" and B="$l_0"], simp_all)
  using emeasure_compact_finite by auto

corollary l_integrable_on_Icc: "l integrable_on {a..b}" for a b :: real
  using l_integrable_Icc by (rewrite integrable_on_iff_set_integrable_nonneg[THEN sym]; simp)

lemma l_integrable_Icc_shift: "set_integrable lborel {a..b} (λt. $l_(x+t))" for a b x :: real
  using set_integrable_Icc_shift l_integrable_Icc by (metis (full_types) add_diff_cancel_right')

corollary l_integrable_on_Icc_shift: "(λt. $l_(x+t)) integrable_on {a..b}" for x a b :: real
  using l_integrable_Icc_shift by (rewrite integrable_on_iff_set_integrable_nonneg[THEN sym]; simp)

lemma l_normal_antimono: "antimono (λx. $l_x / $l_0)"
  using divide_le_cancel l_0_pos l_antimono unfolding antimono_def by fastforce

lemma compl_l_normal_right_continuous: "continuous (at_right x) (λx. 1 - $l_x / $l_0)" for x::real
    using l_0_pos l_right_continuous by (intro continuous_intros; simp)

lemma compl_l_normal_NInfty_0: "((λx. 1 - $l_x / $l_0)  0) at_bot"
    apply (rewrite tendsto_cong[where g="λ_. 0"], simp_all)
    by (smt (verit) div_self eventually_at_bot_linorder l_0_pos l_neg_nil)

lemma compl_l_normal_PInfty_1: "((λx. 1 - $l_x / $l_0)  1) at_top"
    using l_0_pos l_PInfty_0 by (intro tendsto_eq_intros) simp_all+

lemma compl_l_real_distribution: "real_distribution (interval_measure (λx. 1 - $l_x / $l_0))"
  using l_normal_antimono compl_l_normal_right_continuous
    compl_l_normal_NInfty_0 compl_l_normal_PInfty_1
  by (intro real_distribution_interval_measure; simp add: antimono_def)

definition total :: "real  real" ($T'__› [101] 200) where "$T_x  LBINT y:{x..}. $l_y"
  ― ‹the number of lives older than the ones aged x›
  ― ‹The parameter x› must be nonnegative.›

lemma T_nonneg[simp]: "$T_x  0" for x::real
  unfolding total_def by simp

definition "total_finite  set_integrable lborel {0..} l"

lemma total_finite_iff_set_integrable_Ici:
  "total_finite  set_integrable lborel {x..} l" for x::real
  unfolding total_finite_def using set_integrable_Ici_equiv l_integrable_Icc by blast

lemma total_finite_iff_integrable_on_Ici: "total_finite  l integrable_on {x..}" for x::real
  using total_finite_iff_set_integrable_Ici integrable_on_iff_set_integrable_nonneg l_nonneg
  by (metis atLeast_borel l_measurable measurable_lborel2 sets_lborel)

lemma total_finite_iff_summable: "total_finite  summable (λk. $l_(x+k))" for x::real
  apply (rewrite total_finite_iff_set_integrable_Ici)
  apply (rule set_integrable_iff_summable[of x, simplified], simp_all)
  using l_antimono unfolding antimono_def monotone_on_def by simp

lemma T_tendsto_0: "((λx. $T_x)  0) at_top" if total_finite
proof -
  have "x. x  0  $T_x = $T_0 - (LBINT y:{0..x}. $l_y)"
  proof -
    fix x::real assume asm: "x  0"
    let ?A = "{x..}" and ?B = "{0..x}"
    have "{0..} = ?A  ?B" using asm by auto
    thus "$T_x = $T_0 - (LBINT y:{0..x}. $l_y)"
      unfolding total_def apply (rewrite eq_diff_eq)
      using that total_finite_iff_set_integrable_Ici l_integrable_Icc
      apply (rewrite set_integral_Un_AE[THEN sym], simp_all)
      using AE_lborel_singleton add_0 asm le_add_same_cancel2 le_numeral_extra(3) by force
  qed
  hence "F x in at_top. $T_x = $T_0 - (LBINT y:{0..x}. $l_y)"
    by (rule eventually_at_top_linorderI[of 0])
  moreover have "((λx. LBINT y:{0..x}. $l_y)  $T_0) at_top"
    using that unfolding total_def total_finite_def
    by (intro tendsto_set_lebesgue_integral_at_top; simp)
  ultimately show ?thesis
    apply (rewrite tendsto_cong, simp_all)
    using LIM_zero_iff' by force
qed

definition lives :: "real  real  real" ($L'_{_&_} [0,0] 200)
  where "$L_{n&x}  LBINT y:{x..x+n}. $l_y"
    ― ‹the number of lives between ages x› and x+n›
    ― ‹The parameter x› must be nonnegative.›
    ― ‹The parameter n› is usually nonnegative, but theoretically it can be negative.›

abbreviation lives_1 :: "real  real" ($L'__› [101] 200)
  where "$L_x  $L_{1&x}"

lemma l_has_integral_L: "(l has_integral $L_{n&x}) {x..x+n}" for x n :: real
  unfolding lives_def by (rule has_integral_set_integral_real) (rule l_integrable_Icc)

lemma L_neg_0[simp]: "$L_{n&x} = 0" if "n < 0" for x n :: real
  unfolding lives_def using that by (rewrite to "{}" atLeastatMost_empty; simp)

lemma L_nonneg[simp]: "$L_{n&x}  0" for x n :: real
  unfolding lives_def by simp

lemma L_T: "$L_{n&x} = $T_x - $T_(x+n)" if "total_finite" "n  0" for x n :: real
proof -
  have "{x..x+n}{x+n..} = {x..}" using that by force
  moreover have
    "(LBINT y:{x..x+n}{x+n..}. $l_y) = (LBINT y:{x..x+n}. $l_y) + (LBINT y:{x+n..}. $l_y)"
  proof -
    have "AE y in lborel. ¬ (y  {x..x+n}  y  {x+n..})" by (rule AE_I'[where N="{x+n}"]; force)
    moreover have "set_integrable lborel {x..x+n} l" by (rule l_integrable_Icc)
    moreover have "set_integrable lborel {x+n..} l"
      using that total_finite_iff_set_integrable_Ici by simp
    ultimately show ?thesis by (intro set_integral_Un_AE; simp)
  qed
  ultimately show ?thesis unfolding total_def lives_def by simp
qed

lemma L_sums_T: "(λk. $L_(x+k)) sums $T_x" if total_finite for x::real
proof -
  have "(λk::nat. $T_(x+k))  0"
    using T_tendsto_0
    apply (rule filterlim_compose[where f="λk::nat. x+k" and g=total], simp add: that)
    using filterlim_real_sequentially filterlim_tendsto_add_at_top by blast
  hence "(λk. $T_(x+k) - $T_(x + Suc k)) sums $T_x"
    by (simp) (rule telescope_sums'[of "λk. $T_(x+k)" 0, simplified])
  thus ?thesis using that L_T by (rewrite sums_cong, simp_all) smt
qed

definition death :: "real  real  real" ($d'_{_&_} [0,0] 200)
  where "$d_{t&x}  max 0 ($l_x - $l_(x+t))"
    ― ‹the number of deaths between ages x› and x+t›
    ― ‹The parameter t› is usually nonnegative, but theoretically it can be negative.›

abbreviation death1 :: "real  real" ($d'__› [101] 200)
  where "$d_x  $d_{1&x}"

lemma death_def_nonneg: "$d_{t&x} = $l_x - $l_(x+t)" if "t  0" for t x :: real
  using that l_antimono unfolding death_def antimono_def by simp

lemma d_nonpos_0: "$d_{t&x} = 0" if "t  0" for t x :: real
  using that l_antimono unfolding death_def antimono_def by simp

corollary d_0_0: "$d_{0&x} = 0" for x::real
  using d_nonpos_0 by simp

lemma d_nonneg[simp]: "$d_{t&x}  0" for t x :: real
  unfolding death_def by simp

lemma dx_l: "$d_x = $l_x - $l_(x+1)" for x::real
  using death_def_nonneg by simp

lemma sum_dx_l: "(k<n. $d_(x+k)) = $l_x - $l_(x+n)" for x::real and n::nat
proof (induction n)
  case 0
  thus ?case by simp
next
  case (Suc n)
  thus ?case
    using dx_l
    by (metis Set_Interval.comm_monoid_add_class.sum.lessThan_Suc
        add_diff_cancel_left' diff_diff_eq2 of_nat_Suc)
qed

corollary d_sums_l: "(λk. $d_(x+k)) sums $l_x" for x::real
  unfolding sums_def
  apply (rewrite sum_dx_l)
  apply (rule tendsto_diff[where b=0, simplified], simp)
  using l_PInfty_0 filterlim_compose filterlim_real_sequentially filterlim_tendsto_add_at_top
    tendsto_const by blast

lemma add_d: "$d_{t&x} + $d_{t' & x+t} = $d_{t+t' & x}" if "t  0" "t'  0" for t t' :: real
  using death_def_nonneg that by (smt (verit))

definition die_central :: "real  real  real" ($m'_{_&_} [0,0] 200)
  where "$m_{n&x}  $d_{n&x} / $L_{n&x}"
    ― ‹central death rate›

abbreviation die_central_1 :: "real  real" ($m'__› [101] 200)
  where "$m_x  $m_{1&x}"

subsection ‹Construction of Survival Model from Life Table›

definition life_table_measure :: "real measure" (𝔐)
  where "𝔐  interval_measure (λx. 1 - $l_x / $l_0)"

lemma prob_space_actuary_MM: "prob_space_actuary 𝔐"
  unfolding life_table_measure_def using compl_l_real_distribution real_distribution_def
  by (intro prob_space_actuary.intro) force

definition survival_model_X :: "real  real" (X) where "X  λx. x"

lemma survival_model_MM_X: "survival_model 𝔐 X"
proof -
  let ?F = "λx. 1 - $l_x / $l_0"
  show "survival_model 𝔐 X"
    unfolding life_table_measure_def survival_model_X_def
  proof (rule survival_model.intro)
    show "prob_space_actuary (interval_measure ?F)"
      using prob_space_actuary_MM unfolding life_table_measure_def by simp
    show "survival_model_axioms (interval_measure ?F) (λx. x)"
    proof -
      have [simp]: "{ξ::real. ξ  0} = {..0}" by blast
      have "measure (interval_measure (λx. 1 - $l_x / $l_0)) {..0} = 0"
        using l_normal_antimono compl_l_normal_right_continuous compl_l_normal_NInfty_0
        by (rewrite measure_interval_measure_Iic, simp_all add: antimono_def)
      hence "emeasure (interval_measure (λx. 1 - $l_x / $l_0)) {..0} = ennreal 0"
        apply (rewrite finite_measure.emeasure_eq_measure, simp_all)
        using compl_l_real_distribution prob_space_def real_distribution_def by blast
      thus ?thesis
        apply (intro survival_model_axioms.intro, simp)
        apply (rewrite AE_iff_null, simp)
        by (rewrite not_less) auto
    qed
  qed
qed

end

sublocale life_table  survival_model 𝔐 X
  by (rule survival_model_MM_X)

context life_table
begin

interpretation distrX_RD: real_distribution "distr 𝔐 borel X"
  using MM_PS.real_distribution_distr by simp

subsubsection ‹Relations between Life Table and Survival Function for X›

lemma ccdfX_l_normal: "ccdf (distr 𝔐 borel X) = (λx. $l_x / $l_0)"
proof (rule ext)
  let ?F = "λx. 1 - $l_x / $l_0"
  interpret F_FBM: finite_borel_measure "interval_measure ?F"
    using compl_l_real_distribution real_distribution.finite_borel_measure_M by blast
  show "x. ccdf (distr 𝔐 borel X) x = $l_x / $l_0"
    unfolding ccdf_def life_table_measure_def survival_model_X_def
    apply (rewrite measure_distr, simp_all)
    using l_normal_antimono compl_l_normal_right_continuous
      compl_l_normal_NInfty_0 compl_l_normal_PInfty_1
    by (rewrite F_FBM.measure_interval_measure_Ioi; simp add: antimono_def)
qed

corollary deriv_ccdfX_l: "deriv (ccdf (distr 𝔐 borel X)) x = deriv l x / $l_0"
  if "l differentiable at x" for x::real
  using differentiable_eq_field_differentiable_real that
  by (rewrite ccdfX_l_normal, rewrite deriv_cdivide_right; simp)

notation death_pt ()

lemma l_0_equiv: "$l_x = 0  x  " for x::real
  using ccdfX_l_normal ccdfX_0_equiv by simp

lemma d_old_0: "$d_{t&x} = 0" if "x  " "t  0" for x t :: real
  unfolding death_def using l_0_equiv that by (smt (verit) le_ereal_le)

lemma d_l_equiv: "$d_{t&x} = $l_x  x+t  " if "t  0" for x t :: real
  using death_def_nonneg l_0_equiv that by simp

lemma continuous_ccdfX_l: "continuous F (ccdf (distr 𝔐 borel X))  continuous F l"
  for F :: "real filter"
proof -
  have "continuous F (ccdf (distr 𝔐 borel X))  continuous F (λx. $l_x / $l_0)"
    using ccdfX_l_normal by simp
  also have "  continuous F l" using continuous_cdivide_iff l_0_neq_0 by blast
  finally show ?thesis .
qed

lemma has_real_derivative_ccdfX_l:
  "(ccdf (distr 𝔐 borel X) has_real_derivative D) (at x) 
    (l has_real_derivative $l_0 * D) (at x)"
  for D x :: real
proof -
  have "(ccdf (distr 𝔐 borel X) has_real_derivative D) (at x) 
    ((λx. $l_x / $l_0) has_real_derivative D) (at x)"
    by (rule has_field_derivative_cong_eventually; simp add: ccdfX_l_normal)
  also have "  ((λx. $l_0 * ($l_x / $l_0)) has_real_derivative $l_0 * D) (at x)"
    by (rule DERIV_cmult_iff, simp)
  also have "  (l has_real_derivative $l_0 * D) (at x)" by simp
  finally show ?thesis .
qed

corollary differentiable_ccdfX_l:
  "ccdf (distr 𝔐 borel X) differentiable (at x)  l differentiable (at x)"
  for D x :: real
  using has_real_derivative_ccdfX_l
  by (metis l_0_neq_0 mult.commute nonzero_divide_eq_eq real_differentiable_def)

lemma PX_l_normal: "𝒫(ξ in 𝔐. X ξ > x) = $l_x / $l_0" for x::real
  using MM_PS.ccdf_distr_P ccdfX_l_normal X_RV  by (metis (mono_tags, lifting) Collect_cong)

lemma set_integrable_ccdfX_l:
  "set_integrable lborel A (ccdf (distr 𝔐 borel X))  set_integrable lborel A l"
  if "A  sets lborel" for A :: "real set"
proof -
  have "set_integrable lborel A (ccdf (distr 𝔐 borel X)) 
    set_integrable lborel A (λx. $l_x / $l_0)"
    by (rule set_integrable_cong; simp add: ccdfX_l_normal)
  also have "  set_integrable lborel A l" by simp
  finally show ?thesis .
qed

corollary integrable_ccdfX_l: "integrable lborel (ccdf (distr 𝔐 borel X))  integrable lborel l"
  using set_integrable_ccdfX_l[where A=UNIV] by (simp add: set_integrable_def)

lemma integrable_on_ccdfX_l:
  "ccdf (distr 𝔐 borel X) integrable_on A  l integrable_on A" for A :: "real set"
proof -
  have "ccdf (distr 𝔐 borel X) integrable_on A  (λx. $l_x / $l_0) integrable_on A"
    by (rule integrable_cong) (simp add: ccdfX_l_normal)
  also have "  l integrable_on A"
    using integrable_on_cdivide_iff[of "$l_0" l] by simp
  finally show ?thesis .
qed

subsubsection ‹Relations between Life Table and Cumulative Distributive Function for X›

lemma cdfX_l_normal: "cdf (distr 𝔐 borel X) = (λx. 1 - $l_x / $l_0)" for x::real
  using ccdfX_l_normal distrX_RD.cdf_ccdf distrX_RD.prob_space by presburger

lemma deriv_cdfX_l: "deriv (cdf (distr 𝔐 borel X)) x = - deriv l x / $l_0"
  if "l differentiable at x" for x::real
  using distrX_RD.cdf_ccdf differentiable_eq_field_differentiable_real that differentiable_ccdfX_l
    deriv_diff deriv_ccdfX_l that by simp

lemma continuous_cdfX_l: "continuous F (cdf (distr 𝔐 borel X))  continuous F l"
  for F :: "real filter"
  using distrX_RD.continuous_cdf_ccdf continuous_ccdfX_l by simp

lemma has_real_derivative_cdfX_l:
  "(cdf (distr 𝔐 borel X) has_real_derivative D) (at x) 
    (l has_real_derivative - ($l_0 * D)) (at x)"
  for D x :: real
  using distrX_RD.has_real_derivative_cdf_ccdf has_real_derivative_ccdfX_l by simp

lemma differentiable_cdfX_l:
  "cdf (distr 𝔐 borel X) differentiable (at x)  l differentiable (at x)" for D x :: real
  using differentiable_eq_field_differentiable_real distrX_RD.differentiable_cdf_ccdf
    differentiable_ccdfX_l by simp

lemma PX_compl_l_normal: "𝒫(ξ in 𝔐. X ξ  x) = 1 - $l_x / $l_0" for x::real
  using PX_l_normal by (metis MM_PS.prob_compl X_compl_gt_le X_gt_event)

subsubsection ‹Relations between Life Table and Survival Function for T(x)›

context
  fixes x::real
  assumes x_lt_psi[simp]: "x < "
begin

notation futr_life (T)

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 lx_neq_0[simp]: "$l_x  0"
  using l_0_equiv x_lt_psi linorder_not_less by blast

corollary lx_pos[simp]: "$l_x > 0"
  using lx_neq_0 l_nonneg by (smt (verit))

lemma ccdfTx_l_normal: "ccdf (distr (𝔐  alive x) borel (T x)) t = $l_(x+t) / $l_x"
  if "t  0" for t::real
  using ccdfTx_PX PX_l_normal l_0_neq_0 that by simp

lemma deriv_ccdfTx_l:
  "deriv (ccdf (distr (𝔐  alive x) borel (T x))) t = deriv (λt. $l_(x+t) / $l_x) t"
  if "t > 0" "l differentiable at (x+t)" for t::real
proof -
  have "F s in nhds t. ccdf (distr (𝔐  alive x) borel (T x)) s = $l_(x+s) / $l_x"
    apply (rewrite eventually_nhds_metric)
    using that ccdfTx_l_normal dist_real_def by (intro exI[of _ t]) auto
  thus ?thesis by (rule deriv_cong_ev) simp
qed

lemma continuous_at_within_ccdfTx_l:
  "continuous (at t within {0..}) (ccdf (distr (𝔐  alive x) borel (T x))) 
    continuous (at (x+t) within {x..}) l"
  if "t  0" for t::real
  using continuous_ccdfX_ccdfTx that continuous_ccdfX_l by force

lemma isCont_ccdfTx_l:
  "isCont (ccdf (distr (𝔐  alive x) borel (T x))) t  isCont l (x+t)" if "t > 0" for t::real
  using that continuous_ccdfX_l isCont_ccdfX_ccdfTx by force

lemma has_real_derivative_ccdfTx_l:
  "(ccdf (distr (𝔐  alive x) borel (T x)) has_real_derivative D) (at t) 
    (l has_real_derivative $l_x * D) (at (x+t))"
  if "t > 0" for t D :: real
proof -
  have "(ccdf (distr (𝔐  alive x) borel (T x)) has_real_derivative D) (at t) 
    (ccdf (distr (𝔐  alive x) borel (T x)) has_real_derivative
    ($l_x / $l_0 * D / 𝒫(ξ in 𝔐. X ξ > x))) (at t)"
    using PX_l_normal by force
  also have " = (ccdf (distr 𝔐 borel X) has_real_derivative ($l_x / $l_0 * D)) (at (x+t))"
    using has_real_derivative_ccdfX_ccdfTx that by simp
  also have " = (l has_real_derivative ($l_x * D)) (at (x+t))"
    using has_real_derivative_ccdfX_l by simp
  finally show ?thesis .
qed

lemma differentiable_ccdfTx_l:
  "ccdf (distr (𝔐  alive x) borel (T x)) differentiable at t  l differentiable (at (x+t))"
  if "t > 0" for t::real
  using differentiable_ccdfX_ccdfTx differentiable_ccdfX_l that by force

lemma PTx_l_normal: "𝒫(ξ in 𝔐. T x ξ > t ¦ T x ξ > 0) = $l_(x+t) / $l_x" if "t  0" for t::real
  using ccdfTx_l_normal that by (simp add: ccdfTx_cond_prob)

subsubsection ‹Relations between Life Table and Cumulative Distributive Function for T(x)›

lemma cdfTx_compl_l_normal: "cdf (distr (𝔐  alive x) borel (T x)) t = 1 - $l_(x+t) / $l_x"
  if "t  0" for t::real
  using distrTx_RD.cdf_ccdf ccdfTx_l_normal that distrTx_RD.prob_space by auto

lemma deriv_cdfTx_l:
  "deriv (cdf (distr (𝔐  alive x) borel (T x))) t = - deriv (λt. $l_(x+t) / $l_x) t"
  if "t > 0" "l differentiable at (x+t)" for t::real
  using deriv_ccdfTx_l differentiable_cdfX_cdfTx differentiable_cdfX_l distrTx_RD.deriv_cdf_ccdf
    that by fastforce

lemma continuous_at_within_cdfTx_l:
  "continuous (at t within {0..}) (cdf (distr (𝔐  alive x) borel (T x))) 
    continuous (at (x+t) within {x..}) l"
  if "t  0" for t::real
  using that continuous_cdfX_l continuous_cdfX_cdfTx by force

lemma isCont_cdfTx_l:
  "isCont (cdf (distr (𝔐  alive x) borel (T x))) t  isCont l (x+t)" if "t > 0" for t::real
  using that continuous_cdfX_l isCont_cdfX_cdfTx by force

lemma has_real_derivative_cdfTx_l:
  "(cdf (distr (𝔐  alive x) borel (T x)) has_real_derivative D) (at t) 
    (l has_real_derivative - $l_x * D) (at (x+t))"
  if "t > 0" for t D :: real
  using has_real_derivative_ccdfTx_l that distrTx_RD.has_real_derivative_cdf_ccdf by auto

lemma differentiable_cdfTx_l:
  "cdf (distr (𝔐  alive x) borel (T x)) differentiable at t  l differentiable (at (x+t))"
  if "t > 0" for t::real
  using differentiable_cdfX_l that differentiable_cdfX_cdfTx by auto

lemma PTx_compl_l_normal: "𝒫(ξ in 𝔐. T x ξ  t ¦ T x ξ > 0) = 1- $l_(x+t) / $l_x"
  if "t  0" for t::real
  using cdfTx_compl_l_normal that by (simp add: cdfTx_cond_prob)

subsubsection ‹Life Table and Actuarial Notations›

notation survive ($p'_{_&_} [0,0] 200)
notation survive_1 ($p'__› [101] 200)
notation die ($q'_{_&_} [0,0] 200)
notation die_1 ($q'__› [101] 200)
notation die_defer ($q'_{_¦_&_} [0,0,0] 200)
notation die_defer_1 ($q'_{_¦&_} [0,0] 200)
notation life_expect ($e`∘'__› [101] 200)
notation temp_life_expect ($e`∘'_{_:_} [0,0] 200)
notation curt_life_expect ($e'__› [101] 200)
notation temp_curt_life_expect ($e'_{_:_} [0,0] 200)

lemma p_l: "$p_{t&x} = $l_(x+t) / $l_x" if "t  0" for t::real
  unfolding survive_def using ccdfTx_l_normal that by simp

corollary p_1_l: "$p_x = $l_(x+1) / $l_x"
  using p_l by simp

lemma isCont_p_l: "isCont (λs. $p_{s&x}) t  isCont l (x+t)" if "t > 0" for t::real
proof -
  have "F s in nhds t. $p_{s&x} = $l_(x+s) / $l_x"
    apply (rewrite eventually_nhds_metric)
    apply (rule exI[of _ t], auto simp add: that)
    by (rewrite p_l; simp add: dist_real_def)
  hence "isCont (λs. $p_{s&x}) t  isCont (λs. $l_(x+s) / $l_x) t" by (rule isCont_cong)
  also have "  isCont (λs. $l_(x+s)) t" using continuous_cdivide_iff lx_neq_0 by metis
  also have "  isCont l (x+t)" using isCont_shift by (force simp add: add.commute)
  finally show ?thesis .
qed

lemma total_finite_iff_p_set_integrable_Ici:
  "total_finite  set_integrable lborel {0..} (λt. $p_{t&x})"
  apply (rewrite set_integrable_cong_AE[where g="λt. $l_(x+t) / $l_x"]; simp)
  using survive_def apply simp
  using p_l apply (intro AE_I2, simp)
  by (metis l_integrable_Icc_shift set_integrable_Ici_equiv set_integrable_Ici_shift
      total_finite_iff_set_integrable_Ici)

lemma p_PTx_ge_l_isCont: "$p_{t&x} = 𝒫(ξ in 𝔐. T x ξ  t ¦ T x ξ > 0)"
  if "isCont l (x+t)" "t > 0" for t::real
  using p_PTx_ge_ccdf_isCont that continuous_ccdfX_l by force

lemma q_defer_l: "$q_{f¦t&x} = ($l_(x+f) - $l_(x+f+t)) / $l_x" if "f  0" "t  0" for f t :: real
  apply (rewrite q_defer_p, simp_all add: that)
  using that by (rewrite p_l, simp)+ (smt (verit) diff_divide_distrib)

corollary q_defer_d_l: "$q_{f¦t&x} = $d_{t & x+f} / $l_x" if "f  0" "t  0" for f t :: real
  using q_defer_l that death_def_nonneg by simp

corollary q_defer_1_d_l: "$q_{f¦&x} = $d_(x+f) / $l_x" if "f  0" for f::real
  using q_defer_d_l that by simp

lemma q_d_l: "$q_{t&x} = $d_{t&x} / $l_x" for t::real
proof (cases t  0)
  case True
  thus ?thesis using q_defer_d_l[of 0] by simp
next
  case False
  thus ?thesis using q_nonpos_0 d_nonpos_0 by simp
qed

corollary q_1_d_l: "$q_x = $d_x / $l_x"
  using q_d_l by simp

lemma LBINT_p_l: "(LBINT t:A. $p_{t&x}) = (LBINT t:A. $l_(x+t)) / $l_x"
  if "A  {0..}" "A  sets lborel" for A :: "real set"
  ― ‹Note that 0 = 0› holds when the integral diverges.›
proof -
  have [simp]: "t. t  A  $p_{t&x} = $l_(x+t) / $l_x" using p_l that by blast
  hence "(LBINT t:A. $p_{t&x}) = (LBINT t:A. $l_(x+t) / $l_x)"
    using that by (rewrite set_lebesgue_integral_cong[where g="λt. $l_(x+t) / $l_x"]; simp)
  also have " = (LBINT t:A. $l_(x+t)) / $l_x" by (rewrite set_integral_divide_zero) simp
  finally show ?thesis .
qed

corollary e_LBINT_l: "$e`∘_x = (LBINT t:{0..}. $l_(x+t)) / $l_x"
  ― ‹Note that 0 = 0› holds when the integral diverges.›
  by (simp add: e_LBINT_p LBINT_p_l)

corollary e_LBINT_l_Icc: "$e`∘_x = (LBINT t:{0..n}. $l_(x+t)) / $l_x" if "x+n  " for n::real
  using e_LBINT_p_Icc by (rewrite LBINT_p_l[THEN sym]; simp add: that)

lemma temp_e_LBINT_l: "$e`∘_{x:n} = (LBINT t:{0..n}. $l_(x+t)) / $l_x" if "n  0" for n::real
  using temp_e_LBINT_p by (rewrite LBINT_p_l[THEN sym]; simp add: that)

lemma integral_p_l: "integral A (λt. $p_{t&x}) = (integral A (λt. $l_(x+t))) / $l_x"
  if "A  {0..}" "A  sets lborel" for A :: "real set"
  ― ‹Note that 0 = 0› holds when the integral diverges.›
  using that apply (rewrite set_borel_integral_eq_integral_nonneg[THEN sym], simp_all)
  apply (simp add: survive_def)
  apply (rewrite set_borel_integral_eq_integral_nonneg[THEN sym], simp_all)
  by (rule LBINT_p_l; simp)

corollary e_integral_l: "$e`∘_x = integral {0..} (λt. $l_(x+t)) / $l_x"
  ― ‹Note that 0 = 0› holds when the integral diverges.›
  by (simp add: e_integral_p integral_p_l)

corollary e_integral_l_Icc:
  "$e`∘_x = integral {0..n} (λt. $l_(x+t)) / $l_x" if "x+n  " for n::real
  using e_integral_p_Icc by (rewrite integral_p_l[THEN sym]; simp add: that)

lemma e_pos_total_finite: "$e`∘_x > 0" if total_finite
  using e_pos total_finite_iff_p_set_integrable_Ici that by simp

lemma temp_e_integral_l:
  "$e`∘_{x:n} = integral {0..n} (λt. $l_(x+t)) / $l_x" if "n  0" for n::real
  using temp_e_integral_p by (rewrite integral_p_l[THEN sym]; simp add: that)

lemma curt_e_sum_l: "$e_x = (k. $l_(x+k+1)) / $l_x" if total_finite "k::nat. isCont l (x+k+1)"
proof -
  have "summable (λk. $l_(x+(k+1::nat)))"
    using that total_finite_iff_summable by (rewrite summable_iff_shift[of "λk. $l_(x+k)" 1]) simp
  moreover hence "summable (λk. $p_{k+1&x})" by (rewrite p_l, simp_all add: add.commute)
  moreover have "k::nat. isCont (λt. $p_{t&x}) (k+1)"
    using isCont_p_l that by (simp add: add.assoc)
  ultimately show ?thesis
    apply (rewrite curt_e_sum_p, simp_all)
    apply (rewrite p_l, simp)
    by (rewrite suminf_divide) (simp add: add.commute, simp add: add.assoc)
qed

lemma curt_e_sum_l_finite: "$e_x = (k<n. $l_(x+k+1)) / $l_x"
  if "k::nat. k < n  isCont l (x+k+1)" "x+n+1 > " for n::nat
  apply (rewrite curt_e_sum_p_finite[of x n], simp_all add: that)
  using isCont_p_l that apply (simp add: add.assoc)
  apply (rewrite sum_divide_distrib, rule sum.cong, simp)
  using p_l by (smt (verit) of_nat_0_le_iff)

lemma temp_curt_e_sum_p: "$e_{x:n} = (k<n. $l_(x+k+1)) / $l_x"
  if "k::nat. k < n  isCont l (x+k+1)" for n::nat
  apply (rewrite temp_curt_e_sum_p[of x n], simp_all add: that)
  using isCont_p_l that apply (simp add: add.assoc)
  apply (rewrite sum_divide_distrib, rule sum.cong, simp)
  using p_l by (smt (verit) of_nat_0_le_iff)

lemma e_T_l: "$e`∘_x = $T_x / $l_x"
  unfolding total_def
  apply (rewrite e_LBINT_l, simp_all)
  by (metis add_cancel_left_left diff_add_cancel lborel_set_integral_Ici_shift)

lemma temp_e_L_l: "$e`∘_{x:n} = $L_{n&x} / $l_x" if "n  0" for n::real
  unfolding lives_def using that
  apply (rewrite temp_e_LBINT_l, simp_all)
  using diff_self add_diff_cancel_left' lborel_set_integral_Icc_shift by metis

lemma m_q_e: "$m_{n&x} = $q_{n&x} / $e`∘_{x:n}" if "n  0" for n::real
proof -
  have "$m_{n&x} = ($d_{n&x} / $l_x) / ($L_{n&x} / $l_x)" unfolding die_central_def by simp
  thus ?thesis using q_d_l temp_e_L_l that by simp
qed

end

lemma l_p: "$l_x / $l_0 = $p_{x&0}" for x::real
  using ccdfX_l_normal ccdfX_p by force

lemma e_p_e_total_finite: "$e`∘_x = $e`∘_{x:n} + $p_{n&x} * $e`∘_(x+n)"
  if total_finite "n  0" "x+n < " for x n :: real
  using e_p_e that total_finite_iff_p_set_integrable_Ici by (smt (verit) ereal_less_le)

proposition x_ex_const_equiv_total_finite: "x + $e`∘_x = y + $e`∘_y  $q_{y-x&x} = 0"
  if total_finite "x  y" "y < " for x y :: real
  using x_ex_const_equiv that total_finite_iff_p_set_integrable_Ici p_set_integrable_shift
  by blast

corollary x_ex_const_iff_l_const: "x + $e`∘_x = y + $e`∘_y  $l_x = $l_y"
  if total_finite "x  y" "y < " for x y :: real
  using x_ex_const_equiv_total_finite that
  by (smt (verit, ccfv_threshold) divide_cancel_right ereal_less_le
      l_0_equiv life_table.death_def_nonneg life_table.q_d_l life_table_axioms q_1_equiv)

end

subsection ‹Piecewise Differentiable Life Table›

locale smooth_life_table = life_table +
  assumes l_piecewise_differentiable[simp]: "l piecewise_differentiable_on UNIV"
begin

lemma smooth_survival_function_MM_X: "smooth_survival_function 𝔐 X"
proof (rule smooth_survival_function.intro)
  show "survival_model 𝔐 X" by (rule survival_model_axioms)
  show "smooth_survival_function_axioms 𝔐 X"
  proof
    show "ccdf (distr 𝔐 borel X) piecewise_differentiable_on UNIV"
      apply (rewrite ccdfX_l_normal)
      apply (rewrite divide_inverse, rewrite mult.commute)
      using l_piecewise_differentiable piecewise_differentiable_scaleR[of l] by simp
  qed
qed

end

sublocale smooth_life_table  smooth_survival_function 𝔐 X
  by (rule smooth_survival_function_MM_X)

context smooth_life_table
begin

notation force_mortal ($μ'__› [101] 200)

lemma l_continuous[simp]: "continuous_on UNIV l"
  using l_piecewise_differentiable piecewise_differentiable_on_imp_continuous_on by fastforce

lemma l_nondifferentiable_finite_set[simp]: "finite {x. ¬ l differentiable at x}"
  using differentiable_ccdfX_l ccdfX_nondifferentiable_finite_set by simp

lemma l_differentiable_borel_set[measurable, simp]: "{x. l differentiable at x}  sets borel"
  using differentiable_ccdfX_l ccdfX_differentiable_borel_set by simp

lemma l_differentiable_AE: "AE x in lborel. l differentiable at x"
  using differentiable_ccdfX_l ccdfX_differentiable_AE by simp

lemma deriv_l_measurable[measurable]: "deriv l  borel_measurable borel"
proof -
  let ?S = "{x. ¬ l differentiable at x}"
  have "x. x  ?S  $l_0 * deriv (ccdf (distr 𝔐 borel X)) x = deriv l x"
    using deriv_ccdfX_l by simp
  thus ?thesis
    apply -
    by (rule measurable_discrete_difference
        [where X="?S" and f="λx. $l_0 * deriv (ccdf (distr 𝔐 borel X)) x"])
      (simp_all add: countable_finite)
qed

lemma pdfX_l_normal:
  "pdfX x = (if l differentiable at x then - deriv l x / $l_0 else 0)" for x::real
  unfolding pdfX_def
  using differentiable_eq_field_differentiable_real differentiable_cdfX_l deriv_cdfX_l by simp

lemma mu_deriv_l: "$μ_x = - deriv l x / $l_x" if "l differentiable at x" for x::real
  using mu_pdfX that ccdfX_l_normal that pdfX_l_normal by (simp add: differentiable_cdfX_l)

lemma mu_nonneg_differentiable_l: "$μ_x  0" if "l differentiable at x" for x::real
  using differentiable_cdfX_l mu_nonneg_differentiable that by simp

lemma mu_deriv_ln_l:
  "$μ_x = - deriv (λx. ln ($l_x)) x" if "l differentiable at x" "x < " for x::real
proof -
  have "F x in nhds x. ln ($l_x / $l_0) = ln ($l_x) - ln ($l_0)"
  proof (cases  < )
    case True
    thus ?thesis
      apply (rewrite eventually_nhds_metric)
      apply (intro exI[of _ "real_of_ereal  - x"], auto)
      using that True not_inftyI apply fastforce
      apply (rewrite ln_div, simp_all)
      using lx_pos dist_real_def not_inftyI that(2) by fastforce
  next
    case False
    hence "x. $l_x > 0" using l_0_equiv by force
    thus ?thesis
      by (simp add: ln_divide_pos)
  qed
  hence "deriv (λx. ln ($l_x / $l_0)) x = deriv (λx. ln ($l_x)) x"
    apply (rewrite deriv_cong_ev[of _ "λx. ln ($l_x) - ln ($l_0)"], simp_all)
    apply (rewrite deriv_diff, simp_all)
    unfolding field_differentiable_def using that
    by (metis DERIV_ln_divide_chain lx_pos real_differentiable_def)
  thus ?thesis using ccdfX_l_normal mu_deriv_ln that differentiable_ccdfX_l by force
qed

lemma deriv_l_shift: "deriv l (x+t) = deriv (λt. $l_(x+t)) t"
  if "l differentiable at (x+t)" for x t :: real
  using deriv_shift differentiable_eq_field_differentiable_real that by simp

context
  fixes x::real
  assumes x_lt_psi[simp]: "x < "
begin

lemma p_mu_l: "$p_{t&x} * $μ_(x+t) = - deriv l (x+t) / $l_x"
  if "l differentiable at (x+t)" "t > 0" "x+t < " for t::real
  using p_l mu_deriv_l that by simp

lemma p_mu_l_AE: "AE s in lborel. 0 < s  x+s <   $p_{s&x} * $μ_(x+s) = - deriv l (x+s) / $l_x"
proof  -
  have "AE s in lborel. l differentiable at (x+s)"
    apply (rule AE_borel_affine[of 1 "λu. l differentiable at u" x, simplified])
    unfolding pred_def using l_differentiable_AE by simp_all
  moreover have "AE s in lborel.
    l differentiable at (x+s)  0 < s  x+s <   $p_{s&x} * $μ_(x+s) = - deriv l (x+s) / $l_x"
    using p_mu_l by (intro AE_I2) simp
  ultimately show ?thesis by (rule AE_mp)
qed

lemma LBINT_l_mu_q: "(LBINT s:{f<..f+t}. $l_(x+s) * $μ_(x+s)) / $l_x = $q_{f¦t&x}"
  if "t  0" "f  0" for t f :: real
proof -
  have "s. s{f<..f+t}  $p_{s&x} = $l_(x+s) / $l_x" using p_l that by simp
  hence "$q_{f¦t&x} = (LBINT s:{f<..f+t}. $l_(x+s) / $l_x * $μ_(x+s))"
    using LBINT_p_mu_q_defer 
    by (smt (verit) greaterThanAtMost_borel set_lebesgue_integral_cong sets_lborel that x_lt_psi)
  also have " = (LBINT s:{f<..f+t}. $l_(x+s) * $μ_(x+s)) / $l_x"
    using set_integral_divide_zero by simp
  finally show ?thesis by simp
qed

lemma set_integrable_l_mu: "set_integrable lborel {f<..f+t} (λs. $l_(x+s) * $μ_(x+s))"
  if "t  0" "f  0" for t f :: real
proof -
  have "set_integrable lborel {f<..f+t} (λs. $l_(x+s) * $μ_(x+s) / $l_x)"
    using p_l set_integrable_p_mu that
    by (rewrite set_integrable_cong[where f'="λs. $p_{s&x} * $μ_(x+s)"]) simp_all+
  thus ?thesis by simp
qed

lemma l_mu_has_integral_q_defer:
  "((λs. $l_(x+s) * $μ_(x+s) / $l_x) has_integral $q_{f¦t&x}) {f..f+t}"
  if "t  0" "f  0" for t f :: real
  using p_l that p_mu_has_integral_q_defer_Icc
  by (rewrite has_integral_cong[of _ _ "λs. $p_{s&x} * $μ_(x+s)"]; simp)

corollary l_mu_has_integral_q:
  "((λs. $l_(x+s) * $μ_(x+s) / $l_x) has_integral $q_{t&x}) {0..t}" if "t  0" for t::real
  using l_mu_has_integral_q_defer[where f=0] that by simp

lemma l_mu_has_integral_d:
  "((λs. $l_(x+s) * $μ_(x+s)) has_integral $d_{t & x+f}) {f..f+t}"
  if "t  0" "f  0" for t f :: real
proof -
  have "((λs. $l_x * ($p_{s&x} * $μ_(x+s))) has_integral $l_x * $q_{f¦t&x}) {f..f+t}"
    apply (rule has_integral_mult_right)
    by (rule p_mu_has_integral_q_defer_Icc; simp add: that)
  thus ?thesis
    using that apply (rewrite in asm q_defer_d_l, simp_all)
    apply (rewrite has_integral_cong[where g="λs. $l_x * ($p_{s&x} * $μ_(x + s))"])
    by (rewrite p_l; simp)
qed

corollary l_mu_has_integral_d_1:
  "((λs. $l_(x+s) * $μ_(x+s)) has_integral $d_(x+f)) {f..f+1}" if "t  0" "f  0" for t f :: real
  using l_mu_has_integral_d[where t=1] that by simp

lemma e_LBINT_l: "$e`∘_x = (LBINT s:{0..}. $l_(x+s) * $μ_(x+s) * s) / $l_x"
  ― ‹Note that 0 = 0› holds when the life expectation diverges.›
proof -
  have "s. s{0..}  $p_{s&x} = $l_(x+s) / $l_x" using p_l by simp
  hence "$e`∘_x = (LBINT s:{0..}. $l_(x+s) / $l_x * $μ_(x+s) * s)"
    using e_LBINT_p_mu
    by (smt (verit) atLeast_borel set_lebesgue_integral_cong sets_lborel x_lt_psi)
  also have " = (LBINT s:{0..}. $l_(x+s) * $μ_(x+s) * s) / $l_x"
    using set_integral_divide_zero by simp
  finally show ?thesis .
qed

lemma e_integral_l: "$e`∘_x = integral {0..} (λs. $l_(x+s) * $μ_(x+s) * s) / $l_x"
  ― ‹Note that 0 = 0› holds when the life expectation diverges.›
proof -
  have "AE s in lborel. $μ_(x+s)  0" by (rule AE_translation, rule mu_nonneg_AE)
  hence "(LBINT s:{0..}. $l_(x+s) * $μ_(x+s) * s) = integral {0..} (λs. $l_(x+s) * $μ_(x+s) * s)"
    by (intro set_borel_integral_eq_integral_nonneg_AE; force)
  thus ?thesis using e_LBINT_l by simp
qed

lemma m_LBINT_p_mu: "$m_{n&x} = (LBINT t:{0<..n}. $p_{t&x} * $μ_(x+t)) / (LBINT t:{0..n}. $p_{t&x})"
  if "n  0" for n::real
  using that
  apply (rewrite m_q_e, simp_all)
  apply (rewrite LBINT_p_mu_q[simplified], simp_all)
  by (rewrite temp_e_LBINT_p; simp)

lemma m_integral_p_mu:
  "$m_{n&x} = integral {0..n} (λt. $p_{t&x} * $μ_(x+t)) / integral {0..n} (λt. $p_{t&x})"
  if "n  0" for n::real
  using that
  apply (rewrite m_q_e, simp_all)
  apply (rewrite integral_unique[OF p_mu_has_integral_q_Icc])
    apply simp_all[2]
  by (rewrite temp_e_integral_p; simp)

end

lemma deriv_x_p_mu_l: "deriv (λy. $p_{t&y}) x = $p_{t&x} * ($μ_x - $μ_(x+t))"
  if "l differentiable at x" "l differentiable at (x+t)" "t  0" "x < " for x t :: real
  using deriv_x_p_mu that differentiable_ccdfX_l by blast

lemma e_has_derivative_mu_e_l: "((λx. $e`∘_x) has_real_derivative ($μ_x * $e`∘_x - 1)) (at x)"
  if total_finite "l differentiable at x" "x{a<..<b}" "b  " for a b x :: real
  using total_finite_iff_set_integrable_Ici that
    e_has_derivative_mu_e differentiable_ccdfX_l set_integrable_ccdfX_l
  by force

corollary e_has_derivative_mu_e_l': "((λx. $e`∘_x) has_real_derivative ($μ_x * $e`∘_x - 1)) (at x)"
  if total_finite "l differentiable at x" "x{a<..<b}" "b  " for a b x :: real
  using that by (intro e_has_derivative_mu_e_l[where a=a]; simp)

context
  fixes x::real
  assumes x_lt_psi[simp]: "x < "
begin

lemma curt_e_sum_l_smooth: "$e_x = (k. $l_(x+k+1)) / $l_x" if total_finite
proof -
  have [simp]: "summable (λk. $l_(x+k+1))"
    using total_finite_iff_summable[of "x+1"] that
    by (metis (no_types, lifting) add.commute add.left_commute summable_def sums_cong)
  hence "summable (λk. $p_{k+1&x})" by (rewrite p_l; simp add: add.assoc)
  hence "$e_x = (k. $p_{k+1&x})" using curt_e_sum_p_smooth by simp
  also have " = (k. $l_(x+k+1) / $l_x)" by (rewrite p_l; simp add: add.assoc)
  also have " = (k. $l_(x+k+1)) / $l_x" by (rewrite suminf_divide; simp)
  finally show ?thesis .
qed

lemma curt_e_sum_l_finite_smooth: "$e_x = (k<n. $l_(x+k+1)) / $l_x" if "x+n+1 > " for n::nat
  apply (rewrite curt_e_sum_p_finite_smooth[of x n], simp_all add: that)
  apply (rewrite p_l, simp_all)
  by (smt (verit) sum.cong sum_divide_distrib)

lemma temp_curt_e_sum_l_smooth: "$e_{x:n} = (k<n. $l_(x+k+1)) / $l_x" for n::nat
  apply (rewrite temp_curt_e_sum_p_smooth[of x n], simp)
  apply (rewrite p_l, simp_all)
  by (smt (verit) sum.cong sum_divide_distrib)

end

end

subsection ‹Interpolations›

context life_table
begin

definition "linear_interpolation 
  (x::nat)(t::real). 0  t  t  1  $l_(x+t) = (1-t)*$l_x + t*$l_(x+1)"

lemma linear_l: "$l_(x+t) = (1-t)*$l_x + t*$l_(x+1)"
  if linear_interpolation "0  t" "t  1" for x::nat and t::real
  using that unfolding linear_interpolation_def by (metis of_nat_1 of_nat_add)

lemma linear_l_d: "$l_(x+t) = $l_x - t*$d_x"
  if linear_interpolation "0  t" "t  1" for x::nat and t::real
  using death_def_nonneg that unfolding linear_interpolation_def
  by (smt (verit) distrib_left left_diff_distrib')

lemma linear_p_q: "$p_{t&x} = 1 - t*$q_x"
  if linear_interpolation "0  t" "t  1" "x < " for x::nat and t::real
  using that
  apply (rewrite p_l, simp_all)
  apply (rewrite q_d_l, simp_all)
  using divide_self[of "$l_(real x)"] linear_l_d
  by (smt (verit, ccfv_SIG) add_divide_distrib lx_neq_0)

lemma linear_q: "$q_{t&x} = t*$q_x"
  if linear_interpolation "0  t" "t  1" "x < " for x::nat and t::real
  using that linear_p_q p_q_1 by (smt (verit))

lemma linear_L_l_d: "$L_x = $l_x - $d_x / 2" if linear_interpolation for x::nat
proof -
  have "$L_(real x) = (LBINT t:{0..1}. $l_(real x + t))"
    unfolding lives_def using lborel_set_integral_Icc_shift[of "real x" "real x + 1" l "real x"]
    by (simp add: add.commute)
  also have " = (LBINT t:{0..1}. $l_(real x) - t*$d_(real x))"
    using linear_l_d that by (intro set_lebesgue_integral_cong; simp)
  also have " = $l_(real x) - $d_(real x) / 2"
  proof -
    have "(LBINT t:{0::real..1}. t) = 1/2"
      unfolding set_lebesgue_integral_def using integral_power[of 0 1 1] by (simp add: mult.commute)
    hence "(LBINT t:{0..1}. t*$d_(real x)) = $d_(real x) / 2" by auto
    moreover have "set_integrable lborel {0..1} (λt. t*$d_(real x))"
      apply (rule set_integrable_mult_left[where f=id and a="$d_(real x)", simplified])
      unfolding set_integrable_def using integrable_power[of 0 1 1] by (simp add: mult.commute)
    moreover have "(LBINT t:{0::real..1}. $l_(real x)) = $l_(real x)"
      unfolding set_lebesgue_integral_def by simp
    ultimately show ?thesis using set_integrable_def by (rewrite set_integral_diff; force)
  qed
  finally show ?thesis .
qed

lemma linear_L_l_d' : "$L_x = $l_(x+1) + $d_x / 2" if linear_interpolation for x::nat
proof -
  have "$L_(real x) = $l_(real x) - $d_(real x) + $d_(real x) / 2" using that linear_L_l_d by simp
  also have " = $l_(real (x+1)) + $d_(real x) / 2" using dx_l by (smt (verit) of_nat_1 of_nat_add)
  finally show ?thesis .
qed

lemma linear_l_continuous: "continuous_on UNIV l" if linear_interpolation
  unfolding continuous_on_def
proof
  fix u::real
  show "l u $l_u"
  proof (cases u  0)
    case True
    hence "(l  $l_u) (at_left u)" using l_left_continuous_nonpos continuous_within by auto
    thus ?thesis
      apply (rule filterlim_split_at_real)
      using l_right_continuous continuous_within by auto
  next
    case False
    hence u_pos: "u > 0" by simp
    thus ?thesis
    proof (cases u = real_of_int u)
      case True
      from this u_pos obtain x::nat where ux: "u = Suc x"
        by (metis gr0_implies_Suc of_int_0_less_iff of_int_of_nat_eq pos_int_cases)
      have "((λt. (1-t)*$l_(real x) + t*$l_(real x + 1))  $l_(real x + 1)) (at_left 1)"
        apply (rewrite in "(_  ) _" add_0[THEN sym], rule tendsto_add)
         apply (simp add: LIM_zero_iff' tendsto_mult_left_zero)
        by (rewrite in "(_  ) _" mult_1[THEN sym], rule tendsto_mult_right) simp
      hence "((λt. $l_(real x + t))  $l_(real x + 1)) (at_left 1)"
        apply (rewrite tendsto_cong; simp)
        apply (rule eventually_at_leftI[of 0]; simp)
        using that by (rewrite linear_l; simp add: add.commute)
      moreover have "((λt. $l_(real x + t))  $l_(real x + 1)) (at_right 1)"
        using l_right_continuous apply (rule continuous_within_tendsto_compose, simp_all)
         apply (rule eventually_at_right_less)
        by (rule tendsto_intros, simp_all)
      ultimately show ?thesis
        apply (rewrite ux)+
        apply (rewrite filterlim_shift_iff[where d=x, THEN sym])
        by (rule filterlim_split_at_real; simp add: comp_def add.commute)
    next
      case False
      let ?x = "nat u"
      let ?t = "u - real ?x"
      let ?e = "min ?t (1 - ?t)"
      from False have "?t > 0" using u_pos by linarith
      moreover have "?t < 1" by linarith
      ultimately have e_pos: "?e > 0" by simp
      hence
        "F v in nhds u. $l_v = (1 - (v - real ?x))*$l_(real ?x) + (v - real ?x)*$l_(real ?x + 1)"
      proof -
        { fix v::real assume vu_e: "dist v u < ?e"
          hence "v - real ?x  0" using dist_real_def by force
          moreover have "v - real ?x  1" using dist_real_def vu_e by force
          ultimately have "$l_v = (1 - (v - real ?x))*$l_(real ?x) + (v - real ?x)*$l_(real ?x + 1)"
            using linear_l that by (smt (verit, ccfv_threshold) linear_interpolation_def) }
        thus ?thesis using eventually_nhds_metric e_pos by blast
      qed
      moreover have
        "isCont (λv. (1 - (v - real ?x))*$l_(real ?x) + (v - real ?x)*$l_(real ?x + 1)) u"
        by (rule continuous_intros)+
      ultimately have "isCont l u" using isCont_cong by force
      thus ?thesis by (simp add: isContD)
    qed
  qed
qed

lemma linear_l_sums_T_l: "(λk. $l_(x + Suc k)) sums ($T_x - $l_x / 2)"
  if linear_interpolation total_finite for x::nat
proof -
  have "k::nat. $l_(real (x + Suc k)) = $L_(real (x+k)) - $d_(real (x+k)) / 2"
    using linear_L_l_d' that by (smt (verit) Suc_eq_plus1 add_Suc_right)
  moreover have "(λk::nat. $L_(real (x+k))) sums $T_x" using L_sums_T that by simp
  moreover have "(λk::nat. $d_(real (x+k)) / 2) sums ($l_(real x) / 2)"
    using sums_divide d_sums_l by auto
  ultimately show ?thesis
    apply (rewrite sums_cong, simp)
    by (rule sums_diff; simp)
qed

corollary linear_T_suminf_l: "$T_x = (k. $l_(x+k+1)) + $l_x / 2"
  if linear_interpolation total_finite for x::nat
  using linear_l_sums_T_l that sums_unique by (smt (z3) Suc_eq_plus1 add_Suc_right suminf_cong)

lemma linear_mx_q: "$m_x = $q_x / (1 - $q_x / 2)" if linear_interpolation "x < " for x::nat
proof -
  have [simp]: "$l_(real x)  0" using that by simp
  have "$m_(real x) = $d_(real x) / ($l_(real x) - $d_(real x) / 2)"
    unfolding die_central_def using linear_L_l_d that by simp
  also have " = ($d_(real x) / $l_(real x)) / (($l_(real x) - $d_(real x) / 2) / $l_(real x))"
    by simp
  also have " = ($d_(real x) / $l_(real x)) / (1 - ($d_(real x) / $l_(real x)) / 2)"
    by (rewrite diff_divide_distrib) simp
  also have " = $q_(real x) / (1 - $q_(real x) / 2)" using that q_d_l by simp
  finally show ?thesis .
qed

lemma linear_e_curt_e: "$e`∘_x = $e_x + 1/2" 
  if linear_interpolation total_finite "x < " for x::nat
proof -
  have "$e`∘_(real x) = ((k::nat. $l_(real (x+k+1))) + $l_(real x) / 2) / $l_(real x)"
    using e_T_l linear_T_suminf_l that by simp
  also have " = (k::nat. $l_(real (x+k+1))) / $l_(real x) + ($l_(real x) / 2) / $l_(real x)"
    using add_divide_distrib by blast
  also have " = $e_(real x) + 1/2"
    using that apply (rewrite curt_e_sum_l, simp_all)
    using linear_l_continuous by (rule continuous_on_interior, simp_all add: that add.commute)
  finally show ?thesis .
qed

end

context smooth_life_table
begin

lemma linear_l_has_derivative_at_frac:
  "((λs. $l_(x+s)) has_real_derivative - $d_x) (at t)"
  if linear_interpolation "0 < t" "t < 1" for x::nat and t::real
proof -
  let ?x = "real x"
  have "((λs. $l_?x - s*$d_?x) has_real_derivative (0 - $d_?x)) (at t)"
    apply (rule derivative_intros, simp)
    apply (rule DERIV_cmult_right[of id 1, simplified])
    by (metis DERIV_ident eq_id_iff)
  moreover have "F s in nhds t. $l_(?x + s) = $l_?x - s*$d_?x"
  proof -
    let ?r = "min t (1-t)"
    have "?r > 0" using that by simp
    moreover
    { fix s assume "dist s t < ?r"
      hence "$l_(?x + s) = $l_?x - s*$d_?x" using linear_l_d that dist_real_def by force }
    ultimately show ?thesis using eventually_nhds_metric that by blast
  qed
  ultimately show ?thesis by (rewrite DERIV_cong_ev; simp)
qed

lemma linear_l_has_derivative_at_frac':
  "(l has_real_derivative - $d_x) (at y)"
  if linear_interpolation "x < y" "y < x+1" for x::nat and y::real
  apply (rewrite DERIV_at_within_shift[where x="y - real x" and z="real x" and S=UNIV, simplified])
  using linear_l_has_derivative_at_frac that by simp

lemma linear_l_differentiable_on_frac:
  "l differentiable_on {x<..<x+1}" if linear_interpolation for x::nat
proof -
  { fix y::real assume "y  {real x <..< real (x+1)}"
    hence "l differentiable at y"
      using linear_l_has_derivative_at_frac' that real_differentiable_def by auto }
  thus ?thesis unfolding differentiable_on_def by (metis differentiable_at_withinI)
qed

lemma linear_l_has_right_derivative_at_nat:
  "(l has_real_derivative - $d_x) (at_right x)" if linear_interpolation for x::nat
proof -
  let ?x = "real x"
  have [simp]: "plus ?x ` {0<..} = {?x<..}"
    unfolding image_def greaterThan_def apply simp
    by (metis Groups.ab_semigroup_add_class.add.commute
        add_minus_cancel neg_less_iff_less real_0_less_add_iff)
  have "((λs. $l_(?x + s)) has_real_derivative - $d_?x) (at_right 0)"
    apply (rewrite has_field_derivative_cong_eventually[where g="λs. $l_?x - s*$d_?x"])
    using linear_l_d that apply (intro eventually_at_rightI[of 0 1], simp_all)
    apply (rule has_field_derivative_at_within)
    apply (rewrite diff_0[of "$d_?x", THEN sym])
    apply (rule DERIV_diff, simp)
    apply (rule DERIV_cmult_right[of id 1, simplified])
    by (metis DERIV_ident eq_id_iff)
  thus ?thesis
    by (rewrite DERIV_at_within_shift[where z="?x" and x=0 and S="{0<..}", simplified]) simp
qed

lemma linear_l_has_left_derivative_at_nat:
  "(l has_real_derivative - $d_(real x - 1)) (at_left x)" if linear_interpolation for x::nat
proof (cases x)
  case 0
  hence "(l has_real_derivative 0) (at_left (real x))"
    apply (rewrite has_field_derivative_cong_eventually[where g="λ_. $l_0"]; simp)
    apply (rule eventually_at_leftI[of "-1"]; simp)
    using l_neg_nil less_eq_real_def by blast
  moreover have "$d_(real x - 1) = 0" using 0 dx_l l_neg_nil less_eq_real_def by fastforce
  ultimately show ?thesis by auto
next
  case (Suc y)
  let ?x = "real x" and ?y = "real y"
  have [simp]: "?y + 1 = ?x" using Suc by simp
  have [simp]: "plus ?y ` {..<1} = {..<?x}"
    using Suc unfolding image_d