Prior expected ultimate and Bornhuetter-Ferguson reconciliation: clBFReserve_zero_expectation
ProvedActuarialValuation.clBFReserve_zero_expectationactuarial-scienceclaims-development-reservingformal-verification
No prior expected ultimate means no additional expected future claims. 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_clBFReserve
Formal statement
namespace ActuarialValuation theorem clBFReserve_zero_expectation (f : ℝ) : clBFReserve 0 f = 0 := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 283. Klaus D. Schmidt, Methods and Models of Loss Reserving Based on Run-Off Triangles, Casualty Actuarial Society Forum (2006), https://www.casact.org/sites/default/files/database/forum_06fforum_273.pdf; Casualty Actuarial Society, The Bornhuetter-Ferguson Principle (2008), https://www.casact.org/sites/default/files/2021-07/Bornhuetter-Ferguson-Schmidt-Zocher.pdf. Parent topic: Finite cumulative claim triangles, volume-weighted age-to-age factors, development-to-ultimate and Bornhuetter-Ferguson reserve valuation. 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.casact.org/sites/default/files/database/forum_06fforum_273.pdf
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.