Theory Examples

theory Examples
  imports Life_Table
begin

section ‹Examples›

text ‹
  The following lemma is a verification of the solution to the multiple choice question No.\ 3
  of Exam LTAM Spring 2022 by Society of Actuaries.
›

context smooth_survival_function
begin

lemma SoA_LTAM_2022_Spring_MCQ_No3:
  assumes "x::real. 0  x  x  100  ccdf (distr 𝔐 borel X) x = (1 - 0.01*x).^0.5"
  shows "¦1000*$μ_25 - 6.7¦ < 0.05"
proof -
  let ?svl = "ccdf (distr 𝔐 borel X)"
  have [simp]: "ereal 25 < "
    apply (rewrite not_le[THEN sym])
    using assms by (rewrite ccdfX_0_equiv[THEN sym]) simp
  have : "((λx. ln (1 - x/100)) has_real_derivative (-1/75)) (at 25)"
  proof -
    have "((λx. (1 - x/100)) has_real_derivative (0 - 1/100)) (at 25)"
      apply (intro derivative_intros)
      by (rule DERIV_cdivide) simp
    hence "((λx. ln (1 - x/100)) has_real_derivative (1 / (1 - 25/100) * (-1/100))) (at 25)"
      by (intro derivative_intros) auto
    thus ?thesis by simp
  qed
  have "exp  (λx::real. 0.5 * ln (1 - 0.01*x)) field_differentiable at 25"
    apply (rule field_differentiable_compose, simp_all)
     apply (rule derivative_intros, simp_all)
    using  field_differentiable_def apply blast
    using field_differentiable_within_exp by blast
  hence "?svl differentiable at 25"
    apply (rewrite differentiable_eq_field_differentiable_real)
    by (rule field_differentiable_transform_within[where d=1])
      (simp_all add: powr_def dist_real_def assms)
  hence "$μ_25 = - deriv (λx. ln (?svl x)) 25" by (rule mu_deriv_ln; simp)
  also have " = 0.005 / (1 - 0.01*25)"
  proof -
    have "F x in nhds 25. ln (?svl x) * 2 = ln (1 - x/100)"
    proof -
      { fix x::real assume "dist x 25 < 1"
        hence asm: "0 < x" "x < 100" using dist_real_def by auto
        hence "ln (?svl x) * 2 = ln ((1 - 0.01*x).^0.5) * 2" using assms by (smt (verit))
        also have " = (0.5 * ln (1 - 0.01*x)) * 2" using asm by (rewrite ln_powr) auto
        finally have "ln (?svl x) * 2 = ln (1 - x/100)" by simp }
      thus ?thesis by (rewrite eventually_nhds_metric) (smt (verit, del_insts))
    qed
    hence "((λx. ln (?svl x)) has_real_derivative (-0.005 / (1 - 0.01*25))) (at 25)"
      using  apply (rewrite DERIV_cong_ev[where g="λx. 0.5 * ln (1 - 0.01*x)"], simp_all)
      by (rule derivative_eq_intros) auto
    thus ?thesis using DERIV_imp_deriv by force
  qed
  finally show ?thesis by simp
qed

end

text ‹
  The following lemma is a verification of the solution to the problem No.\ 2.\ (1)-1
  of Life Insurance Mathematics 2016 by the Institute of Actuaries of Japan,
  slightly modified; see the remark below.
›

context smooth_life_table
begin

lemma IAJ_Life_Insurance_Math_2016_2_1_1:
  fixes a b :: real
  assumes "-1 < a" "a < 0" "0 < b" "-b/a  " and
    total_finite and
    "x. 0 < x  x < -b/a  l differentiable at x" and
    "x. 0  x  x < -b/a  $e`∘_x = a*x + b"
  shows "x. 0  x  x < -b/a  $l_x = $l_0 * (b / (a*x + b)).^((a+1)/a)"
