Class relativities and aggregate technical premium: ratWeightedExposure_zero
ProvedActuarialValuation.ratWeightedExposure_zeroactuarial-scienceexposure-weighted-ratemakingformal-verification
Zero classes produce no relativity-weighted exposure. 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_ratWeightedExposure
Formal statement
namespace ActuarialValuation theorem ratWeightedExposure_zero (e r : ℕ → ℝ) : ratWeightedExposure e r 0 = 0 := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 1. Actuarial Standards Board, ASOP 53 Estimating Future Costs for Prospective Property/Casualty Risk Transfer and Risk Retention (2017), Section 3.7, https://www.actuarialstandardsboard.org/asops/estimating-future-costs-prospective-propertycasualty-risk-transfer-risk-retention/; Casualty Actuarial Society, Basic Ratemaking presentation (2012), https://www.airc.org.tw/newsfiles/BasicRatemakingI.pdf. Parent topic: General insurance loss-cost pricing, exposure-weighted class relativities and exact pure premium calibration. 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.actuarialstandardsboard.org/asops/estimating-future-costs-prospective-propertycasualty-risk-transfer-risk-retention/
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.