Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Corollary 7.7Convergence to types with different limits

Let $(A_n)_{n \in \mathbb {N}}$ and $(\widetilde{A}_n)_{n \in \mathbb {N}}$ be two sequences of oriented affine isomorphisms of $\mathbb {R}$, $A_n, \widetilde{A}_n \in \mathrm{Aff}^+_{\mathbb {R}}$. Write $A_n(x) = a_n x + b_n$ and $\widetilde{A}_n(x) = \tilde{a}_n x + \tilde{b}_n$, and for the inverses $A_n^{-1}(x) = c_n x + d_n$ and $\widetilde{A}^{-1}_n(x) = \tilde{c}_n x + \tilde{d}_n$.

Let $(F_n)_{n \in \mathbb {N}}$ be a sequence of c.d.f.s such that $A_n.F_n \overset {\mathrm{d}}{\longrightarrow }G$ and $\widetilde{A}_n.F_n \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}$, with $G$ and $\widetilde{G}$ nondegenerate c.d.f.s. Then for some $\alpha {\gt}0$ and $\beta \in \mathbb {R}$ we have

\begin{align*} \frac{\tilde{a}_n}{a_n} \to \alpha \quad \text{ and } \quad \frac{a_n \tilde{b}_n - \tilde{a}_n b_n}{a_n} \to \beta , \end{align*}

and we have

\begin{align*} A.G = \widetilde{G} \qquad \text{ where } \; A(x) = \alpha x + \beta . \end{align*}

Equivalently, with $\gamma = \alpha ^{-1}$ and $\delta = -\alpha ^{-1} \beta $ so that $A^{-1}(x) = \gamma x + \delta $, we have

\begin{align*} \frac{\tilde{c}_n}{c_n} \to \gamma \quad \text{ and } \quad \frac{\tilde{d}_n - d_n}{c_n} \to \delta . \end{align*}

In particular, $G$ and $\widetilde{G}$ have the same type.

LaTeX

Definition 1.18

We equip the space $\mathrm{Aff}^+_{\mathbb {R}}$ of orientation-preserving affine isomorphisms with the topology of pointwise convergence, i.e., with the coarsest topology which makes the evaluations $A \mapsto A(x)$ continuous for all $x \in \mathbb {R}$.

LaTeX Lean

Definition 1.1

A function $F \colon \mathbb {R}\to \mathbb {R}$ is a cumulative distribution function (c.d.f.) if

$x \mapsto F(x)$ is increasing;
$x \mapsto F(x)$ is right-continuous;
$\lim _{x \to -\infty } F(x) = 0$ and $\lim _{x \to +\infty } F(x) = 1$.

LaTeX Lean

Definition 5.1Extended cumulative distribution function

The extension $\widetilde{F}$ of a c.d.f. $F$ is the function

\begin{align*} \widetilde{F} \colon [-\infty ,+\infty ] \to [0,1] \end{align*}

given by

\begin{align*} \widetilde{F}(x) = \begin{cases} 0 & \; \text{ if } x = -\infty \\ F(x) & \; \text{ if } -\infty {\lt} x {\lt} +\infty \\ 1 & \; \text{ if } x = +\infty . \end{cases}\end{align*}

LaTeX Lean

Definition 7.1Type (of distribution on $\mathbb {R}$)

Two c.d.f.s $F, G$ are said to be of the same type, if there exists an order-preserving affine isomorphism $A \in \mathrm{Aff}^+_{\mathbb {R}}$ such that $G = A . F$.

Being of the same type is an equivalence relation, and the equivalence classes are called types (of distributions on $\mathbb {R}$).

LaTeX

Definition 4.1Weak convergence of probability measures

A sequence $(\mu _n)_{n \in \mathbb {N}}$ of Borel probability measures on $\mathbb {R}$ converges weakly to a Borel probability measure $\mu $ on $\mathbb {R}$ if for all bounded continuous functions $f \colon \mathbb {R}\to [0,+\infty )$ we have

\begin{align*} \lim _{n \to \infty } \int _{\mathbb {R}} f(x) \, \mathrm{d}\mu _n(x) = \int _{\mathbb {R}} f(x) \, \mathrm{d}\mu (x) . \end{align*}

LaTeX

Lean

MeasureTheory.ProbabilityMeasure.instTopologicalSpace
MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto

Definition 1.3

A c.d.f. $F$ is said to be degenerate if for every $x \in \mathbb {R}$ we have either $F(x) = 0$ or $F(x) = 1$. Otherwise $F$ is said to be nondegenerate.

LaTeX Lean

Definition 2.1

A c.d.f. $G$ is said to be an extreme value distribution if $G$ is nondegenerate and there exists a c.d.f. $F$ and a sequence $(A_n)_{n \in \mathbb {N}}$ of orientation preserving affine isomorphisms $A_n \in \mathrm{Aff}^+_{\mathbb {R}}$, such that for every continuity point $x \in \mathbb {R}$ of $G$ we have

\begin{align*} \lim _{n \to \infty } \big( (A_n.F)(x) \big)^n \; = \; G(x) . \end{align*}

LaTeX Lean

Definition 7.12Subgroup fixing a point

The mapping $s \mapsto A_s$ with

\begin{align*} A_s(x) = e^{s} (x - c) + c \end{align*}

is a homomorphism $\mathbb {R}\to \mathrm{Aff}^+_{\mathbb {R}}$. The image of this homomorphism is the subgroup fixing $c$ in $\mathrm{Aff}^+_{\mathbb {R}}$.

LaTeX

Lean

AffineIncrEquiv.homOfIndex
AffineIncrEquiv.subGroupOfIndex

Definition 8.1

Let $f \colon R \to S$ be a function (usually assumed nondecreasing). The left-continuous inverse of $f$ is the function ${f}^{\rightarrow 1} \colon S \to R$ given by

\begin{align*} {f}^{\rightarrow 1}(y) := \inf \big\{ x \in R \; \big| \; f(x) \ge y \big\} \qquad \text{ for } y \in S. \end{align*}

The right-continuous inverse ${f}^{\leftarrow 1} \colon S \to R$ is analoguously defined by

\begin{align*} {f}^{\leftarrow 1}(y) := \sup \big\{ x \in R \; \big| \; f(x) \le y \big\} \qquad \text{ for } y \in S. \end{align*}

LaTeX Lean

Definition 5.5One over negative logarithm cumulative distribution function

