Exposure-scaled credibility error is nonnegative
ProvedActuarialValuation.credibilityScaledMSE_nonnegactuarial-scienceaggregate-claimsformal-verification
The scaled prediction loss is a sum of nonnegative variance coefficients times squared deviations of the credibility weight. For nonnegative exposure and variance parameters, the prediction-error objective cannot be negative for any real weight.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_credibilityScaledMSE
Formal statement
namespace ActuarialValuation theorem credibilityScaledMSE_nonneg (p epv vhm z : ℝ) (hp : 0 ≤ p) (he : 0 ≤ epv) (hv : 0 ≤ vhm) : 0 ≤ credibilityScaledMSE p epv vhm z := by sorry end ActuarialValuation
Source
S David Promislow (2015), Fundamentals of Actuarial Mathematics (3rd ed), sections 24.5.2-24.5.3 equations (24.13)-(24.16), library PDF pages 489-491; weighted Buehlmann-Straub model and least-squares premium; https://openacttexts.github.io/LDAVer2/ChapCredibility.html
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. The real-valued scaled risk is the sum of two squared quantities multiplied by nonnegative coefficients: exposure times VHM and EPV. Squares are nonnegative for any real candidate weight. The total criterion is therefore nonnegative without having to assume the candidate z lies in the unit interval.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.