Extreme Value Theory

Michikazu Hirata 📧

September 11, 2026

Abstract

This entry is a formalization of extreme value theory (EVT). EVT is a branch of probability theory and statistics that studies rare events. We formalize two main results of EVT, mainly following the books by de Haan and Ferreira and by Embrechts et al.
  • The Fisher–Tippett–Gnedenko theorem, stating that if the properly normalized maximum of i.i.d. random variables converges in distribution to a non-degenerate limit, then the limit is an extreme value distribution.
  • The Pickands–Balkema–de Haan theorem, stating that the conditional distribution of the excesses over a threshold \(u\) converges uniformly in the excess, with a suitable scale \(\beta(u)\), to a generalized Pareto distribution as \(u\) tends to the right endpoint of the support, if and only if the underlying distribution belongs to the maximum domain of attraction of an extreme value distribution.

License

BSD License

Note

More than 95% of the Isabelle codes were written by a generative AI.

Topics

Session Extreme_Value_Theory

Depends on

Cite

× 
@article{Extreme_Value_Theory-AFP,
  author  = {Michikazu Hirata},
  title   = {Extreme Value Theory},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Extreme_Value_Theory.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download