The transform $\frac{\mathbf{1}}{\widetilde{\log } \big( 1 / \widetilde{F} \big)}$ of a c.d.f. $F$ is the function

\begin{align*} \frac{\mathbf{1}}{\widetilde{\log } \big( 1 / \widetilde{F} \big)} \colon [-\infty ,+\infty ] \to [0,+\infty ] \end{align*}

given by

\begin{align*} \frac{\mathbf{1}}{\widetilde{\log } \big( 1 / \widetilde{F} \big)}(x) = \begin{cases} 0 & \; \text{ if } \widetilde{F}(x) = 0 \\ \frac{1}{\log \big( 1/\widetilde{F}(x) \big)} & \; \text{ if } 0 {\lt} \widetilde{F}(x) {\lt} 1 \\ +\infty & \; \text{ if } \widetilde{F}(x) = 1 , \end{cases}\end{align*}

where $\widetilde{F} \colon [-\infty ,+\infty ] \to [0,1]$ is the extension of the c.d.f. $F$.

LaTeX Lean

Definition 5.3One over one minus cumulative distribution function

The transform $\frac{\mathbf{1}}{\mathbf{1}-\widetilde{F}}$ of a c.d.f. $F$ is the function

\begin{align*} \frac{\mathbf{1}}{\mathbf{1}-\widetilde{F}} \colon [-\infty ,+\infty ] \to [1,+\infty ] \end{align*}

given by

\begin{align*} \frac{\mathbf{1}}{\mathbf{1}-\widetilde{F}}(x) = \begin{cases} 1 & \; \text{ if } \widetilde{F}(x) = 0 \\ \frac{1}{1-\widetilde{F}(x)} & \; \text{ if } 0 {\lt} \widetilde{F}(x) {\lt} 1 \\ +\infty & \; \text{ if } \widetilde{F}(x) = 1 , \end{cases}\end{align*}

where $\widetilde{F} \colon [-\infty ,+\infty ] \to [0,1]$ is the extension of the c.d.f. $F$.

LaTeX Lean

Definition 1.10

The collection of all transformations $\mathbb {R}\to \mathbb {R}$ of the form $x \mapsto a x + b$, where $a{\gt}0$, $b \in \mathbb {R}$, forms a group. We call this the orientation preserving affine isomorphism group and denote it by $\mathrm{Aff}^+_{\mathbb {R}}$.

LaTeX Lean

Definition 1.11

The action of an orientation preserving affine isomorphism $A \in \mathrm{Aff}^+_{\mathbb {R}}$ on a cumulative distribution function $F$ is defined so that $A.F \colon \mathbb {R}\to \mathbb {R}$ is given by $(A.F)(x) = F(A^{-1}(x))$. Then $A.F$ is also a c.d.f.

LaTeX Lean

Definition 2.5

The standard Fréchet distribution of parameter $\alpha {\gt} 0$ is the c.d.f. $\Phi _{\alpha }$ given by

\begin{align*} \Phi _{\alpha } (x) = \begin{cases} 0 \quad & \text{ for } x \le 0 \\ \exp \big( - x^{-\alpha } \big) \quad & \text{ for } x {\gt} 0 . \end{cases}\end{align*}

(In the parametrization of extreme value distribution types by one index $\gamma \in \mathbb {R}$, this case corresponds to $\gamma {\gt} 0$ via $\gamma = 1/\alpha $.)

LaTeX Lean

Definition 2.3

The standard Gumbel distribution is the c.d.f. $\Lambda $ given by

\begin{align*} \Lambda (x) = \exp \big(-\exp (-x)\big) . \end{align*}

(In the parametrization of extreme value distribution types by one index $\gamma \in \mathbb {R}$, this case corresponds to $\gamma = 0$.)

LaTeX Lean

Definition 2.4

The standard (reverse) Weibull distribution of parameter $\alpha {\gt} 0$ is the c.d.f. $\Psi _{\alpha }$ given by

\begin{align*} \Psi _{\alpha } (x) = \begin{cases} \exp \big( - (-x)^\alpha \big) \quad & \text{ for } x {\lt} 0 \\ 1 \quad & \text{ for } x \ge 0 . \end{cases}\end{align*}

(In the parametrization of extreme value distribution types by one index $\gamma \in \mathbb {R}$, this case corresponds to $\gamma {\lt} 0$ via $\gamma = -1/\alpha $.)

LaTeX Lean

Definition 7.9Subgroup of translations

The mapping $s \mapsto A_s$ with

\begin{align*} A_s(x) = x + s \end{align*}

is a homomorphism $\mathbb {R}\to \mathrm{Aff}^+_{\mathbb {R}}$. The image of this homomorphism is the subgroup of translations in $\mathrm{Aff}^+_{\mathbb {R}}$.

LaTeX

Lean

AffineIncrEquiv.homOfIndex₀
AffineIncrEquiv.subGroupOfIndex₀

Lemma 1.22The action of oriented affine transforms on c.d.f.s is continuous

The action $A . F$ of $A \in \mathrm{Aff}^+_{\mathbb {R}}$ on a c.d.f $F$ depends jointly continuously on $A$ and $F$.

(The topology on c.d.f.s is the topology of convergence in distribution, i.e., convergence at all continuity points of the limit cdf.)

LaTeX Lean

Lemma 1.19The coefficients of affine map depend continuously on the map

The coefficients $a$ and $b$ of an orientation-preserving affine isomorphism $A(x) = a x + b$ depend continuously on $A$.

LaTeX

Lean

AffineIncrEquiv.continuous_coefs_fst
AffineIncrEquiv.continuous_coefs_snd

Lemma 1.21Inversion of orientation preserving affine isomorphisms is continuous

The map $A \mapsto A^{-1}$ is continuous on $\mathrm{Aff}^+_{\mathbb {R}}$. In particular, inversion defines a homeomorphism of $\mathrm{Aff}^+_{\mathbb {R}}$ to itself.

LaTeX

Lean

AffineIncrEquiv.continuous_inv
AffineIncrEquiv.invHomeomorph

Lemma 1.20Metrizability of the topology on oriented affine isomorphisms

The topology of pointwise convergence makes $\mathrm{Aff}^+_{\mathbb {R}}$ homeomorphic to $\mathbb {R}^2$, and in particular metrizable.

LaTeX

Lean

AffineIncrEquiv.homeomorph_prod
AffineIncrEquiv.metrizableSpace

