Since \(F\) is nondegenerate, we can find two different points \(x_1 {\lt} x_2\) such that \(0 {\lt} F(x_1) {\lt} F(x_2) \le 1\). By right continuity of \(F\), we can assume these points to be taken minimal with the given values, i.e., \(x_j = \inf \big\{ x \in \mathbb {R}\; \big| \; F(x) = F(x_j) \big\} \) for \(j=1,2\).

The assumption \(G = A.F\) means \(G(x) = F \big( A^{-1}(x) \big)\) for all \(x \in \mathbb {R}\). Therefore \(G \big( A(x_1) \big) = F(x_1) {\lt} F(x_2) = G \big( A(x_2) \big)\). We also get \(A(x_j) = \inf \big\{ y \in \mathbb {R}\; \big| \; G(y) = F(x_j) \big\} \) for \(j=1,2\) by strict monotonicity and bijectivity of \(A\) (if, for example, there would exist a \(y'_2 {\lt} A(x_2)\) such that \(G(y'_2) = F(x_2)\), then the point \(x'_2 = A^{-1}(y'_2) {\lt} x_2\) would be such that \(F\big(A^{-1}(y'_2)\big) = G(y'_2) = F(x_2)\), contradicting the minimality of \(x_2\)).

If \(\widetilde{A} \in \mathrm{Aff}^+_{\mathbb {R}}\) is also such that \(G = \widetilde{A}.F\), then the same holds for it: \(\widetilde{A}(x_j) = \inf \big\{ y \in \mathbb {R}\; \big| \; G(y) = F(x_j) \big\} \) for \(j=1,2\). We conclude that

But an affine map of \(\mathbb {R}\) is determined by its values at two distinct points: from \(a x_1 + b = y_1\) and \(a x_2 + b = y_2\) with \(x_1 \ne x_2\) one can solve \(a, b\). Therefore we must have \(\widetilde{A} = A\).

It suffices to prove that for any \(x {\lt} \beta \) we have \(\widetilde{G}(x) = 0\) and for any \(x {\gt} \beta \) we have \(\widetilde{G}(x) = 1\).

Let us focus on the latter, so let \(x {\gt} \beta \). Let also \(\varepsilon {\gt} 0\); we will prove that \(\widetilde{G}(x) {\gt} 1 - \varepsilon \), and the claim will follow.

