Embedded Poisson-arrival capital paths and first-passage partition: srNetLoss_zero
ProvedActuarialValuation.srNetLoss_zeroactuarial-scienceformal-verificationstochastic-ruin-firstpassage
Net claims start at zero. 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_srNetLoss
Formal statement
namespace ActuarialValuation
theorem srNetLoss_zero {Ω : Type*} (c : ℝ) (W Y : ℕ → Ω → ℝ) (ω : Ω) : srNetLoss c W Y 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.