Lemma 6.1Functional equation in one parameter subgroups of affine isomorphisms

Suppose that $t \mapsto A_t$ is a homomorphism of multiplicative groups $(0,+\infty ) \to \mathrm{Aff}^+_{\mathbb {R}}$, i.e., for any $s, t {\gt} 0$ we have

\begin{align*} A_{s t} = A_s \circ A_t . \end{align*}

Write $A_t(x) = a_t x + b_t$, with $a_t {\gt} 0$ and $b_t \in \mathbb {R}$. Then we have, for any $s, t {\gt} 0$,

\begin{align*} a_{t s} = \; & a_t \, a_s \qquad \text{ and } \\ b_{t s} = \; & a_t \, b_s + b_t . \end{align*}

(Also by symmetry $b_{t s} = a_s \, b_t + b_s$.)

LaTeX

Lemma 1.15Continuity points of c.d.f.s are those which carry no point mass

Let $F$ be cumulative distribution function of a probability measure $\mu $ on $\mathbb {R}$. A point $x \in \mathbb {R}$ is a continuity point of $F$ if and only if $\mu [\left\{ x \right\} ] = 0$.

LaTeX Lean

Lemma 1.14

Let $F$ be a cumulative distribution function, and $A \in \mathrm{Aff}^+_{\mathbb {R}}$ an orientation preserving affine isomorphism. If a point $x \in \mathbb {R}$ is a continuity point of $F$, then the point $A(x) \in \mathbb {R}$ is a continuity point of $A.F$.

LaTeX Lean

Lemma 4.9Necessary condition for convergence in distribution with cdfs

Let $\mu $ and $\mu _n$, $n \in \mathbb {N}$, be Borel probability measures on $\mathbb {R}$, and let $F$ and $F_n$, $n \in \mathbb {N}$, be their cumulative distribution functions, respectively, i.e.,

\begin{align*} F(x) = \; & \mu \big[(-\infty ,x]\big] & & \text{for $x \in \mathbb {R}$} \\ F_n(x) = \; & \mu _n \big[(-\infty ,x]\big] & & \text{for $x \in \mathbb {R}$ and $n \in \mathbb {N}$.} \end{align*}

If $\lim _{n \to \infty } \mu _n = \mu $ in the sense of weak convergence of measures, Definition 4.1, then for all continuity points $x$ of $F$ we have $\lim _{n \to \infty } F_n(x) = F(x)$.

LaTeX Lean

Lemma 1.17Equality of c.d.f.s on a dense set suffices

Suppose that $F,G$ are two c.d.f.s and $S \subseteq \mathbb {R}$ is a dense subset of the real line. If $F(\xi ) = G(\xi )$ for all $\xi \in S$, then we have $F = G$.

LaTeX Lean

Lemma 5.2Continuity points of extended c.d.f.

The extension $\widetilde{F}$ of a c.d.f. $F$ is continuous at $x = -\infty $, $x = + \infty $, and at any $x \in (-\infty ,+\infty )$ where $F$ is continuous.

LaTeX

Lean

CumulativeDistributionFunction.extend_continuousAt
CumulativeDistributionFunction.extend_continuousAt_top
CumulativeDistributionFunction.extend_continuousAt_bot

Lemma 1.9

Let $X_0, X_1, \ldots , X_{n-1}$ be independent identically distributed real-valued random variables with cumulative distribution functions $F$, i.e. $F(x) = \mathsf{P}\big[ X_j \le x \big]$ for every $j$, and let $a {\gt} 0$ and $b \in \mathbb {R}$. Then the c.d.f. of

\begin{align*} \hat{M}_n = \frac{\max _{0 \le j {\lt} n} X_j - b}{a} \end{align*}

is the function $x \mapsto \big(F(a x + b)\big)^n$.

LaTeX

Lemma 1.8

\[ M_n = \max _{0 \le j {\lt} n} X_j \]

is the function $x \mapsto \big(F(x)\big)^n$.

LaTeX

Lemma 1.7

Let $X$ and $Y$ be two independent real-valued random variables with respective cumulative distribution functions $F$ and $G$, i.e. $F(x) = \mathsf{P}\big[ X \le x \big]$ and $G(x) = \mathsf{P}\big[ Y \le x \big]$. Then the c.d.f. of $M = \max (X, Y)$ is $x \mapsto F(x) \, G(x)$.

LaTeX

Lemma 1.2

If $X$ is a real-valued random variable, then the function $F \colon \mathbb {R}\to \mathbb {R}$ given by $F(x) = \mathsf{P}\big[ X \le x \big]$ is a c.d.f.

LaTeX Lean

Lemma 4.3Tightness of a cumulative distribution function

Let $F$ be a cumulative distribution function. Then for any $\varepsilon {\gt} 0$ there exists points $a,b \in \mathbb {R}$ with $a {\lt} b$ such that $F(b) - F(a) {\gt} 1 - \varepsilon $ and $F$ is continuous at the points $a$ and $b$.

LaTeX Lean

Lemma 7.19Self-similar continuous c.d.f. family characterization $\gamma {\lt} 0$

Suppose that $G$ is a nondegenerate c.d.f. such that

\begin{align*} G^{t} = A_t . G \qquad \text{ for any } t {\gt} 0 , \end{align*}

where

\begin{align*} A_t(x) = t^{-\alpha } x + c \, (1 - t^{-\alpha }) = t^{-\alpha } (x-c) + c \end{align*}

with $c \in \mathbb {R}$ and $\alpha {\gt} 0$.

Then with $\sigma = \big(- \log G(c-1)\big)^{-\alpha }$, for all $x \le c$ we have

\begin{align*} G(x) = \exp \Big( - \big( \frac{c - x}{\sigma } \big)^{1/\alpha } \big) \Big) . \end{align*}

(It easily follows that $G$ is of Weibull type: there exists an $A \in \mathrm{Aff}^+_{\mathbb {R}}$ such that $G = A.\Psi _{\alpha }$.)

LaTeX

Lean

weibull_type_of_selfSimilar_index_neg'
weibull_type_of_selfSimilar_index_neg

Lemma 7.18Self-similar continuous c.d.f. family characterization $\gamma {\gt} 0$

Suppose that $G$ is a nondegenerate c.d.f. such that

\begin{align*} G^{t} = A_t . G \qquad \text{ for any } t {\gt} 0 , \end{align*}

where

\begin{align*} A_t(x) = t^{\alpha } x + c \, (1 - t^{\alpha }) = t^{\alpha } (x-c) + c \end{align*}

