diff --git a/metadata/entries/Actuarial_Mathematics.toml b/metadata/entries/Actuarial_Mathematics.toml --- a/metadata/entries/Actuarial_Mathematics.toml +++ b/metadata/entries/Actuarial_Mathematics.toml @@ -1,66 +1,51 @@ title = "Actuarial Mathematics" date = 2024-04-07 topics = [ "Mathematics/Games and economics", ] abstract = """ Actuarial Mathematics is a theory in applied mathematics. This is mainly used for determining the prices of insurance products and evaluating the liability of a company associating with insurance contracts. It is related to calculus, probability theory and financial theory, etc. In this entry, I formalize the very basic part of Actuarial Mathematics in Isabelle/HOL. It includes the theory of interest, survival model, and life table. The theory of interest deals with interest rates, present value factors, an annuity certain, etc. The survival model is a probabilistic model that represents the human mortality. The life table is based on the survival model and used for practical calculations. I have already formalized the basic part of Actuarial Mathematics in Coq (https://github.com/Yosuke-Ito-345/Actuary) in a purely axiomatic manner. In contrast, Isabelle formalization is based on the probability theory and the survival model is developed as generally as possible. Such rigorous and general formulation seems very rare; at least I cannot find any similar documentation on the web. This formalization in Isabelle is still at an early stage, and I cannot guarantee the backward compatibility in the future development. If you heavily depend on this entry, please let me know. (Updated April 7th, 2024.) """ license = "bsd" note = "" [authors] [authors.ito] email = "ito_email" [contributors] [notify] ito = "ito_email" [history] -2024-04-07 = { - "Newly Added Lemmas" = "Added some lemmas with fractional age assumptions on life tables." - "Incompatible Changes" = { - Interest = "Deleted the actuarial notations in the global scope." - Survival_Model = { - "Renamed \" lemma LBINT_p_mu_q \" to \" lemma LBINT_p_mu_q_defer \", and added new \" corollary LBINT_p_mu_q \" .", - "Adopted the word \" limited \" instead of \" finite \" to indicate that \" death_pt \" is not infinite." - } - Life_Table = { - "Modified the definition of \" death \" .", - "Dropped the hypothesis in the corollary \" e_integral_l \" .", - "Changed the hypothesis of integrability to \" total_finite \" in the lemmas \" e_has_derivative_mu_e_l \", \" e_has_derivative_mu_e_l' \" .", - "Changed the hypotheses of summability to \" total_finite \" in the lemmas \" curt_e_sum_l \", \" curt_e_sum_l_smooth \" .", - "Changed the term \" measurize \" to \" measurable_extension \" .", - "Adopted the word \" limited \" instead of \" finite \" to indicate the life table that takes the value zero at a certain age." - } - } -} +2024-04-07 = """ +Added some lemmas with fractional age assumptions on life tables. +""" 2023-07-08 = """ Added the theories Survival_Model, Life_Table and Examples. Updated the theories Preliminaries and Interest. """ 2022-01-23 = """ Submitted the theories Preliminaries and Interest. """ [extra] [related]