An iterated-logarithm price of anytime validity for log-optimal e-processes: Lean formalization

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).

Definition 1 Peskir and Shiryaev (2006, Theorem 1.2)
✓
#

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.

Definition 2 Koolen and Grünwald (2022, Theorem 5)
✓
#

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}\).

Definition 3 The law of the iterated logarithm
✓
#

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\).

Definition 4 Larsson, Ramdas and Ruf (2025, Theorem 2.6)
✓
#

For every nonempty null of probability measures and every alternative probability measure, a numéraire exists at every horizon.

Definition 5 Choe and Ramdas (2026, Theorem 2)
✓

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)\).