Stop-loss reinsurance, retained deficit and pathwise capital: ruStopLoss_nonneg
ProvedActuarialValuation.ruStopLoss_nonnegactuarial-scienceformal-verificationruin-deficit-process
The ceded stop-loss layer is a nonnegative insurance payment. 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_ruStopLoss
Formal statement
namespace ActuarialValuation theorem ruStopLoss_nonneg (x d : ℝ) : 0 ≤ ruStopLoss x d := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 433. S. David Promislow, Fundamentals of Actuarial Mathematics, third edition (2015), Chapter 23, https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml; Palmowski, Ramsden and Papaioannou (2018), Parisian ruin for the dual risk process in discrete-time, https://link.springer.com/article/10.1007/s13385-018-0172-8. Parent topic: Actuarial surplus and ruin: first-passage event, claim timing, nonnegative deficit, retained loss and reinsurance comparison for finite portfolios. 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.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.