Explicit ruin candidate and exact renewal valuation: erRenewalIntegral_at_zero
ProvedActuarialValuation.erRenewalIntegral_at_zeroactuarial-sciencecompound-poisson-ruin-renewalformal-verification
No positive claim can be integrated below capital zero. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.
Mathematical relation:
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Analysis.SpecialFunctions.ExpDeriv import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic import Definitions.Def_actuarial_erRenewalIntegral
Formal statement
namespace ActuarialValuation theorem erRenewalIntegral_at_zero (lambda c beta : ℝ) : erRenewalIntegral lambda c beta 0=0 := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 438. S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23, sections 23.3–23.7; Hanspeter Schmidli, Risk Theory (2017), Springer Actuarial, https://link.springer.com/book/10.1007/978-3-319-72005-0; Palmowski et al. 2020, https://doi.org/10.1007/s13385-020-00223-4. Parent topic: Compound Poisson surplus with exponentially distributed claims, net profit, adjustment root, exact candidate ruin function and renewal differential/integral 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.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.