Results of the literature

The results of the literature on which the paper relies, and which are not in Mathlib, enter the statements of LogOptimalEProcesses.Paper as hypotheses, never as axioms. Each is a proposition def … : Prop, stated as in its source or as the consequence of it that the paper uses.

• PeskirShiryaevTheorem12: the finite-horizon optimal stopping theorem of Peskir and Shiryaev (2006, Theorem 1.2), for nonnegative rewards, used for the Snell envelope of Section 2.
• KoolenGrunwaldTheorem5: the primal-dual equivalence of Koolen and Grünwald (2022, Theorem 5) for a finite outcome space, applied to a data-independent stopping time, in the form used in the proof of Proposition S1(ii).
• LawOfIteratedLogarithm: the law of the iterated logarithm for the Gaussian random walk, used after Lemma 2 and in the proof of Proposition 4.
• LarssonRamdasRufTheorem26: the existence of a numéraire for every null and every alternative (Larsson, Ramdas and Ruf, 2025, Theorem 2.6), cited in Section 1; it shows that the statements on the numéraires of the mixtures with ρ² < 1 − s² are not vacuous (Proposition S5).
• ChoeRamdasTheorem2: the e-lifting theorem of Choe and Ramdas (2026, Theorem 2) with their adjuster A(e) = (e − 1 − log e)/(log e)² (adjusterMix), used in Section S3.

The other results of the literature that the paper uses are in Mathlib (Sion's minimax theorem, Doob's maximal inequality, the strong law of large numbers, Fubini's theorem, Fatou's lemma, and Jensen's inequality) or are proved in this library (the uniqueness of the log-optimal e-variable of Larsson, Ramdas and Ruf, 2025, Proposition 2.4, the inequality of the Donsker–Varadhan variational formula, and Ville's inequality).

def LogOptimal.PeskirShiryaevTheorem12 : Prop

Peskir and Shiryaev (2006, Theorem 1.2), finite horizon, for nonnegative rewards. Let (Ω, ℱ, P) be a filtered probability space and (G_n)_{0 ≤ n ≤ N} a nonnegative adapted process with E_P(G_n) < ∞, so that E_P(sup_{n ≤ N} |G_n|) < ∞. The Snell envelope S defined by backward induction (snell) dominates G, is a supermartingale under P, is dominated by every supermartingale that dominates G (its eq. (1.1.13)), and satisfies E_P(S_0) = sup_τ E_P(G_{τ ∧ N}) over the stopping times τ of ℱ (its eqs. (1.1.9) and (1.1.10) at n = 0).

Equations

• One or more equations did not get rendered due to their size.

def LogOptimal.KoolenGrunwaldTheorem5 : Prop

Koolen and Grünwald (2022, Theorem 5), in the form used in the proof of Proposition S1(ii). For a finite outcome space 𝒳, a finite horizon T, any null 𝔓, and an alternative Q, their theorem, applied to a data-independent stopping time with distribution ξ ∈ Δ_T, gives sup_{(E_t)} ∑_t ξ_t E_Q(log E_t) = inf_{P̄} KL(Q^ξ ‖ P̄) over their Bayesian mixtures P̄ of stopped null distributions. These mixtures belong to ℬ (Section 3), so that the supremum is at least the infimum of KL(Q^ξ ‖ P̄) over P̄ ∈ ℬ.

Equations

• One or more equations did not get rendered due to their size.

def LogOptimal.LawOfIteratedLogarithm : Prop

The law of the iterated logarithm (Khinchine) for the random walk (S_t) with S₀ = 0 and independent N(0, 1) increments: almost surely, limsup_{t → ∞} S_t/(2t log log t)^{1/2} = 1 and liminf_{t → ∞} S_t/(2t log log t)^{1/2} = −1. The limits are taken in [−∞, ∞].

Equations

• One or more equations did not get rendered due to their size.

def LogOptimal.LarssonRamdasRufTheorem26 : Prop

Larsson, Ramdas and Ruf (2025, Theorem 2.6): 'A numeraire exists', for every nonempty null of probability measures and every alternative, with no further assumption. Applied on the σ-algebra ℱ_t, it gives a numéraire at every horizon t. Their definition takes ∞/∞ = 1, while ENNReal takes ∞/∞ = 0, so that their numéraire satisfies IsNumeraire.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LogOptimal.adjusterMix (e : ℝ) : ℝ

The adjuster A(e) = (e − 1 − log e)/(log e)² for e > 1, with A(1) = 1/2, of Choe and Ramdas (2026, eq. (12)); its values for e < 1 are not used.

Equations

• LogOptimal.adjusterMix e = if e = 1 then 1 / 2 else (e - 1 - Real.log e) / Real.log e ^ 2

def LogOptimal.ChoeRamdasTheorem2 : Prop

Choe and Ramdas (2026, Theorem 2) (e-lifting), with the adjuster adjusterMix of their eq. (12), in the form used in Section S3. A test supermartingale with respect to a filtration 𝒢 coarser than (ℱ_t) is an e-process in 𝒢, and their theorem lifts the adjusted running maximum A(max_{i ≤ t} M_i) to an e-process with respect to (ℱ_t). Their adjusted process takes the value 1 at t = 0, and the value A(1) = 1/2 here is smaller.

Equations

• One or more equations did not get rendered due to their size.