Email Gateway (Sep 13 2023 at 12:36): Email Gateway (Sep 13 2023 at 12:36):From: 伊藤洋介 <glacier345@gmail.com>
Dear Isabelle users,
This is an announcement of the update of the AFP entry
"Actuarial_Mathematics" with the release of Isabelle2023.
https://www.isa-afp.org/entries/Actuarial_Mathematics.html
The newly added theories are:
1. "Survival_Model"
the probabilistic model of human mortality,
2. "Life_Table"
the table format of the survival model which is used for practical
calculation of the probability of death, expected future lifetime, etc,
3. "Examples"
some applications of the above theories.
During the formalization of actuarial mathematics, I added many lemmas
mainly on "HOL-Analysis" and "HOL-Probability" such as
1. the interchange of differentiation and Lebesgue integration,
2. the tail expectation formula,
3. the conditional probability space,
4. the complementary cumulative distribution function,
5. the hazard rate.
I formalized these lemmas in a general and reusable manner, so they may be
useful to anyone who formalizes theories on analysis.
I also suggest that these lemmas should be included in the standard library.
Best regards,
Last updated: Jan 04 2025 at 20:18 UTC