Observed risk sets and interval exits: kmDeathHazard_le_one
ProvedActuarialValuation.kmDeathHazard_le_oneactuarial-scienceformal-verificationsurvival-product-limit
Death counts cannot exceed people at risk at a valid observed event time. The full Lean declaration specifies the finite boundaries, exact units and any positivity, independence or regularity assumptions. This is an original derived Actuarial mathematical statement, not a claim of a numbered previously published theorem.
Mathematical relation:
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Definitions.Def_actuarial_kmDeathHazard
Formal statement
namespace ActuarialValuation theorem kmDeathHazard_le_one (d r : ℝ) (hd : d ≤ r) (hr : 0 < r) : kmDeathHazard d r ≤ 1 := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 267. Society of Actuaries, Mortality Differences by Handedness, Transactions of the Society of Actuaries 45 (1993), p. 267, https://www.soa.org/globalassets/assets/library/research/transactions-of-society-of-actuaries/1990-95/1993/january/tsa93v459.pdf; Kaplan and Meier, Nonparametric Estimation from Incomplete Observations (1958), Journal of the American Statistical Association 53, pp. 457-481. Parent topic: At-risk exposure and deaths with administrative censoring, product-limit survival estimator and Greenwood variance correction. 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.soa.org/globalassets/assets/library/research/transactions-of-society-of-actuaries/1990-95/1993/january/tsa93v459.pdf
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.