Embedded Poisson-arrival capital paths and first-passage partition: srWaitingTotal_zero
ProvedActuarialValuation.srWaitingTotal_zeroactuarial-scienceformal-verificationstochastic-ruin-firstpassage
Zero claim arrivals have no elapsed waiting time. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.
Mathematical relation:
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Mathlib.MeasureTheory.Measure.Typeclasses.Probability import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.Analysis.SpecialFunctions.ExpDeriv import Definitions.Def_actuarial_srWaitingTotal
Formal statement
namespace ActuarialValuation
theorem srWaitingTotal_zero {Ω : Type*} (W : ℕ → Ω → ℝ) (ω : Ω) : srWaitingTotal W 0 ω=0 := by sorry
end ActuarialValuationSource
Original derived actuarial mathematics, published source page 3. S. David Promislow (2015), Fundamentals of Actuarial Mathematics, chapter 23, https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml; Hanspeter Schmidli, Risk Theory (2017), https://link.springer.com/book/10.1007/978-3-319-72005-0; probability ruin bound overview https://www.mdpi.com/2227-9091/12/2/28. Parent topic: Actual compound-Poisson embedded arrival paths, measurable first ruin events, disjoint first-hit times, deficit and conditional stopped-exponential Lundberg bound. 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.mdpi.com/2227-9091/12/2/28
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.