with $c \in \mathbb {R}$ and $\alpha {\gt} 0$.

Then with $\sigma = \big(- \log G(c+1)\big)^{\alpha }$, for all $x \ge c$ we have

\begin{align*} G(x) = \exp \Big( - \big( \frac{x - c}{\sigma } \big)^{-1/\alpha } \big) \Big) . \end{align*}

(It easily follows that $G$ is of Fréchet type: there exists an $A \in \mathrm{Aff}^+_{\mathbb {R}}$ such that $G = A.\Phi _{\alpha }$.)

LaTeX

Lean

frechet_type_of_selfSimilar_index_pos'
frechet_type_of_selfSimilar_index_pos

Lemma 7.17Self-similar continuous c.d.f. family characterization $\gamma = 0$

Suppose that $G$ is a nondegenerate c.d.f. such that

\begin{align*} G^{t} = A_t . G \qquad \text{ for any } t {\gt} 0 , \end{align*}

where

\begin{align*} A_t(x) = x + \beta \, \log t \end{align*}

with $\beta {\gt} 0$.

Then with $d = \log \big(-\log G(0) \big)$, for all $x \in \mathbb {R}$ we have

\begin{align*} G(x) = \exp \Big( - \exp \big( -\beta ^{-1} x + d \big) \Big) . \end{align*}

(In particular, $G$ is of Gumbel type: there exists an $A \in \mathrm{Aff}^+_{\mathbb {R}}$ such that $G = A.\Lambda $.)

LaTeX

Lean

gumbel_type_of_selfSimilar_index_zero'
gumbel_type_of_selfSimilar_index_zero

Lemma 7.14Conjugate of fixing is fixing image

Let $A^{(\alpha ;c)}_s = e^{\alpha s} (x - c) + c$ for $\alpha , c \in \mathbb {R}$ as in Definition 7.12. Let also $B \in \mathrm{Aff}^+_{\mathbb {R}}$ be given by $B(x) = a x + b$. Then

\begin{align*} B \, A^{(\alpha ;c)}_s \, B^{-1} = A^{(\alpha ;B(c))}_{s} . \end{align*}

LaTeX Lean

Lemma 7.11Conjugate of translation is translation

Let $A^{(\beta )}_s = x + \beta s$ for $s, \beta \in \mathbb {R}$ as in Definition 7.9. Let also $B \in \mathrm{Aff}^+_{\mathbb {R}}$ be given by $B(x) = a x + b$. Then

\begin{align*} B \, A^{(\beta )}_s \, B^{-1} = A^{(a \beta )}_{s} . \end{align*}

LaTeX Lean

Lemma 4.5Subdivision for continuous function approximation

Let $D \subset \mathbb {R}$ be a dense set, let $f \colon \mathbb {R}\to \mathbb {R}$ be continuous, let $a, b \in D$ with $a {\lt} b$, and let $\varepsilon {\gt} 0$. Then there exists a $k \in \mathbb {N}$ and points $a=c_0 {\lt} c_1 {\lt} \cdots {\lt} c_{k-1} {\lt} c_k = b$ such that for each $j = 1, \ldots , k$ we have $c_j \in D$ and

\begin{align*} \big| f(x) - f(c_j) \big| {\lt} \varepsilon \qquad \text{ for } \qquad x \in [c_{j-1} , c_j] . \end{align*}

LaTeX Lean

Lemma 7.15Continuous parameter extreme value limit relation

Let $F$ be a c.d.f.

(Note that below we use the sequence $(F^n)_{n \in \mathbb {N}}$ of $n$th powers of a fixed c.d.f., not a sequence of arbitrary c.d.f.s. Recall that the $n$th power $F^n$ is the c.d.f. of the maximum of $n$ independent random variables with the distribution $F$.)

Suppose that for a sequence $(A_n)_{n \in \mathbb {N}}$ of oriented affine isomorphisms of $\mathbb {R}$, $A_n \in \mathrm{Aff}^+_{\mathbb {R}}$, we have

\begin{align*} A_n.F^n \overset {\mathrm{d}}{\longrightarrow }G , \end{align*}

where $G$ is a c.d.f.

Then, for any $t {\gt} 0$, denoting by $G^t$ the c.d.f. given by $G^t(x) = \big( G(x) \big)^t$, we have

\begin{align*} A_{n}.F^{\lfloor n t \rfloor } \overset {\mathrm{d}}{\longrightarrow }G^t , \end{align*}

where, for $x \in \mathbb {R}$, the floor notation $\lfloor x \rfloor $ stands for the greatest integer $k \in \mathbb {Z}$ such that $k \le x$.

LaTeX Lean

Lemma 9.1Countably many connected components for an open set

Let $X$ be a locally connected separable space. Then any open subset $U \subseteq X$ has at most countably many connected components.

LaTeX Lean

Lemma 1.4

$F$ is a degenerate c.d.f. if and only if there exists a $x_0 \in \mathbb {R}$ such that

\begin{align*} F(x) = \begin{cases} 0 & \text{ for } x {\lt} x_0 \\ 1 & \text{ for } x \ge x_0 . \end{cases}\end{align*}

LaTeX Lean

Lemma 1.6

If a c.d.f. $F$ is degenerate, then it is the c.d.f. of a Dirac delta mass $\delta _{x_0}$ at some point $x_0 \in \mathbb {R}$.

LaTeX Lean

Lemma 1.13

Let $F$ be a cumulative distribution function and $A \in \mathrm{Aff}^+_{\mathbb {R}}$ an orientation preserving affine isomorphism. Then $A.F$ is degenerate if and only if $F$ is degenerate.

LaTeX Lean

Lemma 7.3Degeneration by shrinking affine transformations

Let $(F_n)_{n \in \mathbb {N}}$ be a sequence of c.d.f.s which converges to a c.d.f. $G$, $F_n \overset {\mathrm{d}}{\longrightarrow }G$. Consider affine transformations of the form $A_n(x) = a_n x + b_n$, with $a_n {\gt} 0$ and $b_n \in \mathbb {R}$, such that $a_n \to 0$ and $b_n \to \beta \in \mathbb {R}$ as $n \to \infty $. Then $A_n . F_n \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}$, where $\widetilde{G}$ is the degenerate c.d.f. of the delta mass at $\beta $.

LaTeX Lean

Lemma 1.5

