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

9 Formalization notes

The formalization makes explicit the following conventions, which the paper leaves implicit and which do not change its results. Section S5 of the supplementary material lists the parts of the paper that were improved after the formalization and the steps in which the formal proofs differ. The other departures of the formal proofs from those of the paper are given in the proofs of the previous chapters and in the docstrings of the Lean modules.

9.1 Types and values

  • The observations take values in a measurable space \(\mathcal{X}\) of a universe \(u\), and a path \(x\colon \mathbb {N}\to \mathcal{X}\) carries the product \(\sigma \)-algebra. The coordinate \(x_i\) is the observation \(X_{i+1}\). The null \(\mathcal{P}\) is written \(\mathfrak {P}\) in Lean, since \(\mathcal{P}\) is the notation of Mathlib for the power set.

  • E-variables and e-processes take values in \([0,\infty ]\), and stopping times take the values \(0,1,\ldots \) and \(\infty \), with \(E_\infty =\limsup _{t\to \infty }E_t\).

  • Expectations in \([-\infty ,\infty ]\) are the integral of the positive part minus that of the negative part, in the extended reals, where \(\infty -\infty =-\infty \). Regrets, e-powers, and minimax regrets take values in \([-\infty ,\infty ]\), and \(\eta _T\) in \([0,\infty ]\), with \(\log \infty =\infty \).

  • Ratios in \([0,\infty ]\) follow \(0/0=0\) and \(\infty /\infty =0\), while Larsson, Ramdas and Ruf (2025) take \(\infty /\infty =1\); this does not affect the regrets, since a numéraire is positive and finite \(Q\)-almost surely under the standing assumption, and their numéraire satisfies the definition used here.

  • A sum \(\sum _t\xi _tR_t(E_t)\) is taken in the extended reals, where \(0\times \infty =0\), the convention of Lemma 1.

  • Suprema over a condition are taken in \([0,\infty ]\) or in the extended reals, since a real supremum takes the value zero when the condition fails.

9.2 The setting and the statements

  • The standing assumption of Section 2 (Definition 11) collects the hypotheses of the paper: probability measures, numéraires at every horizon in versions fixed once and for all, and \(\sup _{E\in \mathcal{E}_t}\mathrm{E}_Q(\log E){\lt}\infty \).

  • In the Gaussian model, the numéraires of \(Q\) are taken in the versions \(\prod _{i=2}^t\ell (Y_i)\) of Proposition 2, and the regrets \(R^\mu _t\) use any numéraires of \(Q_\mu \); the statements on the mixtures with \(\rho ^2{\lt}1-s^2\) use any numéraires of \(Q\), which exist by the theorem of Larsson, Ramdas and Ruf.

  • The pairs \((t,x^t)\) of Section 3 are pairs of a time and a whole path, under the \(\sigma \)-algebra that observes only \(x^t\). A mixture in \(\mathcal{B}\) is the distribution of \((\tau _\Lambda (X,U),X^\tau )\) for \(\Lambda \sim \pi \) in a measurable space of the universe \(u\), \(X\sim P_\Lambda \) given \(\Lambda \), and \(U\) uniform on \([0,1]\).

  • The random walk of Lemma 2 is realized on the space of its increments.

  • Limits of ratios such as \(\Gamma _T/\log \log T\) are limits in the extended reals, so that a limit statement also states that the numerator is eventually finite.

  • Lemmas S4 to S6 are stated for every \(\rho {\gt}0\) and any numéraires of \(Q\), the generality in which the proof of Proposition S5 uses them.

  • The claims of Example S1 and of Sections S3 and S4 that do not depend on a computation are stated in general form (Lemmas 25, 26, and 27, and Lemma 98). The numerical results, values, and computations are not formalized: Example S1 and Table S1, the values \(1.1132068\) and \(0.885\) of Section S2.3, the computations of Sections S3 and S4 with Tables S2 and S3, Fig. 1, the comparison with three fifths in Section 4.3, and the numbers of Section 5.

  • The statements and comparisons of the literature, the interpretations and proof outlines of the main text, the explanations at the start of Sections S1.3, S1.6, and S1.7, and the conjectures and open questions of Section 5 are not formalized.

9.3 Findings

  • Three parts of the paper were improved after the formalization (Section S5 of the supplementary material): Proposition S1(ii) now holds on every sample space, Proposition S5 now also gives the limit of \(\log \eta _T\), on which the claim of Section 4.3 that Proposition 3(i) holds for every \(\rho {\gt}0\) relies, and the proofs of Lemma 1, Remark 2, and Proposition S1(i) are shorter.

  • As first stated, the claim that test supermartingales are e-processes was false for an empty null, because the adaptedness came only from the supermartingale property under some null distribution; test supermartingales are now adapted by definition.

  • Some hypotheses of the paper are not needed: \(\alpha \le 1\) in the threshold test of Section 5, \(s\ne 1\) for (S15), and \(\rho \ge 0\) in the claims of Section S2.3; Proposition S4(ii) holds for \(s\ge 1\), and the standing assumption holds for every mixture \(Q\), whatever \(\rho \).

  • The series of Proposition S3(i) converges only as the limit of its partial sums.

  • The fact \(E^{\star }_0=1\) of Section 2 needs a nonempty null, which the standing assumption gives.