1 Results of the literature
The results of the literature on which the paper relies, and which are not in Mathlib, enter the Lean statements as hypotheses. Each is a proposition of Literature.lean, and the statements that use it assume it. The other cited results are in Mathlib (Sion’s minimax theorem, Doob’s maximal inequality and convergence theorem, the strong law of large numbers, Fubini’s theorem, Fatou’s lemma, and Jensen’s inequality) or are proved in the library (the uniqueness of the numéraire, the inequality of the Donsker–Varadhan variational formula, and Ville’s inequality).
Let \((G_n)_{0\le n\le N}\) be a nonnegative process adapted to a filtration, with \(\mathrm{E}_P(G_n){\lt}\infty \) for every \(n\). Its Snell envelope \(S\), defined by backward induction, dominates \(G\), is a supermartingale under \(P\), and is dominated by every supermartingale that dominates \(G\). Moreover, \(\mathrm{E}_P(S_0)=\sup _\tau \mathrm{E}_P(G_{\tau \wedge N})\), where \(\tau \) ranges over the stopping times of the filtration.
Let \(\mathcal{X}\) be finite, let \(T\ge 0\), and let \(\xi \in \Delta _T\). Then \(\inf _{\bar P\in \mathcal{B}}\mathrm{KL}(Q^\xi \| \bar P)\le \sup _{(E_t)}\sum _{t=0}^T\xi _t\mathrm{E}_Q(\log E_t)\), where \((E_t)\) ranges over the e-processes. Their primal-dual equivalence, applied to a data-independent stopping time with distribution \(\xi \), gives the equality over their Bayesian mixtures of stopped null distributions, which belong to \(\mathcal{B}\).
For the random walk \((S_t)_{t\ge 0}\) with \(S_0=0\) and independent \(\mathrm{N}(0,1)\) increments, almost surely, \(\limsup _{t\to \infty }S_t/(2t\log \log t)^{1/2}=1\) and \(\liminf _{t\to \infty }S_t/(2t\log \log t)^{1/2}=-1\).
For every nonempty null of probability measures and every alternative probability measure, a numéraire exists at every horizon.
Let \(A(e)=(e-1-\log e)/(\log e)^2\) for \(e{\gt}1\) and \(A(1)=1/2\), the adjuster of their eq. (12). If \((M_t)\) is a test supermartingale with respect to a filtration coarser than \((\mathcal{F}_t)\), then the process with terms \(A(\max _{i\le t}M_i)\) is an e-process with respect to \((\mathcal{F}_t)\).