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

The results of the paper An iterated-logarithm price of anytime validity for log-optimal e-processes by Adrien Corenflos, and of its supplementary material, are formalized in Lean 4 with Mathlib. Every result is proved, and depends only on the axioms propext, Classical.choice, and Quot.sound. The results of the literature that are not in Mathlib enter as hypotheses of the statements.

• Blueprint: the statements of the paper, each with its Lean statement and proof.
• Dependency graph of the blueprint.
• API documentation of the Lean code, shared with the other formalizations of this site.