The c.d.f. of Dirac delta mass $\delta _{x_0}$ at $x_0 \in \mathbb {R}$ is degenerate.

LaTeX Lean

Lemma 9.5Difference set of positive measure set contains an interval

Let $A \subset \mathbb {R}$ be a measurable set of positive Lebesgue measure. Then there exists a $\delta {\gt} 0$ such that

\begin{align*} (-\delta ,\delta ) \, \subseteq \, A - A . \end{align*}

LaTeX Lean

Lemma 9.7Difference of two positive measure sets contains an interval

Let $A, B \subset \mathbb {R}$ be two measurable sets of positive Lebesgue measure. Then the difference set $A - B$ contains a nontrivial open interval.

LaTeX

Lemma 9.6Dividing a high overlap interval

Let $A$ be a measurable. Suppose that for some $a {\lt} b$, the interval $J = (a,b)$ satisfies $\Lambda [A \cap J] \; {\gt} \; r \, \Lambda [J]$. Let $m \in \mathbb {N}_{+}$, and consider the subintervals

\begin{align*} J_i = \Big( a + \frac{i}{(b-a)m} , \; a + \frac{i+1}{(b-a)m} \Big) \qquad \text{ for $i = 0, \ldots , m-1$.} \end{align*}

Then for some $i$ we have $\Lambda [A \cap J_i] \; {\gt} \; r \, \Lambda [J_i]$.

LaTeX

Lemma 2.10Relation implies $F$ tending to one

Let $F$ and $G$ be c.d.f.s, and $(A_n)_{n \in \mathbb {N}}$ a sequence of orientation preserving affine isomorphisms $A_n \in \mathrm{Aff}^+_{\mathbb {R}}$. Then for any $x \in \mathbb {R}$ such that $0 {\lt} G(x) {\lt} 1$, if

\begin{align*} \text{(i)} & & \lim _{n \to \infty } \big( (A_n.F)(x) \big)^n \, = \; & G(x) \end{align*}

holds, then necessarily

\begin{align*} \lim _{n \to \infty } F (A_n^{-1}(x)) \; = \; 1 . \end{align*}

LaTeX Lean

Lemma 9.2Finding an interval with high overlap

Let $A \subset \mathbb {R}$ be a measurable set such that $0 {\lt} \Lambda [A] {\lt} +\infty $. Then for any $r \in [0,1)$, there exists a nontrivial interval $J \subset \mathbb {R}$ (a subset of the real line which is connected and has nonempty interior) such that

\begin{align*} \Lambda [A \cap J] \; {\gt} \; r \, \Lambda [J] . \end{align*}

LaTeX Lean

Lemma 1.16A pair of nontrivial continuity points of nondegenerate c.d.f.

Let $G$ be a nondegenerate c.d.f. Then there exists continuity points $x_1 {\lt} x_2$ of $G$ such that $0 {\lt} G(x_1) \le G(x_2) {\lt} 1$.

LaTeX Lean

Lemma 2.2

Let $G$ be an extreme value distribution and and $A \in \mathrm{Aff}^+_{\mathbb {R}}$ an orientation preserving affine isomorphism. Then also $A.G$ is an extreme value distribution.

LaTeX Lean

Lemma 7.13Characterization of the subgroup fixing a point

An orientation-preserving affine transformation $A \in \mathrm{Aff}^+_{\mathbb {R}}$ belongs to the subgroup fixing $c \in \mathbb {R}$ if and only if $A(c) = c$.

(Note that the subgroup is a priori defined as the image of a homomorphism, so the statement indeed requires a proof.)

LaTeX Lean

Lemma 7.4Impossibility of expanding affine transformations

Let $(F_n)_{n \in \mathbb {N}}$ be a sequence of c.d.f.s which converges to a nondegenerate c.d.f. $G$, $F_n \overset {\mathrm{d}}{\longrightarrow }G$. Consider affine transformations of the form $A_n(x) = a_n x + b_n$, with $a_n {\gt} 0$ and $b_n \in \mathbb {R}$, such that $a_n \to +\infty $ as $n \to \infty $. Then $A_n . F_n$ cannot converge to any c.d.f.

LaTeX Lean

Lemma 2.13Inverted Taylored version of the limit relation

\begin{align*} \text{(iii)} & & \lim _{n \to \infty } \Big( n \, \big(1 - F (A_n^{-1}(x)) \big) \Big) \, = \; & - \log G(x) \\ \text{(iv)} & & \lim _{n \to \infty } \frac{1}{n \, \big(1 - F (A_n^{-1}(x)) \big)} \, = \; & \frac{1}{-\log G(x)} \end{align*}

are equivalent.

LaTeX Lean

Lemma 2.9Logarithmic version of the limit relation

\begin{align*} \text{(i)} & & \lim _{n \to \infty } \big( (A_n.F)(x) \big)^n \, = \; & G(x) \\ \text{(ii)} & & \lim _{n \to \infty } n \, \log F (A_n^{-1}(x)) \, = \; & \log G(x) \end{align*}

are equivalent.

LaTeX Lean

Lemma 2.11Taylor expansion limit modification

Let $S \subset \mathbb {R}$ be a subset with $0 \in S$, and let $f_1, f_2 \colon S \to \mathbb {R}$ be functions. Let also $(t_n)_{n \in \mathbb {N}}$ be a sequence in $S$, and let $(m_n)_{n \in \mathbb {R}}$ be a sequence of real numbers tending to infinity, $\lim _{n \to \infty } m_n = +\infty $. Assume that for $j = 1,2$

$f_j(0)=0$;
the derivative $f_j'(0)$ exists (derivative taken within the set $S$)

Assume further about $j = 1$ that

$f_1'(0) \ne 0$;
the limit $\lim _{n \to \infty } \big( m_n \, f_1 (t_n) \big)$ exists;
for any $\delta {\gt} 0$ there exists an $\varepsilon {\gt} 0$ such that if $|f_1(t)| {\lt} \varepsilon $ (with $t \in S$) then $|t| {\lt} \delta $.