By density of continuity points of \(\widetilde{G}\), we can choose \(x'\) such that \(\beta {\lt} x' {\lt} x\) and \(\widetilde{G}\) is continuous at \(x'\). Then the assumed convergence \(A_n . F_n \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}\) implies that \((A_n . F_n)(x') \to \widetilde{G}(x')\). Since \(\widetilde{G}(x) \ge \widetilde{G}(x')\), it suffices to prove that \(\widetilde{G}(x') {\gt} 1 - \varepsilon \).

Since \(G\) is a c.d.f., we can choose a continuity point \(z\) of \(G\) large enough so that \(G(z) {\gt} 1 - \varepsilon \). Then by the assumed convergence \(F_n \overset {\mathrm{d}}{\longrightarrow }G\), we have \(F_n(z) \to G(z)\). By definition we have

Note that \(A_n(z) = a_n z + b_n \to \beta \) as \(n \to \infty \) by the assumptions \(a_n \to 0\) and \(b_n \to \beta \). In particular, for \(n\) large enough, we have \(A_n(z) {\lt} x'\). Therefore, for \(n\) large enough

The LHS tends to \(G(z)\) and the RHS tends to \(\widetilde{G}(x')\), showing

This concludes the proof that \(\widetilde{G}(x) = 1\) for all \(x {\gt} \beta \).

The proof that \(\widetilde{G}(x) = 0\) for all \(x {\lt} \beta \) is similar.

Since \(G\) is assumed nondegenerate, by Lemma 1.16 we can pick two continuity points \(x_1 {\lt} x_2\) of \(G\) such that \(0 {\lt} G(x_1) \le G(x_2) {\lt} 1\). Then from the assumption \(F_n \overset {\mathrm{d}}{\longrightarrow }G\) we get \(F_n(x_1) \to G(x_1)\) and \(F_n(x_2) \to G(x_2)\).

Assume, by way of contradiction, that we have convergence \(A_n . F \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}\) to some c.d.f. \(\widetilde{G}\).

We claim that then \(\big(A_n(x_1)\big)_{n \in \mathbb {N}}\) is bounded from below and \(\big(A_n(x_2)\big)_{n \in \mathbb {N}}\) is bounded from above. Since

this will show that \((a_n)_{n \in \mathbb {N}}\) is bounded from above, contradicting the assumption \(a_n \to +\infty \), and finishing the proof.

To show that \(\big(A_n(x_1)\big)_{n \in \mathbb {N}}\) is bounded from below, choose a continuity point \(z\) of \(\widetilde{G}\) such that \(\widetilde{G}(z) {\lt} G(x_1)\). Then the assumed convergence \(A_n . F \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}\) implies \((A_n . F)(z) \to \widetilde{G}(z)\). On the other hand, if \(\big(A_n(x_1)\big)_{n \in \mathbb {N}}\) is not bounded from below, then along some subsequence \((n_k)_{k \in \mathbb {N}}\) of indices we have \(A_{n_k}(x_1) {\lt} z\), and for those indices we then have

The LHS tends to \(G(x_1)\) as \(k \to \infty \), whereas the RHS tends to \(\widetilde{G}(z)\). We get \(G(x_1) \le \widetilde{G}(z)\), contradicting the choice of \(z\). This shows that \(\big(A_n(x_1)\big)_{n \in \mathbb {N}}\) must in fact be bounded from below.

The proof that \(\big(A_n(x_2)\big)_{n \in \mathbb {N}}\) must be bounded from above is similar.

Let us first argue that \((a_n)_{n \in \mathbb {N}}\) are bounded. If not, then by passing to a subsequence, we have \(a_{n_k} \to +\infty \). But since \(F_{n_k} \overset {\mathrm{d}}{\longrightarrow }G\) and \(G\) is nondegenerate, it contradicts Lemma 7.4 to have \(A_{n_k} . F_{n_k} \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}\). Therefore \((a_n)_{n \in \mathbb {N}}\) must be bounded: there exists some \(M{\gt}0\) such that \(a_n \le M\) for all \(n \in \mathbb {N}\).

Let us then argue that \((b_n)_{n \in \mathbb {N}}\) is bounded. If not, then we can extract a subsequence such that either \(b_{n_k} \to -\infty \) or \(b_{n_k} \to +\infty \). Let us prove the impossibility of the second one, the first is similar. So assume that \(b_{n_k} \to +\infty \). Since \(G\) is nondegenerate, we may pick a continuity point \(x_0\) of \(G\) such that \(0 {\lt} G(x_0) {\lt} 1\). Then we have \(F_n(x_0) \to G(x_0)\) by the assumption \(F_n \overset {\mathrm{d}}{\longrightarrow }G\). We may also pick a continuity point \(z\) of \(\widetilde{G}\) such that \(\widetilde{G}(z) {\gt} G(x_0)\). Then we have \((A_n.F_n)(z) \to \widetilde{G}(z)\) by the assumption \(A_n.F_n \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}\). But \(A_{n_k}(x_0) = a_{n_k} x_0 + b_{n_k} \to +\infty \), since \(0 {\lt} a_{n_k} \le M\) and \(b_{n_k} \to +\infty \). Therefore we have for all large enough \(k\) that \(A_{n_k}(x_0) {\gt} z\). And then

The LHS tends to \(\widetilde{G}(z)\) as \(k \to \infty \), and the RHS tends to \(G(x_0)\). Therefore we get \(\widetilde{G}(z) \le G(x_0)\), contradicting the choice of \(z\). This shows that we cannot have \(b_{n_k} \to +\infty \). Similarly one proves that we cannot have \(b_{n_k} \to -\infty \). We conclude that \((b_n)_{n \in \mathbb {N}}\) is indeed bounded.

From now on, suppose furthermore that also \(\widetilde{G}\) is nondegenerate. We claim that then \((a_n)_{n \in \mathbb {N}}\) is bounded away from \(0\): for some \(\varepsilon {\gt} 0\) we have \(a_n \ge \varepsilon \) for all \(n \in \mathbb {N}\). If not, then we could extract a subsequence such that \(a_{n_k} \to 0\) and also \(b_n \to \beta \) (since \(b_n\) is bounded). But since \(F_{n_k} \overset {\mathrm{d}}{\longrightarrow }G\) and \(G\) is nondegenerate, from Lemma 7.3 we would get \(A_{n_k} . F_{n_k} \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}_0\), where \(\widetilde{G}_0\) is degenerate. But by assumption \(A_{n_k} . F_{n_k} \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}\), where \(\widetilde{G}\) is nondegenerate; this is impossible by uniqueness of limits for convergence in distribution. Therefore \((a_n)_{n \in \mathbb {N}}\) must indeed be bounded away from \(0\).

