Prove2Me

Extreme claim quantiles, threshold stability and expected shortfall: exVariance_nonneg

Proved
ActuarialValuation.exVariance_nonneg

by WillR · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-scienceextreme-severity-gpd-gevformal-verification

Finite-variance GPD parameter regime yields nonnegative claim variance. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

qp=σξ((1−p)−ξ−1),ESp=qp+σ1−ξq_p=\frac{\sigma}{\xi}\left((1-p)^{-\xi}-1\right),\quad \text{ES}_p=\frac{q_p+\sigma}{1-\xi}
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Definitions.Def_actuarial_exVariance
Formal statement
namespace ActuarialValuation

theorem exVariance_nonneg (xi sigma : ℝ) (hxi : xi<1/2) : 0≤exVariance xi sigma := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 3. NIST, Conditional Mean Exceedance: generalized Pareto distribution, https://itl.nist.gov/div898/software/dataplot/refman1/auxillar/cme.htm; NIST, Extreme Value Type I Distribution, https://www.itl.nist.gov/div898/handbook/eda/section3/eda366g.htm; Annual Review of Statistics, Extreme Value Analysis for Financial Risk Management, https://doi.org/10.1146/annurev-statistics-042720-015705. Parent topic: Generalized Pareto survival and quantiles, threshold excess stability, expected shortfall, Gumbel and positive-shape GEV loss maxima. 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://itl.nist.gov/div898/software/dataplot/refman1/auxillar/cme.htm
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph