An iterated-logarithm price of anytime validity for log-optimal e-processes
Adrien Corenflos
math.ST
Nov 9, 2026 · v1
math.PR stat.ME
TL;DR
All lemmas, propositions, and theorems on minimax regret of e-processes are formalized in Lean with Mathlib, aided by Claude; formalization exposed a gap.
Abstract
Log-optimal e-variables at fixed horizons, also called numéraires, have been conjectured to “almost” form an e-process for exponential-family null hypotheses. A related open question is whether an e-process can attain the optimal e-power at every horizon up to a bounded loss. Given a final horizon, we study the minimax regret of e-processes relative to the numéraires at all times up to it. For the Gaussian location null and the composite alternative of Gaussian distributions with a smaller variance and an unknown location, we show that the minimax regret in the worst case over the location grows like the iterated logarithm of the final horizon. A single e-process attains this rate at every horizon. This growth answers the question negatively. It also refutes the conjecture if “almost” means a regret bounded uniformly over horizons. For this Gaussian location problem, we thus exhibit the frontier precisely: the minimax regret is bounded if and only if the alternatives have at least the variance of the null.
Problem
Log-optimal fixed-horizon e-variables (numéraires) have been conjectured to almost form an e-process for exponential-family nulls. A related open question is whether some e-process attains optimal e-power at every horizon up to a bounded loss.
Approach
The paper studies the minimax regret of e-processes relative to numéraires at all horizons up to a final horizon. It derives a lower bound by duality with mixtures of stopped null distributions, building on Koolen and Grünwald. It then analyzes the Gaussian location null against Gaussian alternatives with smaller variance and unknown location. All results are formalized in Lean with Mathlib, with assistance from Claude.
Results
In the worst case over location, the minimax regret grows like the iterated logarithm of the final horizon, and a single e-process attains this rate at every horizon. This answers the open question negatively and refutes the conjecture under uniformly bounded regret. Regret is bounded if and only if the alternative variance is at least the null variance.