Denote $c = \frac{1}{f_1'(0)} \, \lim _{n \to \infty } \big( m_n \, f_1 (t_n) \big)$. Then we have $\lim _{n \to 0} t_n = 0$ and

\begin{align*} \lim _{n \to \infty } \Big( m_n \, f_2 (t_n) \Big) \; = \; & c \, f_2’(0) . \end{align*}

LaTeX

Lean

tendsto_smul_apply_smul_deriv_of_tendsto_atTop_of_tendsto_smul_apply_smul_deriv
tendsto_zero_of_tendsto_atTop_of_tendsto_smul

Lemma 4.2Monotone real functions have only countably many points of discontinuity

A monotone function $f \colon \mathbb {R}\to \mathbb {R}$ can have at most countably many points of discontinuity. In particular the set $D \subset \mathbb {R}$ of continuity points of $f$ is dense in $\mathbb {R}$.

LaTeX

Lean

Set.Countable.dense_compl
Monotone.countable_not_continuousAt

Lemma 7.10Only translations have no fixed points

If $A \in \mathrm{Aff}^+_{\mathbb {R}}$ has no fixed points (no $x \in \mathbb {R}$ such that $A(x) = x$) then $A$ belongs to the subgroup of translations, i.e., $A(x) = x + s$ for some $s \in \mathbb {R}$ (in fact $s \ne 0$).

LaTeX Lean

Lemma 3.1Second order differential equation for Q

Suppose that

\begin{align*} Q \colon \mathbb {R}\to \mathbb {R}\end{align*}

is differentiable and satisfies

\begin{align*} Q(0) = 0 \qquad \text{ and } \qquad Q’(0) = 1 \end{align*}

and

\begin{align*} Q(h+s) = Q(h) \alpha (s) + Q(s) \end{align*}

for some $\alpha \colon \mathbb {R}\to \mathbb {R}$ and every $s,h \in \mathbb {R}$. Then $Q$ is twice continuously differentiable and satisfies

\begin{align} Q”(s) = Q’(s) \, Q”(0) \qquad \text{ for every } s \in \mathbb {R}. \end{align}

LaTeX Lean

Lemma 5.6Continuity points of one over negative logarithm c.d.f.

The transform $\frac{\mathbf{1}}{\widetilde{\log } \big( 1 / \widetilde{F} \big)}$ of a c.d.f. $F$ is continuous at $x = -\infty $, $x = + \infty $, and at any $x \in (-\infty ,+\infty )$ where $F$ is continuous.

LaTeX

Lean

CumulativeDistributionFunction.oneDivNegLog_continuousAt
CumulativeDistributionFunction.oneDivNegLog_continuousAt_top
CumulativeDistributionFunction.oneDivNegLog_continuousAt_bot

Lemma 5.4Continuity points of one over one minus c.d.f.

The transform $\frac{\mathbf{1}}{\mathbf{1}-\widetilde{F}}$ of a c.d.f. $F$ is continuous at $x = -\infty $, $x = + \infty $, and at any $x \in (-\infty ,+\infty )$ where $F$ is continuous.

LaTeX

Lean

CumulativeDistributionFunction.oneDivOneSub_continuousAt
CumulativeDistributionFunction.oneDivOneSub_continuousAt_top
CumulativeDistributionFunction.oneDivOneSub_continuousAt_bot

Lemma 1.12

The actions of orientation preserving affine isomorphisms on a cumulative distribution functions is a group action, i.e., $1.F = F$ and $(AB).F = A.(B.F)$ for any c.d.f. $F$ and any $A,B \in \mathrm{Aff}^+_{\mathbb {R}}$.

LaTeX Lean

Lemma 9.4Overlapping union of copies of an interval

Let $J$ be a nontrivial interval of finite length ($0 \, {\lt} \, \Lambda [J] \, {\lt} +\infty $). Let $c {\lt} 1$ and denote $\delta = c \Lambda [J] \, {\lt} \, \Lambda [J]$. Then for any $t \in (-\delta ,\delta )$, the set $J' = (t+J) \cup J$ is an interval (connected set with nonempty interior) whose length satisfies the bound $\Lambda [J'] \, {\lt} \, (1+c) \, \Lambda [J]$.

LaTeX

Lean

volume_union_add_self_ge_of_Ioo_subset
volume_union_add_self_le_of_subset_Icc
isConnected_of_Ioo_subset_of_subset_Icc

Lemma 4.7One of the portmanteau implications

Weak convergence of probability measures implies that if the boundary of a Borel set carries no probability mass under the limit measure, then the limit of the measures of the set equals the measure of the set under the limit probability measure.

In other words, if $\lim _{n \to \infty } \mu _n = \mu $ in the sense of weak convergence of measures, Definition 4.1, and if $A \subset \mathbb {R}$ is a Borel set such that $\mu [\partial A] = 0$, then

\begin{align*} \lim _{n \to \infty } \mu _n [ A ] = \mu [ A ] . \end{align*}

LaTeX

Lean

MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto'
MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto

Lemma 7.16Self-similarity of extreme value distributions

Suppose that $G$ is an extreme-value distribution. Then there exists a family $(A_t)_{t {\gt} 0}$ of oriented affine isomorphisms of $\mathbb {R}$, $A_t \in \mathrm{Aff}^+_{\mathbb {R}}$, such that for any $t {\gt} 0$

\begin{align*} G^t = A_t . G . \end{align*}

Moreover, $t \mapsto A_t$ is a measurable homomorphism of multiplicative groups $(0,+\infty ) \to \mathrm{Aff}^+_{\mathbb {R}}$.

LaTeX Lean

Lemma 9.3Shifts of a smaller interval contained in a larger interval

Let $I, J$ be nontrivial intervals, whose length satisfy

\begin{align*} 0 \; {\lt} \; \Lambda [J] \; {\lt} \; \Lambda [I] \; {\lt} \, +\infty . \end{align*}

Then there exists an open interval $\Delta $ of length $\Lambda [\Delta ] = \Lambda [I] - \Lambda [J] {\gt} 0$ such that

\begin{align*} t + J \; \subset \; I \qquad \text{ for any $t \in \Delta $.} \end{align*}

LaTeX

Lemma 4.6Simple function integral as linear combination of cdf differences

Let $a = c_0 {\lt} c_1 {\lt} \cdots {\lt} c_k = b$ and consider the linear combination of indicator functions

\begin{align*} h(x) = \sum _{j=1}^k \alpha _j \; \mathbb {I}_{{(c_{j-1},c_j]}}(x) . \end{align*}

Then the integral of $h$ with respect to a Borel probability measure $\mu $ on $\mathbb {R}$ whose can be written as

\begin{align*} \int _{\mathbb {R}} h(x) \, \mathrm{d}\mu (x) = \sum _{j=1}^k \alpha _j \, \big( F(c_j) - F(c_{j-1}) \big) , \end{align*}