proof -
  fix x assume asm_x: "0  x" "x < -b/a"
  hence x_lt_psi[simp]: "ereal x < " using assms ereal_le_less by presburger
  from asm_x have axb_pos[simp]: "a*x + b > 0"
    using assms by (smt (verit, ccfv_threshold) mult.commute neg_less_divide_eq)
  have mu: "t. t{0<..<-b/a}  $μ_t = (a + 1) / (a*t + b)"
  proof -
    fix t assume asm_t: "t{0<..<-b/a}"
    with assms have "((λu. $e`∘_u) has_real_derivative ($μ_t * $e`∘_t - 1)) (at t)"
      by (intro e_has_derivative_mu_e_l'[where a=0]; simp)
    moreover have "((λu. $e`∘_u) has_real_derivative a) (at t)"
    proof -
      let ?d = "min t (-b/a - t)"
      have "?d > 0" using assms asm_t by simp
      moreover have "u. dist u t < ?d  $e`∘_u = a*u + b" using assms dist_real_def by auto
      ultimately have "F u in nhds t. $e`∘_u = a*u + b" by (rewrite eventually_nhds_metric) blast
      thus ?thesis 
        using assms apply (rewrite DERIV_cong_ev[where g="λt. a*t + b"], simp_all)
        by (intro derivative_eq_intros) auto
    qed
    ultimately have "$μ_t * $e`∘_t - 1 = a" using DERIV_unique by blast
    moreover have "$e`∘_t = a*t + b" using assms asm_t by simp
    ultimately show "$μ_t = (a + 1) / (a*t + b)"
      using assms by (smt (verit) mult_eq_0_iff nonzero_mult_div_cancel_right)
  qed
  hence "$p_{x&0} = (b / (a*x + b)).^((a+1)/a)"
  proof -
    have integ_mu: "integral {0..x} (λt. $μ_t) = (a + 1) / a * ln ((a*x + b) / b)"
    proof -
      have "integral {0..x} (λt. $μ_t) = integral {0<..x} (λt. $μ_t)"
        apply (rule integral_spike_set)
         apply (rule negligible_subset[where s="{0}"]; force)
        by (rule negligible_subset[where s="{}"]; simp)
      also have " = integral {0<..x} (λt. ((a + 1) / a) * (a / (a*t + b)))"
        using asm_x assms by (intro integral_cong) (rewrite mu; simp)
      also have " = (a + 1) / a * integral {0<..x} (λt. a / (a*t + b))"
        by (metis integral_mult_right)
      also have " = (a + 1) / a * ln ((a*x + b) / b)"
      proof -
        have "integral {0<..x} (λt. a / (a*t + b)) = integral {0..x} (λt. a / (a*t + b))"
          apply (rule integral_spike_set)
           apply (rule negligible_subset[where s="{}"]; simp)
          by (rule negligible_subset[where s="{0}"]; force)
        also have " = ln (a*x + b) - ln (a*0 + b)"
          apply (rule integral_unique)
          using assms asm_x apply (intro inverse_fun_has_integral_ln, simp_all)
          using axb_pos assms apply (smt (verit) mult_less_cancel_left)
          apply (intro continuous_intros)
          by (intro derivative_eq_intros) auto
        also have " = ln ((a*x + b) / b)" using assms by (simp add: ln_divide_pos)
        finally have "integral {0<..x} (λt. a / (a*t + b)) = ln ((a*x + b) / b)" .
        thus ?thesis by simp
      qed
      finally show ?thesis .
    qed
    thus ?thesis
      apply (rewrite p_exp_integral_mu, simp_all add: asm_x)
      unfolding powr_def using assms
      by simp (smt (verit) axb_pos ln_div
          nonzero_minus_divide_divide nonzero_minus_divide_right right_diff_distrib')
  qed
  thus "$l_x = $l_0 * (b / (a*x + b)).^((a+1)/a)"
    using assms asm_x apply (rewrite in asm p_l, simp_all)
    by (metis divide_mult_cancel l_0_neq_0 mult.commute)
qed

text ‹REMARK.
  The original problem lacks the following hypotheses:
    (i) 0 < b›,
    (ii) -b/a ≤ $ψ›,
    (iii) ∀x. 0 < x < -b/a ⟶ l differentiable at x›,
    (iv) ∀x. 0 ≤ x < -b/a ⟶ l integrable_on {x..}›.
  Moreover, the hypothesis ∀x. 0 ≤ x < -b/a› is originally ∀x. 0 ≤ x ≤ -b/a›.
›

end

end