Stop-loss risk comparison and limitations of floored risk principles: crStopLoss_nonnegative
ProvedActuarialValuation.crStopLoss_nonnegativeactuarial-sciencecoherent-risk-measure-stop-lossformal-verification
Expected stop-loss excess is nonnegative under a valid finite probability law.
Mathematical relation:
Original derived theorem target; the Lean statement gives the exact conditions and result.
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Data.Fintype.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Definitions.Def_actuarial_crStopLoss
Formal statement
namespace ActuarialValuation
theorem crStopLoss_nonnegative {n : ℕ} (p X : Fin n→ℝ) (d : ℝ) (hp : ∀ i,0≤p i) : 0≤crStopLoss p X d := by sorry
end ActuarialValuationSource
Original derived actuarial mathematics inspired by Promislow (2015), chapters 22, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://doi.org/10.1111/1467-9965.00068. The proposed model is rooted in Promislow chapter 22. The target Lean identity is an original derivation, not a verbatim published result. Published source page 412 gives the actuarial risk assessment chapter context; the Lean statement is an original derived target.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.