where $F$ is the c.d.f. of $\mu $.

LaTeX Lean

Lemma 6.2Functional equation scaling coefficient solution

Suppose that $a \colon (0,+\infty ) \to (0,+\infty )$ is a measurable function satisfying, for any $s, t {\gt} 0$,

\begin{align*} a(t s) = \; & a(t) \, a(s) . \end{align*}

Then there exists a $\rho \in \mathbb {R}$ such that for all $t {\gt} 0$,

\begin{align*} a(t) = t^{\rho } . \end{align*}

LaTeX Lean

Lemma 6.3Functional equation translation coefficient solution with $\rho = 0$

Suppose that $b \colon (0,+\infty ) \to \mathbb {R}$ is a measurable function satisfying, for any $s, t {\gt} 0$,

\begin{align*} b(t s) = \; & b(s) + b(t) . \end{align*}

Then there exists a constant $c$ such that for $t \in (0,+\infty )$ we have

\begin{align*} b(t) = \; & -c \, \log (t) . \end{align*}

LaTeX

Lemma 6.4Functional equation translation coefficient solution with $\rho \ne 0$

Suppose that $\rho \in \mathbb {R}\setminus \left\{ 0 \right\} $ and $b \colon (0,+\infty ) \to \mathbb {R}$ is a measurable function satisfying, for any $s, t {\gt} 0$,

\begin{align*} b(t s) = \; & t^{\rho } \, b(s) + b(t) . \end{align*}

Then there exists a constant $c$ such that for $t \in (0,+\infty ) \setminus \left\{ 1 \right\} $ we have

\begin{align*} b(t) = \; & c (1 - t^{-\rho }) . \end{align*}

LaTeX

Lemma 3.4Solution for E

Suppose that $E \colon (0,\infty ) \to \mathbb {R}$ is nondecreasing and nonconstant function which satisfies $E(1) = 0$ and

\begin{align*} E(\lambda \sigma ) = E(\lambda ) A(\sigma ) + E(\sigma ) \end{align*}

for some $A \colon (0,\infty ) \to (0,\infty )$ and all $\lambda , \sigma {\gt} 0$. Then, denoting $c = E'(1)$ and $\gamma = \frac{1}{E'(1)} \frac{\mathrm{d}^2}{\mathrm{d}{s}^2} E(e^s) \big|_{s=0}$, for all $\lambda \in \mathbb {R}$ we have

\begin{align*} E(\lambda ) = \begin{cases} c \big( \lambda ^\gamma - 1 \big) & \; \; \text{ if $\gamma \ne 0$.} \\ c \, \log (\lambda ) & \; \; \text{ if $\gamma = 0$.} \end{cases}\end{align*}

LaTeX Lean

Lemma 3.2Solution for Q

Suppose that $Q \colon \mathbb {R}\to \mathbb {R}$ is twice continuously differentiable and $Q'$ is positive and $Q$ and satisfies $Q(0)=0$, $Q'(0) = 1$, and the equation concluded in Lemma 3.1 with $\gamma = Q''(0)$, i.e.,

\begin{align} \label{eq: Q eqn dd} Q”(s) = \gamma \, Q’(s) \qquad \text{ for every } s \in \mathbb {R}. \end{align}

Then $Q$ is given by

\begin{align*} Q(s) = \begin{cases} \frac{e^{\gamma s} - 1}{\gamma } & \; \text{ if $\gamma \ne 0$} \\ \; \; s & \; \text{ if $\gamma = 0$} \end{cases} \qquad \text{for $s \in \mathbb {R}$.} \end{align*}

LaTeX Lean

Lemma 4.4Subdivision with small mesh and within dense set

Let $D \subset \mathbb {R}$ be a dense set and $a,b \in D$ with $a {\lt} b$. Then for any $\delta {\gt} 0$ there exists a $k \in \mathbb {N}$ and $a = c_0, c_1, \ldots , c_{k-1}, c_k = b \in D$ such that $|c_j - c_{j-1}| {\lt} \delta $ for all $j=1,\ldots ,k$.

LaTeX Lean

Lemma 2.12Taylored version of the limit relation

\begin{align*} \text{(ii)} & & \lim _{n \to \infty } n \, \log F (A_n^{-1}(x)) \, = \; & \log G(x) \\ \text{(iii)} & & \lim _{n \to \infty } \Big( n \, \big(1 - F (A_n^{-1}(x)) \big) \Big) \, = \; & - \log G(x) \end{align*}

are equivalent.

LaTeX Lean

Lemma 2.14Transformed version of the limit relation

\begin{align*} \text{(iv)} & & \lim _{n \to \infty } \frac{1}{n \, \big(1 - F (A_n^{-1}(x)) \big)} \, = \; & \frac{1}{-\log G(x)} \\ \text{(v)} & & \lim _{n \to \infty } \frac{1}{n} \frac{\mathbf{1}}{\mathbf{1}-\widetilde{A_n . F}} (x) \, = \; & \frac{\mathbf{1}}{\widetilde{\log } \big( 1 / \widetilde{G} \big)} (x) \end{align*}

are equivalent.

(See Definitions 5.3 and 5.5 for the transforms involved in condition (v)).

LaTeX Lean

Lemma 7.2Unique affine relation among two nondegenerate c.d.f.s

Let $F, G$ be two c.d.f.s of the same type, and $A \in \mathrm{Aff}^+_{\mathbb {R}}$ an affine isomorphism such that $G = A.F$. If $F$ is nondegenerate, then $A$ is the only element of $\mathrm{Aff}^+_{\mathbb {R}}$ for which the relation $G = A.F$ holds.

LaTeX Lean

Lemma 7.8A choice of normalizing constants for convergence to types

(It is possible to choose normalization constants for the affine transformations using the left-continuous inverses of the c.d.f.s. TODO: Precise statement.)

LaTeX

Theorem 4.8Sufficient condition for convergence in distribution with cdfs

Let $F$ and $F_n$, $n \in \mathbb {N}$, be cumulative distribution functions of probability measures $\mu $ and $\mu _n$, $n \in \mathbb {N}$, respectively, i.e.,

If $\lim _{n \to \infty } F_n(x) = F(x)$ for all continuity points $x$ of $F$, then $\lim _{n \to \infty } \mu _n = \mu $ in the sense of weak convergence of measures, Definition 4.1.

LaTeX Lean