Note that since \((a_n)_{n \in \mathbb {N}}\) is bounded away from \(0\) and \(+\infty \), and \((b_n)_{n \in \mathbb {N}}\) is bounded, we can extract a subsequence such that \(a_{n_k} \to \alpha \in (0,+\infty )\) and \(b_{n_k} \to \beta \in \mathbb {R}\). By assumption, we have \(A_{n_k} . F_{n_k} \overset {\mathrm{d}}{\longrightarrow }\widetilde{G}\). But since \(A_{n_k} \to A\) where \(A(x) = \alpha x + \beta \) and we have also assumed \(F_{n_k} \overset {\mathrm{d}}{\longrightarrow }G\), this implies by continuity (Lemma 1.22) that \(A_{n_k} . F_{n_k} \overset {\mathrm{d}}{\longrightarrow }A . G\). By uniqueness of limits, we get \(A . G = \widetilde{G}\).

To prove that in fact \(A_n \to A\), not just along a subsequence, note the following. From any subsequence \(A_{n_k}\), we can extract a further convergent subsequence of values of \(a_{n_{k_\ell }}\) and \(b_{n_{k_\ell }}\) values as above, with limits \(\alpha ' \in (0,+\infty )\) and \(\beta ' \in \mathbb {R}\). The same argument as above shows that \(A' . G = \widetilde{G}\) where \(A'(x) = \alpha ' x + \beta '\). Lemma 7.2 then says that we must have \(A' = A\), i.e., \(\alpha ' = \alpha \) and \(\beta ' = \beta \). Since any subsequence has a convergent further subsequence with the same limit, the entire sequence must converge, \(A_n \to A\). The proof is complete.

(This is actually just a special case of what is stated as Corollary 7.7 below. The better organization is to prove that corollary directly, and obtain this lemma as a special case.)

We will apply the convergence to types with the reference sequence \((A_n.F_n)_{n \in \mathbb {N}}\), which by assumption tends to a nondegenerate \(G\).

To express the other sequence in terms of the reference sequence, we write

By assumption this also tends to \(G\).

Theorem 7.5 applies, and guarantees convergence \(\widetilde{A}_n A_n^{-1} \to A\) to some \(A \in \mathrm{Aff}^+_{\mathbb {R}}\), and it also implies \(A.G = G\) (note that the other limit is also \(G\) by our assumptions). However, the unique \(A\) for which we have \(A.G = G\) is \(A = \mathrm{id}\). We therefore get \(\widetilde{A}_n A_n^{-1} \to \operatorname{id}\). To explicitly see the coefficients, note that

and

The convergence \(\widetilde{A}_n A_n^{-1} \to \operatorname{id}\) is equivalent to the convergence of the coefficients,

The second one can be rewritten as

We will apply the convergence to types with the reference sequence \((A_n.F_n)_{n \in \mathbb {N}}\), which by assumption tends to a nondegenerate \(G\).

To express the other sequence in terms of the reference sequence, we write

By assumption this tends to a nondegenerate \(\widetilde{G}\).

Theorem 7.5 applies, and guarantees convergence \(\widetilde{A}_n A_n^{-1} \to A\) to some \(A \in \mathrm{Aff}^+_{\mathbb {R}}\), and it also implies \(A.G = \widetilde{G}\).

Write \(A(x) = \alpha x + \beta \). To explicitly see the coefficients of \(\widetilde{A}_n A_n^{-1}\), note that

and

The convergence \(\widetilde{A}_n A_n^{-1} \to A\) is equivalent to the convergence of the coefficients,

The second one can be rewritten as

…

Let us prove this by contrapositive: that any element \(A\) which is not a translation must have a fixed point. So assume that \(A\) is not a translation, i.e., \(A(x) = a x + b\) with some \(a \ne 1\). Then the fixed point equation \(A(x) = x\) reads

and it has a solution \(x = \frac{-b}{a-1} \in \mathbb {R}\), which then is a fixed point of \(A\).

Calculate, for \(x \in \mathbb {R}\)

Suppose first that \(A\) is an element of the said subgroup, i.e., \(A(x) = e^{s} (x - c) + c\) for some \(s \in \mathbb {R}\). Then clearly \(A(c) = c\).

Suppose then that \(A(c) = c\). Write \(A(x) = a x + b\) for \(a{\gt}0\) and \(b \in \mathbb {R}\). Plug in \(x=c\) in the assumed fixed point property to obtain

The above can be solved to give \(b = (1-a)c\). Also since \(a{\gt}0\), we can write \(a = e^s\) with \(s \in \mathbb {R}\). With these, the formula for \(A\) simplifies to

This shows \(A = A_s\) as desired (with \(A_s\) as in Definition 7.12).

Calculate, for \(x \in \mathbb {R}\)

Let \(t {\gt} 0\) and let \(x \in \mathbb {R}\) be a continuity point of \(G\). For \(n \in \mathbb {N}\), calculate

By assumption, we have \(\big((A_n . F) (x) \big)^n \to G(x)\) as \(n \to \infty \). Also \(\lfloor n t \rfloor / n \to t\) as \(n \to \infty \). By (joint) continuity of the power function \((x,y) \mapsto x^y = \exp \big( y \, \log (x) \big)\), we get that the expression above tends to \(G(x)^t\).

Finally noting that the continuity points of \(G^t\) are the same as the continuity points of \(G\), the above in fact proves the asserted \(A_{n}.F^{\lfloor n t \rfloor } \overset {\mathrm{d}}{\longrightarrow }G^t\).

…

Since \(G\) is nondegenerate, there exists an \(x_0 \in \mathbb {R}\) with \(0 {\lt} G(x_0) {\lt} 1\). Write \(q = -\log G(x_0) {\gt} 0\), so that \(G(x_0) = e^{-q}\).

For \(t {\gt} 0\), from the equation \(G^{t} = A_t . G\) we get for any \(x \in \mathbb {R}\)

In particular, with \(x = x_0 + \beta \, \log (t)\), we get

from which we can solve

The above holds for any \(t{\gt}0\), and any \(x \in \mathbb {R}\) can be written as \(x = x_0 + \beta \, \log \big( e^{(x - x_0)/\beta } \big)\). We therefore get, for any \(x \in \mathbb {R}\),

This is of the desired form, with \(d = \frac{x_0}{\beta } + \log (q)\). Plugging in \(x = 0\) then shows \(d = \log \big(-\log G(0) \big)\).

Since \(G\) is nondegenerate, there exists an \(x_0 \in \mathbb {R}\) with \(0 {\lt} G(x_0) {\lt} 1\). Write \(q = -\log G(x_0) {\gt} 0\), so that \(G(x_0) = e^{-q}\).

For \(t {\gt} 0\), from the equation \(G^{t} = A_t . G\) we get for any \(x \in \mathbb {R}\)

Note that for \(x \le c\) and \(t = 2\) we have \(A_2^{-1}(x) = 2^{-\alpha }(x-c) + c \ge x\), so the above implies \(G(x)^2 = G(A_2^{-1}(x)) \ge G(x)\). This not possible if \(0 {\lt} G(x) {\lt} 1\), so we must in particular have \(x_0 {\gt} c\).

With \(x = A_t(x_0)\) in the above equation, we get

from which we can solve

Any \(x \ge c\) can be written as \(x = A_t(x_0) = t^{\alpha } (x_0-c) + c\) with \(t = \big( \frac{x - c}{x_0 - c} \big)^{1/\alpha }\) (recall that \(x_0 - c {\gt} 0\)). We therefore get, for any \(x \ge c\),

This is of the form

and plugging in \(x = c + 1\) yields \(\sigma = \big(- \log G(c+1)\big)^{\alpha }\).

(Note: The Lean formalized statement uses the opposite sign of \(\alpha \): it is assumed that \(\alpha {\lt} 0\) and \(A_t(x) = t^{+\alpha } (x-c) + c\).)

Since \(G\) is nondegenerate, there exists an \(x_0 \in \mathbb {R}\) with \(0 {\lt} G(x_0) {\lt} 1\). Write \(q = -\log G(x_0) {\gt} 0\), so that \(G(x_0) = e^{-q}\).

For \(t {\gt} 0\), from the equation \(G^{t} = A_t . G\) we get for any \(x \in \mathbb {R}\)

Note that for \(x \ge c\) and \(t = 2\) we have \(A_2^{-1}(x) = 2^{\alpha }(x-c) + c \ge x\), so the above implies \(G(x)^2 = G(A_2^{-1}(x)) \ge G(x)\). This not possible if \(0 {\lt} G(x) {\lt} 1\), so we must in particular have \(x_0 {\lt} c\).

With \(x = A_t(x_0)\) in the above equation, we get

from which we can solve

Any \(x \le c\) can be written as \(x = A_t(x_0) = t^{-\alpha } (x_0-c) + c\) with \(t = \big( \frac{c - x}{c - x_0} \big)^{-1/\alpha }\) (recall that \(c - x_0 {\gt} 0\)). We therefore get, for any \(x \le c\),

This is of the form

and plugging in \(x = c - 1\) yields \(\sigma = \big(- \log G(c-1)\big)^{-\alpha }\).

…