Prove2Me

Conservative multi-state intensity matrices and forward Euler transition: ctRateOut_nonneg

Proved
ActuarialValuation.ctRateOut_nonneg

by WillR · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-sciencectmc-generator-thieleformal-verification

Nonnegative off-diagonal exit intensities imply a nonnegative total exit rate. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.

Mathematical relation:

Nonnegative off-diagonal exit intensities imply a nonnegativetotal exit rate.\begin{aligned}\text{Nonnegative off-diagonal exit intensities imply a nonnegative} \\ \text{total exit rate.}\end{aligned}
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Definitions.Def_actuarial_ctRateOut
Formal statement
namespace ActuarialValuation

theorem ctRateOut_nonneg (r : Fin 3 → Fin 3 → ℝ) (i : Fin 3) (hr : ∀ j, 0 ≤ r i j) : 0 ≤ ctRateOut r i := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 324. Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 19, sections 19.3–19.6, https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml; Norberg and colleagues, Markov models and Thiele's integral equations for the prospective reserve (1997), https://doi.org/10.1016/S0167-6687(97)00020-6; Buchardt, Møller and Schmidt (2015), https://doi.org/10.1080/03461238.2013.879919. Parent topic: Finite actuarial multi-state generator conservation, continuous-time mortality transition matrices, and an analytically derived absorbing-state prospective reserve equation. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://www.sciencedirect.com/science/article/pii/S0167668797000206
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph