1
Results of the literature
2
The setting
3
A lower bound by duality
4
The Gaussian location model
5
Stopping rules that depend on the null mean
6
The lower bound
7
The iterated-logarithm rate
8
Additional results
9
Formalization notes
▶
9.1
Types and values
9.2
The setting and the statements
9.3
Findings
Dependency graph
An iterated-logarithm price of anytime validity for log-optimal e-processes: Lean formalization
Adrien Corenflos
1
Results of the literature
2
The setting
3
A lower bound by duality
4
The Gaussian location model
5
Stopping rules that depend on the null mean
6
The lower bound
7
The iterated-logarithm rate
8
Additional results
9
Formalization notes
9.1
Types and values
9.2
The setting and the statements
9.3
Findings