Theorem 7.5Convergence to types

Suppose that $(F_n)_{n \in \mathbb {N}}$ is a sequence of c.d.f.s which converges to a nondegenerate c.d.f. $G$, i.e., $F_n \overset {\mathrm{d}}{\longrightarrow }G$ as $n \to \infty $. Let $(A_n)_{n \in \mathbb {N}}$ be a sequence of oriented affine isomorphisms of $\mathbb {R}$, $A_n \in \mathrm{Aff}^+_{\mathbb {R}}$ such that $A_n.F_n \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}$ for some c.d.f. $\widetilde{G}$.

If we write $A_n(x) = a_n x + b_n$, then $(a_n)_{n \in \mathbb {N}}$ and $(b_n)_{n \in \mathbb {N}}$ are bounded sequences.

If $\widetilde{G}$ is nondegenerate, then $A_n \to A \in \mathrm{Aff}^+_{\mathbb {R}}$ and $A.G = \widetilde{G}$. In particular $G$ and $\widetilde{G}$ are of the same type. Moreover, $A$ is the unique affine transformation for which the equality $A.G = \widetilde{G}$ holds.

LaTeX

Theorem 7.6Convergence to types again

Let $(F_n)_{n \in \mathbb {N}}$ be a sequence of c.d.f.s such that $A_n.F_n \overset {\mathrm{d}}{\longrightarrow }G$, with $G$ a nondegenerate c.d.f.

Then the convergence of also $\widetilde{A}_n.F_n \overset {\mathrm{d}}{\longrightarrow }G$ holds if and only if the coefficients of the affine maps satisfy the relations

\begin{align*} \frac{\tilde{a}_n}{a_n} \to 1 \quad \text{ and } \quad \frac{a_n \tilde{b}_n - \tilde{a}_n b_n}{a_n} \to 0, \end{align*}

or equivalently,

\begin{align*} \frac{\tilde{c}_n}{c_n} \to 1 \quad \text{ and } \quad \frac{\tilde{d}_n - d_n}{c_n} \to 0 . \end{align*}

LaTeX

Theorem 2.8

For any $\alpha {\gt} 0$, the standard Fréchet distribution $\Phi _{\alpha }$ is an extreme value distribution.

LaTeX Lean

Theorem 2.6

The standard Gumbel distribution $\Lambda $ is an extreme value distribution.

LaTeX Lean

Theorem 3.3Monotone functions are a.e. differentiable

If $f : \mathbb {R}\to \mathbb {R}$ is nondecreasing, then the derivative $f'(x)$ exists at almost every $x \in \mathbb {R}$. In particular there exists points $x$ where $f'(x)$ exists.

LaTeX Lean

Theorem 6.5One-parameter subgroups of affine isomorphisms of $\mathbb {R}$

[TODO: Switch to additive notation and $\mathbb {R}$ rather than multiplicative notation and $(0,+\infty )$, to match the most convenient formalized statements.]

Suppose that $t \mapsto A_t$ is a measurable homomorphism of multiplicative groups $(0,+\infty ) \to \mathrm{Aff}^+_{\mathbb {R}}$, i.e., for any $s, t {\gt} 0$ we have

\begin{align*} A_{s t} = A_s \circ A_t \end{align*}

and $A_t(x) = a_t x + b_t$, with $t \mapsto a_t$ and $t \mapsto b_t$ measurable functions. Then either

(0)

there exists a $\beta \in \mathbb {R}$ such that for all $t {\gt} 0$ and $x \in \mathbb {R}$

\begin{align*} A_t(x) = x + \beta \, \log (t) ; \end{align*}

(1)

there exists a $\rho \ne 0$ and $c \in \mathbb {R}$ such that for all $t {\gt} 0$ and $x \in \mathbb {R}$

\begin{align*} A_t(x) = t^{\rho } (x - c) + c . \end{align*}

LaTeX

Lean

AffineIncrEquiv.homomorphism_from_Real_characterization
AffineIncrEquiv.homomorphism_from_Real_characterization_of_nontrivial

Theorem 2.15Equivalent versions of the limit relation

\begin{align*} \text{(i)} & & \lim _{n \to \infty } \big( (A_n.F)(x) \big)^n \, = \; & G(x) \\ \text{(ii)} & & \lim _{n \to \infty } n \, \log F (A_n^{-1}(x)) \, = \; & \log G(x) \\ \text{(iii)} & & \lim _{n \to \infty } \Big( n \, \big(1 - F (A_n^{-1}(x)) \big) \Big) \, = \; & - \log G(x) \\ \text{(iv)} & & \lim _{n \to \infty } \frac{1}{n \, \big(1 - F (A_n^{-1}(x)) \big)} \, = \; & \frac{1}{-\log G(x)} \\ \text{(v)} & & \lim _{n \to \infty } \frac{1}{n} \frac{\mathbf{1}}{\mathbf{1}-\widetilde{A_n . F}} (x) \, = \; & \frac{\mathbf{1}}{\widetilde{\log } \big( 1 / \widetilde{G} \big)} (x) \end{align*}

are equivalent.

(See Definitions 5.3 and 5.5 for the transforms involved in condition (v)).

(More equivalent conditions are to be added; this is just a theorem to collect various equivalent phrasings.)

LaTeX Lean

Theorem 7.20Three types of extreme value distributions [Fisher-Tippett-Gnedenko]

For any extreme value distribution $G$, one of the following holds:

: ($\Lambda $) $G = A . \Lambda $ for some $A \in \mathrm{Aff}^+_{\mathbb {R}}$;
: ($\Phi _{{}}$) $G = A . \Phi _{\alpha }$ for some $A \in \mathrm{Aff}^+_{\mathbb {R}}$ and $\alpha {\gt} 0$;
: ($\Psi _{{}}$) $G = A . \Psi _{\alpha }$ for some $A \in \mathrm{Aff}^+_{\mathbb {R}}$ and $\alpha {\gt} 0$.

In particular, the only three possible types of extreme value distributions are the type of the Gumbel c.d.f., the type of the Fréchet c.d.f. $\Phi _{\alpha }$ for $\alpha {\gt} 0$, and the type of the Weibull c.d.f. $\Psi _{\alpha }$ for $\alpha {\gt} 0$.

LaTeX Lean

Theorem 2.7

For any $\alpha {\gt} 0$, the standard Weibull distribution $\Psi _{\alpha }$ is an extreme value distribution.

LaTeX Lean