Finite scenario probabilities, losses and positive-part payouts: tailExcess_nonneg
ProvedActuarialValuation.tailExcess_nonnegactuarial-scienceformal-verificationtail-risk-cvar
The insured excess-of-loss indemnity is never negative. 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_tailExcess
Formal statement
namespace ActuarialValuation theorem tailExcess_nonneg (x t : ℝ) : 0 ≤ tailExcess x t := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 5. Rockafellar and Uryasev, Optimization of Conditional Value-at-Risk (1999 preprint, later Journal of Risk 2000), equation 4 and Theorem 1, page 5, https://sites.math.washington.edu/~rtr/papers/rtr179-CVaR1.pdf; Rockafellar and Uryasev, Journal of Risk (2000), https://econpapers.repec.org/RePEc:rsk:journ4:2161159. Parent topic: Finite discrete loss distributions, excess-of-loss functionals and Rockafellar-Uryasev conditional value-at-risk auxiliary threshold objective. 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://sites.math.washington.edu/~rtr/papers/rtr179-CVaR1.pdf
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.