The results of the paper

Each numbered result of the paper An iterated-logarithm price of anytime validity for log-optimal e-processes and of its supplementary material, and each mathematical claim of their running text, is stated here as a proposition def <label> : Prop, in the order of the paper and then of the supplement. A result is named after its label in the LaTeX source, with : and - replaced by _. A claim of the running text is named after its section (intro_…, sec2_…, …, sec5_… for the main text, sec_… for the supplement) and after its content. The docstring of each statement quotes the paper, with the number and the label of the result, and lists the conventions of the formalization. A statement is proved by a theorem <label>_holds : <label>.

Conventions:

• The observations take values in a measurable space 𝒳 : Type u, and a path is x : ℕ → 𝒳, whose coordinate x i is the observation X_{i+1}. The null 𝒫 of the paper is written 𝔓, since 𝒫 is the notation of Mathlib for the power set.
• The setting of Sections 1 and 2 (Setting 𝔓 Q Es) collects the hypotheses of the paper: the null distributions and the alternative Q are probability measures, Es t = E*_t is a numéraire at every horizon t, in versions fixed once and for all (Section 2), and the standing assumption sup_{E ∈ ℰ_t} E_Q(log E) < ∞ holds.
• In Section 4 and in the Gaussian results of the supplement, 𝒳 = ℝ, the null is gaussNull, and the alternative is mixAlt s ρ with s > 0, ρ ≥ 0, and ρ² ≥ 1 − s², unless a statement says otherwise (Lemmas S4 to S6 and Proposition S5 take every ρ > 0). The numéraires of Q are taken in the versions E*_t = ∏_{i=2}^t ℓ(Y_i) of Proposition 2 (gaussNumeraire s t). The regrets R^μ_t with Q_μ in place of Q use any numéraires Esμ μ t of Q_μ, which are unique up to Q_μ-null sets.
• Regrets, e-powers, and minimax regrets take values in [−∞, ∞] (EReal), and η_T in [0, ∞]. The logarithm of η_T is ENNReal.log, with log ∞ = ∞. A ratio such as Γ_T/log log T is the quotient in EReal, so that a limit statement also states that the numerator is eventually finite.
• A sum ∑_t ξ_t R_t(E_t) is taken in EReal, where 0 × ∞ = 0, the convention of Lemma 1.
• Stopping times take values in {0, 1, …} ∪ {∞} (ℕ∞), and E_τ = valueAt E τ, with E_∞ = limsup_t E_t.
• The results of the literature that are not in Mathlib enter as hypotheses: PeskirShiryaevTheorem12 (Sections 2 and S4), KoolenGrunwaldTheorem5 (Proposition S1(ii)), LawOfIteratedLogarithm (Section 4.2 and Proposition 4), LarssonRamdasRufTheorem26 (Proposition S5), and ChoeRamdasTheorem2 (Section S3).

Not formalized: the numerical results, values, and computations (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, 'below 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 and of the explanations of Section S1, and the conjectures and open questions of Section 5. The mathematical claims of Example S1 and of Sections S3 and S4 that do not depend on a computation are stated in general form (sec_eta_monotone, sec_adjuster, sec_methods_snell, and sec_methods_mixture).

Section 1: introduction

def LogOptimal.Paper.intro_test_supermartingale : Prop

Test supermartingales are e-processes (Section 1). 'A test (super)martingale with respect to a filtration is a nonnegative process with initial value one that is a (super)martingale with respect to this filtration under every null distribution. Test supermartingales with respect to (ℱ_t) are e-processes.' A test supermartingale takes real values, and the e-process is its image in [0, ∞].

Equations

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

theorem LogOptimal.Paper.intro_test_supermartingale_holds : intro_test_supermartingale

def LogOptimal.Paper.intro_markov : Prop

Rejection at level α (Section 1). 'By Markov's inequality, we can reject the null at level α as soon as an e-process reaches 1/α (Ramdas et al., 2023, Sections 2.5 and 2.6).' The test rejects at the first time t with E_t ≥ 1/α, and the probability that it ever rejects is at most α under every null distribution.

Equations

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

theorem LogOptimal.Paper.intro_markov_holds : intro_markov

def LogOptimal.Paper.intro_simple_null : Prop

A simple null (Section 1). 'For a simple null 𝒫 = {P}, the numéraires E*_t = dQ_t/dP_t form a test martingale with respect to (ℱ_t). Consequently, Γ_T = 0 for every T (Koolen and Grünwald, 2022, Theorem 8).' Under the standing assumption, Q_t is absolutely continuous with respect to P_t, the versions E*_t(x) = (dQ_t/dP_t)(x^t) are numéraires and form a test martingale, and Γ_T = 0 for every choice of numéraires.

Equations

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

theorem LogOptimal.Paper.intro_simple_null_holds : intro_simple_null

def LogOptimal.Paper.intro_growth_rate : Prop

Regrets that differ by o(t) (Section 1). 'Asymptotic growth-rate optimality depends only on the limit of t^{-1} log E_t. Since two e-processes with regrets differing by o(t) have the same limit in expectation, this criterion cannot distinguish a bounded regret from one that grows like log log T.' The statement formalizes the premise of the second sentence; the rest of that sentence interprets it. In the statement, the regrets are finite, and the difference of the e-powers divided by t tends to zero, so that t^{-1}E_Q(log E_t) and t^{-1}E_Q(log E'_t) have the same limit when one of them has a limit.

Equations

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

theorem LogOptimal.Paper.intro_growth_rate_holds : intro_growth_rate

def LogOptimal.Paper.intro_frontier : Prop

The frontier of the Gaussian location problem (Section 1). 'Thus, the minimax regret is bounded if and only if the alternatives have at least the variance of the null.' The minimax regret is the minimax regret in the worst case over the location μ of the composite alternative {N(μ, s²)^{⊗∞} : μ ∈ ℝ}, with the numéraires Esμ μ t of Q_μ, and it is bounded when some C ∈ ℝ bounds it at every T.

Equations

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

theorem LogOptimal.Paper.intro_frontier_holds : intro_frontier

Section 2: setting and basic bounds

def LogOptimal.Paper.sec2_numeraire : Prop

Facts on the numéraire (Section 2). 'The numéraire E*_t of (2) is positive and unique up to Q-null sets (Larsson, Ramdas and Ruf, 2025, Definition 2.1 and Proposition 2.4), and E*_0 = 1 since ℱ_0 is trivial.'

Equations

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

theorem LogOptimal.Paper.sec2_numeraire_holds : sec2_numeraire

def LogOptimal.Paper.sec2_snell : Prop

The Snell envelope (Section 2). 'For P ∈ 𝒫, the Snell envelope of (E*_{t∧T})_{t≥0} under P is the process (Λ^P_t)_{0≤t≤T} defined by Λ^P_T = E*_T, Λ^P_t = max{E*_t, E_P(Λ^P_{t+1} ∣ ℱ_t)} for t < T. It is the smallest supermartingale under P with respect to (ℱ_t) that dominates (E*_{t∧T})_{0≤t≤T} (Peskir and Shiryaev, 2006, Theorem 1.2). Since ℱ_0 is trivial, the same theorem gives Λ^P_0 = sup_τ E_P(E*_{τ∧T}), and hence η_T = sup_{P∈𝒫} Λ^P_0.' The theorem of Peskir and Shiryaev is the hypothesis PeskirShiryaevTheorem12. Since Λ^P_0 is constant, the last two identities hold at every path x.

Equations

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

theorem LogOptimal.Paper.sec2_snell_holds : sec2_snell

def LogOptimal.Paper.prop_basic : Prop

Proposition 1 (prop:basic, Basic bounds). 'Let T ≥ 0. Then Γ_T ≤ Γ_{T+1}. (i) For every t ≥ 0, the process (E_i)_{i≥0} with E_i = E*_t 1(i ≥ t) is an e-process with R_t(E_t) = 0, where 1(·) is the indicator function. (ii) For every ξ ∈ Δ_T, the process (∑_{i=0}^{t∧T} ξ_i E*_i)_{t≥0} is an e-process with regret at most log(1/ξ_t) at every t ≤ T. Consequently, Γ_T ≤ log(T + 1). (iii) If η_T < ∞, then (E*_{t∧T}/η_T)_{t≥0} is an e-process with regret log η_T at every t ≤ T. Hence, Γ_T ≤ log η_T.' log(1/ξ_t) is log((ξ_t)⁻¹) in [0, ∞], infinite when ξ_t = 0. The bound Γ_T ≤ log η_T is stated for every η_T, since it is trivial when η_T = ∞.

Equations

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

theorem LogOptimal.Paper.prop_basic_holds : prop_basic

def LogOptimal.Paper.rem_zero : Prop

Remark 1 (rem:zero). 'If E*_0, …, E*_T have versions such that (E*_{t∧T})_{t≥0} is an e-process, then Γ_T = 0.' A version of E*_t is an ℱ_t-measurable function equal to E*_t Q-almost surely. The other claims of Remark 1 are intro_simple_null, the converse, which is Proposition S1(i), and Example S1, which is not formalized.

Equations

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

theorem LogOptimal.Paper.rem_zero_holds : rem_zero

Section 3: a lower bound by duality

def LogOptimal.Paper.sec3_randomized : Prop

Randomization preserves validity (Section 3). 'By Fubini's theorem, randomization preserves the second inequality in (1), that is, E_P{E_{τ(X,U)}} ≤ 1 for every e-process (E_t), every P ∈ 𝒫, and every randomized stopping time τ.'

Equations

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

theorem LogOptimal.Paper.sec3_randomized_holds : sec3_randomized

def LogOptimal.Paper.sec3_stopped_alternative : Prop

The stopped alternative (Section 3). 'For ξ ∈ Δ_T, let Q^ξ[{t} × B] = ξ_t Q_t(B) for 0 ≤ t ≤ T. In other words, Q^ξ is the distribution of the path of X ∼ Q stopped at an independent time with distribution ξ.' The set {t} × B is the set of the pairs (t, x^t) with x^t ∈ B, for B ∈ ℱ_t, and Q_t(B) = Q(B). The distribution of the independent time is ∑_t ξ_t δ_t on {0, …, T}.

Equations

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

theorem LogOptimal.Paper.sec3_stopped_alternative_holds : sec3_stopped_alternative

def LogOptimal.Paper.sec3_bayes_mixtures : Prop

Bayesian mixtures of stopped null distributions (Section 3). 'The set ℬ contains the Bayesian mixtures of stopped elements of the null of Koolen and Grünwald (2022, Section 3).' These mixtures mix the stopped distributions P^σ of pairs of a null distribution P and a stopping time σ of (ℱ_t), over a probability measure on the pairs. A stopping time is a randomized stopping time that does not depend on u.

Equations

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

theorem LogOptimal.Paper.sec3_bayes_mixtures_holds : sec3_bayes_mixtures

def LogOptimal.Paper.sec3_epower_le_kl : Prop

The e-power is at most the divergence (Section 3). 'More generally, the inequality ∑_t ξ_t E_Q(log E_t) ≤ KL(Q^ξ ‖ P̄) holds for every 𝒳 and every P̄ ∈ ℬ, as we prove in Section S1.'

Equations

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

theorem LogOptimal.Paper.sec3_epower_le_kl_holds : sec3_epower_le_kl

def LogOptimal.Paper.lem_duality : Prop

Lemma 1 (lem:duality, Lower bound by duality). 'Let T ≥ 0. For every e-process (E_t), every ξ ∈ Δ_T, and every P̄ ∈ ℬ, ∑_{t=0}^T ξ_t R_t(E_t) ≥ ∑_{t=0}^T ξ_t E_Q(log E*_t) − KL(Q^ξ ‖ P̄) (5), with the convention 0 × ∞ = 0 in the sums. Consequently, for every ξ ∈ Δ_T, Γ_T ≥ inf_{(E_t)} ∑_{t=0}^T ξ_t R_t(E_t) ≥ ∑_{t=0}^T ξ_t E_Q(log E*_t) − inf_{P̄∈ℬ} KL(Q^ξ ‖ P̄) (6).'

Equations

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

theorem LogOptimal.Paper.lem_duality_holds : lem_duality

def LogOptimal.Paper.rem_deterministic : Prop

Remark 2 (rem:deterministic). 'If every τ_λ is independent of X, then KL(Q^ξ ‖ P̄) ≥ ∑_t ξ_t E_Q(log E*_t), and the right-hand side of (5) is at most zero.' The mixture P̄ ∈ ℬ is given by its components, as in the definition of ℬ, and τ_λ(x, u) does not depend on x.

Equations

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

theorem LogOptimal.Paper.rem_deterministic_holds : rem_deterministic

Section 4.1: numéraires

def LogOptimal.Paper.sec4_worst_case_average : Prop

The worst case over the location is at least the average (Section 4.1). 'For this alternative, we take the regret in the worst case over μ. This worst case is at least the average of the regret under N(0, ρ²).' The average is the integral of the regret over μ ∼ N(0, ρ²), in [−∞, ∞].

Equations

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

theorem LogOptimal.Paper.sec4_worst_case_average_holds : sec4_worst_case_average

def LogOptimal.Paper.prop_numeraire : Prop

Proposition 2 (prop:numeraire, Numéraires of the Gaussian location model). 'For every t ≥ 1, E*_t = ∏_{i=2}^t ℓ(Y_i), P*_t = ∫ P_{θ,t} N{0, ρ² − (1 − s²)/t}(dθ), E_Q(log E*_t) = (t − 1)κ, where κ = KL{N(0, s²) ‖ N(0, 1)} = (s² − 1 − log s²)/2. Under every P_θ, (E*_t)_{t≥0} is a test martingale with respect to (𝒢_t)_{t≥0}.' E*_t = ∏_{i=2}^t ℓ(Y_i) is a numéraire (the first property in (2)) with the third property E*_t = dQ_t/dP*_t. The test martingale is the real-valued product, equal to one for t ≤ 1.

Equations

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

theorem LogOptimal.Paper.prop_numeraire_holds : prop_numeraire

def LogOptimal.Paper.sec4_mixture_mean : Prop

The running mean under P*_t (Section 4.1). 'The following proposition shows that the measure P*_t of (2) is a mixture of null distributions under which X̄_t has the same distribution as under Q_t.' The running mean of x^t ∈ ℝ^t is (∑_i x_i)/t, and its distribution under Q_t is N(0, ρ² + s²/t).

Equations

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

theorem LogOptimal.Paper.sec4_mixture_mean_holds : sec4_mixture_mean

def LogOptimal.Paper.sec4_maximal_invariant : Prop

The numéraire is the likelihood ratio of a maximal invariant (Section 4.1). 'Since the vector Y^t is a maximal invariant under translations x ↦ (x_1 + m, …, x_t + m), the numéraire E*_t is the likelihood ratio of a maximal invariant.' The first conjunct is the maximal invariance: Y^t takes the same value at x and x' exactly when x'^t is a translation of x^t. The second states that E*_t = ∏_{i=2}^t ℓ(Y_i) is the density of the distribution of Y^t under Q with respect to its distribution under P_θ, for every θ, evaluated at Y^t.

Equations

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

theorem LogOptimal.Paper.sec4_maximal_invariant_holds : sec4_maximal_invariant

def LogOptimal.Paper.sec4_conditional_Y2 : Prop

The conditional distribution of Y₂ given X₁ (Section 4.1). 'Under P_θ and given X_1, the variable Y_2 = (X_2 − X_1)/2^{1/2} is normal with mean (θ − X_1)/2^{1/2} and variance 1/2 instead of 1.'

Equations

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

theorem LogOptimal.Paper.sec4_conditional_Y2_holds : sec4_conditional_Y2

def LogOptimal.Paper.sec4_lik : Prop

The likelihood ratio ℓ (Section 4.1). 'For s < 1, ℓ(y) decreases in |y|, and its expectation under N(0, 1) is one.'

Equations

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

theorem LogOptimal.Paper.sec4_lik_holds : sec4_lik

Section 4.2: stopping rules that depend on the null mean

def LogOptimal.Paper.sec4_lik_process : Prop

The likelihood ratio L^θ_t (Section 4.2). 'For θ ∈ ℝ, let L^θ_t = ∏_{i=1}^t ℓ(X_i − θ) be the likelihood ratio of Q_θ against P_θ on ℱ_t, with L^θ_0 = 1. Under P_θ, (L^θ_t)_{t≥0} is a nonnegative martingale with respect to (ℱ_t) with initial value one.'

Equations

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

theorem LogOptimal.Paper.sec4_lik_process_holds : sec4_lik_process

def LogOptimal.Paper.lem_identity : Prop

Lemma 2 (lem:identity, Change of measure). '(i) For every θ ∈ ℝ and every t ≥ 1, E*_t = s L^θ_t exp{(1 − s²)t(X̄_t − θ)²/(2s²)}. (ii) Let (S_t)_{t≥0} be a random walk with S_0 = 0 and independent N(0, 1) increments, and let h_0 = 1 and h_t = s exp{(1 − s²)S_t²/(2t)} for t ≥ 1. For every T ≥ 0, η_T = sup_τ E(h_{τ∧T}), where τ ranges over the stopping times of the filtration generated by (S_t).' The random walk is realized on the space of its increments, with distribution N(0, 1)^{⊗∞}.

Equations

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

theorem LogOptimal.Paper.lem_identity_holds : lem_identity

def LogOptimal.Paper.sec4_lil : Prop

The law of the iterated logarithm for the reward (Section 4.2). 'If s < 1, the reward h_t is large when |S_t| is large compared with t^{1/2}, and the law of the iterated logarithm gives limsup_{t→∞} log h_t / log log t = 1 − s² almost surely.' The law of the iterated logarithm is the hypothesis LawOfIteratedLogarithm.

Equations

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

theorem LogOptimal.Paper.sec4_lil_holds : sec4_lil

Section 4.3: the iterated-logarithm rate

def LogOptimal.Paper.prop_mixture : Prop

Proposition 3 (prop:mixture, Iterated-logarithm rate for the mixture). 'Let s ∈ (0, 1) and ρ² ≥ 1 − s². (i) As T → ∞, Γ_T/log log T → 1 − s² and log η_T/log log T → 1 − s². (ii) For j ≥ 1, let T_j = ⌈exp(e^j)⌉ and q_j = 1 + s²/{(1 − s²)(j + 1)}. The process (E_t)_{t≥0} with E_t = ∑_{j=1}^∞ E*_{t∧T_j}/{j(j + 1)u_j}, u_j = {(j + 1)/(s² j)}(2 + 2 log T_j/log q_j)^{1 − s² j/(j + 1)}, is an e-process with limsup_{t→∞} R_t(E_t)/log log t = 1 − s².'

Equations

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

theorem LogOptimal.Paper.prop_mixture_holds : prop_mixture

def LogOptimal.Paper.sec4_every_rho : Prop

Proposition 3(i) for every ρ > 0 (Section 4.3). 'Proposition 3(i) holds for every ρ > 0 (Proposition S5).' For ρ² < 1 − s², Γ_T and η_T are defined with any numéraires Es t of Q, which differ from ∏_{i=2}^t ℓ(Y_i) at the first horizons; Proposition S5 gives both limits.

Equations

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

theorem LogOptimal.Paper.sec4_every_rho_holds : sec4_every_rho

def LogOptimal.Paper.sec4_single_horizon : Prop

The minimax regret at a single horizon (Section 4.3). 'For s < 1 and a single horizon t ≥ 1, the numéraire E*_t attains the minimax regret κ in the worst case over μ (see the proof of Theorem 1).' The minimax regret at the horizon t is inf_{E ∈ ℰ_t} sup_μ R^μ_t(E).

Equations

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

theorem LogOptimal.Paper.sec4_single_horizon_holds : sec4_single_horizon

def LogOptimal.Paper.thm_composite : Prop

Theorem 1 (thm:composite, Composite alternative). 'Let s ∈ (0, 1) and ρ² ≥ 1 − s². For μ ∈ ℝ, let R^μ_t be the regret defined by (2) and (3) with Q_μ in place of Q. (i) For T ≥ 1, κ + Γ_T ≤ inf_{(E_t)} max_{0≤t≤T} sup_{μ∈ℝ} R^μ_t(E_t) ≤ κ + log η_T. The middle term divided by log log T therefore tends to 1 − s² as T → ∞. (ii) The e-process (E_t) of Proposition 3(ii) satisfies sup_{μ∈ℝ} R^μ_t(E_t) = κ + R_t(E_t) for t ≥ 1, so that limsup_{t→∞} sup_{μ∈ℝ} R^μ_t(E_t)/log log t = 1 − s².'

Equations

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

theorem LogOptimal.Paper.thm_composite_holds : thm_composite

def LogOptimal.Paper.sec4_growth : Prop

The growth of the minimax regret (Section 4.3). 'Theorem 1 shows that the minimax regret in the worst case over μ is unbounded. It grows more slowly than any power of log T, while the optimal e-power Tκ of each Q_μ grows linearly.' The optimal e-power of Q_μ is Proposition S4(i).

Equations

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

theorem LogOptimal.Paper.sec4_growth_holds : sec4_growth

def LogOptimal.Paper.prop_sge1 : Prop

Proposition 4 (prop:sge1, The case s ≥ 1). 'If s ≥ 1, then Γ_T ≤ log η_T ≤ log s for every T ≥ 0, and log η_T → log s as T → ∞.' The limit uses the law of the iterated logarithm (LawOfIteratedLogarithm), from which the proof deduces that the random walk changes sign infinitely often. The condition ρ² ≥ 1 − s² holds for every ρ ≥ 0.

Equations

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

theorem LogOptimal.Paper.prop_sge1_holds : prop_sge1

def LogOptimal.Paper.sec4_sge1_worst_case : Prop

The case s ≥ 1 in the worst case over the location (Section 4.3). 'For s ≥ 1, the minimax regret is also bounded in the worst case over μ. Indeed, the numéraire ∏_{i=2}^t ℓ(Y_i) of Proposition 2 is then also the numéraire of every Q_μ (Proposition S4). The e-process of Proposition 1(iii) therefore has regret at most log s against every Q_μ.'

Equations

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

theorem LogOptimal.Paper.sec4_sge1_worst_case_holds : sec4_sge1_worst_case

Section 5: discussion

def LogOptimal.Paper.sec5_kappa : Prop

The number of observations for s close to one (Section 5). 'For s close to one, κ ≈ (1 − s²)²/4, so that this number grows like 4 log log T/(1 − s²).' The approximation is κ/{(1 − s²)²/4} → 1 as s → 1. The number of observations log η_T/κ, asymptotically (1 − s²) log log T/κ by Proposition 3(i), then grows like 4 log log T/(1 − s²).

Equations

• LogOptimal.Paper.sec5_kappa = Filter.Tendsto (fun (s : ℝ) => LogOptimal.kappa s / ((1 - s ^ 2) ^ 2 / 4)) (nhdsWithin 1 {1}ᶜ) (nhds 1)

theorem LogOptimal.Paper.sec5_kappa_holds : sec5_kappa

def LogOptimal.Paper.sec5_upper_bound : Prop

An upper bound on η_T may replace η_T (Section 5). 'The e-process is the conditional e-variable of Hao and Grünwald divided by η_T and stopped at T, and an upper bound on η_T, from Table S2 or Lemma S3, may replace η_T.' The statement is the general fact: for every finite u ≥ η_T, (E*_{t∧T}/u)_{t≥0} is an e-process with regret log u at every t ≤ T.

Equations

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

theorem LogOptimal.Paper.sec5_upper_bound_holds : sec5_upper_bound

def LogOptimal.Paper.sec5_threshold_test : Prop

Threshold tests keep their level (Section 5). 'In contrast, the test that rejects the null as soon as the conditional e-variables reach 1/α has level α … Indeed, these e-variables form a test martingale with respect to the filtration (𝒢_t). By Ville's inequality, the probability that they ever reach 1/α is at most α under every null distribution.'

Equations

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

theorem LogOptimal.Paper.sec5_threshold_test_holds : sec5_threshold_test

Section S1: proofs

def LogOptimal.Paper.lem_regret : Prop

Lemma S1 (lem:regret, Integrability of the numéraire). 'For every t ≥ 0, log E*_t is Q-integrable and satisfies the second identity in (2). For every E ∈ ℰ_t, the regret R_t(E) in (3) is well defined, and R_t(E) = E_Q(log E*_t) − E_Q(log E) ∈ [0, ∞].' 'Well defined' is the integrability of the negative part of log(E*_t/E).

Equations

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

theorem LogOptimal.Paper.lem_regret_holds : lem_regret

def LogOptimal.Paper.lem_orth : Prop

Lemma S2 (lem:orth, Orthogonal transformation). 'Let t ≥ 2, x ∈ ℝ^t, x̄_i = i^{-1} ∑_{j=1}^i x_j for 1 ≤ i ≤ t, and y_i = {(i − 1)/i}^{1/2}(x_i − x̄_{i−1}) for 2 ≤ i ≤ t. (i) The map x ↦ (t^{1/2} x̄_t, y_2, …, y_t) is orthogonal. Moreover, the values y_2, …, y_t do not change when the same constant is added to every x_i. Hence, ∑_{i=1}^t (x_i − m)² = t(x̄_t − m)² + ∑_{i=2}^t y_i² for every m ∈ ℝ. (ii) x̄_t = x̄_{t−1} + y_t/{t(t − 1)}^{1/2}. (iii) If X^t ∼ N(m, v)^{⊗t}, then X̄_t, Y_2, …, Y_t are independent, with X̄_t ∼ N(m, v/t) and Y_i ∼ N(0, v).' The vector x ∈ ℝ^t is the first t coordinates of a path. The map of (i) is linear, and it is orthogonal because it preserves the Euclidean norm. In (iii), X^t is the beginning of a path with distribution N(m, v)^{⊗∞}, and the family (X̄_t, Y_2, …, Y_t) is indexed by Fin t.

Equations

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

theorem LogOptimal.Paper.lem_orth_holds : lem_orth

def LogOptimal.Paper.eq_S_gauss : Prop

Equation (S1) (eq:S-gauss) and the logarithm of ℓ (Section S1.1). 'In the model of Section 4, with b = s^{-2} − 1, the likelihood ratio ℓ satisfies log ℓ(y) = −log s − by²/2. For m ∈ ℝ, v ≥ 0 with 1 + bv > 0, and Z ∼ N(0, 1), completing the square gives E{ℓ(m + v^{1/2}Z)} = {s(1 + bv)^{1/2}}^{-1} exp{−bm²/(2 + 2bv)} (S1). Since s(1 + b)^{1/2} = 1 and b/(1 + b) = 1 − s², the right-hand side of (S1) equals exp{−(1 − s²)m²/2} for v = 1.'

Equations

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

theorem LogOptimal.Paper.eq_S_gauss_holds : eq_S_gauss

def LogOptimal.Paper.eq_S_factor : Prop

Equation (S2) (eq:S-factor). 'By Lemma S2(i), for x ∈ ℝ^t, every m ∈ ℝ, and every v > 0, ∏_{i=1}^t φ_v(x_i − m) = t^{-1/2} φ_{v/t}(x̄_t − m) ∏_{i=2}^t φ_v(y_i).'

Equations

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

theorem LogOptimal.Paper.eq_S_factor_holds : eq_S_factor

def LogOptimal.Paper.lem_upper : Prop

Lemma S3 (lem:upper, Upper bound on η_T). 'Let s ∈ (0, 1), a = 1 − s², T ≥ 1, and q ∈ (1, 1/a). Then log η_T ≤ aq log(2 + 2 log T/log q) + log{1/(1 − aq)}.'

Equations

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

theorem LogOptimal.Paper.lem_upper_holds : lem_upper

def LogOptimal.Paper.lem_lbmix : Prop

Lemma S4 (lem:lbmix, Mixture of stopped null distributions). 'For the lower bound, let s ∈ (0, 1) and ρ² ≥ 1 − s², as in Proposition 3, and fix integers r ≥ 4 and K ≥ 1, a horizon T ≥ r^K, and a constant c > 0. … The distribution P̄ belongs to ℬ, and Γ_T ≥ (K + 1)^{-1} ∑_{k=0}^K E_Q[log{(K + 1)J_k}] (S8).' The proof of Proposition S5 adds that 'the proof of Lemma S4 holds with Π_{t_k} in place of E*_{t_k}, for every ρ > 0', where Π_t = ∏_{i=2}^t ℓ(Y_i), and that Lemma 1 then still gives (S8). The statement is therefore for every ρ > 0 and any numéraires Es t of Q; for ρ² ≥ 1 − s², these include the numéraires ∏_{i=2}^t ℓ(Y_i) of Proposition 2. P̄ is lbMixture s ρ r K c, J_k is lbJ s ρ r K c k, and the expectation is taken in [−∞, ∞].

Equations

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

theorem LogOptimal.Paper.lem_lbmix_holds : lem_lbmix

def LogOptimal.Paper.lem_jk : Prop

Lemma S5 (lem:jk, Lower bounds on J_k). 'Let 0 ≤ k ≤ K and t = t_k, let β' = ½ log{ρ²/(γ² + 1)} − log 2, and let p_k(y) = ∫_{𝒵_k(y)} φ_1(z) dz. (i) For every x ∈ ℝ^t, log{(K + 1)J_k(x)} ≥ β'. (ii) For every x ∈ ℝ^t, J_k(x) ≥ {ρ/(2γ)} exp[−{2(c + 1)t^{-1/2}|x̄_t| + (c + 1)²t^{-1}}/(2γ²)] p_k(y). (iii) Let c' = c − (c + 1)r^{-1/2}, assume that c' > 0, and let A_k = {y : max_{j<k} |W_{jk}(y)| < c'}. Then p_k(y) ≥ 2φ_1(c + 1) for every y ∈ A_k.' The setting is that of Lemma S4, with γ = (ρ² + s²)^{1/2}, for every ρ > 0, since the proof of Proposition S5 states that Lemma S5 uses 'only ρ > 0 and (S8)'. Part (i) also states that J_k > 0, so that its logarithm is that of the paper.

Equations

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

theorem LogOptimal.Paper.lem_jk_holds : lem_jk

def LogOptimal.Paper.sec_lb_stopping : Prop

The stopping rule of the lower bound (Section S1.6, after Lemma S5). 'Since Z_t ∼ N(0, 1) is independent of Y^t under P_θ, p_k(Y^t) is the conditional probability that τ' = t, given Y^t. The proof of part (iii) shows that, on the event {Y^t ∈ A_k}, the rule τ' stops at t whenever c ≤ |Z_t| ≤ c + 1.' Here t = t_k = r^k, Z_t = t^{1/2}(X̄_t − θ) (lbZ), and Y^t generates the σ-algebra MeasurableSpace.comap (helmertVec t); part (iii) of Lemma S5 assumes c' > 0.

Equations

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

theorem LogOptimal.Paper.sec_lb_stopping_holds : sec_lb_stopping

def LogOptimal.Paper.lem_fixedk : Prop

Lemma S6 (lem:fixedk, Lower bound for fixed K). 'Let c', A_k, and β' be as in Lemma S5, and let β = log(K + 1) + log φ_1(c + 1) + log(ρ/γ). If c' > 0 and β ≥ β', then Γ_T ≥ β − (β − β')K exp{−c'²/(2s²)} − {2(c + 1)/γ + 2(c + 1)²/(3γ²)}/(K + 1) (S9).' The setting is that of Lemma S4, with γ = (ρ² + s²)^{1/2}, for every ρ > 0 and any numéraires Es t of Q, since the proof of Proposition S5 states that Lemma S6 uses 'only ρ > 0 and (S8)'.

Equations

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

theorem LogOptimal.Paper.lem_fixedk_holds : lem_fixedk

Section S2: additional results

def LogOptimal.Paper.prop_minimax : Prop

Proposition S1 (prop:minimax). 'Let T ≥ 0. (i) Suppose that Γ_T = 0, and that 𝒳 is finite or P_T is absolutely continuous with respect to Q_T for every P ∈ 𝒫. Then E*_0, …, E*_T have versions such that (E*_{t∧T})_{t≥0} is an e-process. (ii) On every sample space 𝒳, Γ_T = max_{ξ∈Δ_T} inf_{(E_t)} ∑_{t=0}^T ξ_t R_t(E_t). (iii) If 𝒳 is finite, then, for every ξ ∈ Δ_T, inf_{(E_t)} ∑_{t=0}^T ξ_t R_t(E_t) = ∑_{t=0}^T ξ_t E_Q(log E*_t) − inf_{P̄∈ℬ} KL(Q^ξ ‖ P̄) (S11).' A finite 𝒳 carries the discrete σ-algebra. The maximum of (ii) is attained at some ξ ∈ Δ_T, and part (iii) uses the hypothesis KoolenGrunwaldTheorem5.

Equations

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

theorem LogOptimal.Paper.prop_minimax_holds : prop_minimax

def LogOptimal.Paper.sec_finite_disjoint : Prop

Disjoint supports (Section S2.1). 'On this space, the stopped null distributions P^τ form the null, and the distributions Q^ξ with ξ a unit mass form the alternatives. … Moreover, these alternatives have disjoint supports.'

Equations

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

theorem LogOptimal.Paper.sec_finite_disjoint_holds : sec_finite_disjoint

def LogOptimal.Paper.sec_finite_bounded : Prop

Bounded e-processes on finite sample spaces (Section S2.1). 'On a finite 𝒳, the e-processes stopped at T may be taken bounded.' For a finite 𝒳, Γ_T is the infimum of max_{t≤T} R_t(E_t) over the bounded e-processes (E_t) stopped at T.

Equations

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

theorem LogOptimal.Paper.sec_finite_bounded_holds : sec_finite_bounded

def LogOptimal.Paper.sec_eta_monotone : Prop

Monotonicity of η_T (Example S1). 'Since τ ∧ T is a stopping time, η_T is nondecreasing in T.' Example S1 states this fact for the Bernoulli model; it holds for every null and every numéraire.

Equations

• LogOptimal.Paper.sec_eta_monotone = ∀ (𝒳 : Type ?u.1) [inst : MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Es : ℕ → (ℕ → 𝒳) → ENNReal), Monotone (LogOptimal.eta 𝔓 Es)

theorem LogOptimal.Paper.sec_eta_monotone_holds : sec_eta_monotone

def LogOptimal.Paper.eq_S_epower : Prop

Equation (S14) (eq:S-epower, Section S2.2). 'For every ξ ∈ Δ_T, Lemma S1 gives sup_{(E_t)} ∑_{t=0}^T ξ_t E_Q(log E_t) = ∑_{t=0}^T ξ_t E_Q(log E*_t) − inf_{(E_t)} ∑_{t=0}^T ξ_t R_t(E_t).'

Equations

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

theorem LogOptimal.Paper.eq_S_epower_holds : eq_S_epower

def LogOptimal.Paper.prop_notep : Prop

Proposition S2 (prop:notep). 'For every θ ∈ ℝ and every s ≠ 1, E_θ(E*_2 ∣ X_1) = {2/(1 + s²)}^{1/2} exp{−(1 − s²)(X_1 − θ)²/(2 + 2s²)} (S15), sup_{τ≤2} E_θ(E*_τ) = E_θ[max{1, E_θ(E*_2 ∣ X_1)}] > 1 (S16), where the supremum runs over the stopping times of (ℱ_t) bounded by 2.' The conditional expectation given X_1 is given ℱ_1. Section S2.3 says that the proposition gives 'the best stopping time up to t = 2': the rule τ = 1 + 1{E_θ(E*_2 ∣ X_1) > 1}, a stopping time bounded by 2, attains the supremum in (S16).

Equations

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

theorem LogOptimal.Paper.prop_notep_holds : prop_notep

def LogOptimal.Paper.sec_notep : Prop

Consequences of Proposition S2 (Section S2.3 and Section 4.1). 'The conditional expectation E_θ(E*_2 ∣ X_1) exceeds one when (X_1 − θ)² < {(1 + s²)/(1 − s²)} log{2/(1 + s²)} if s < 1, and when the reverse strict inequality holds if s > 1. … Since the supremum in (S16) exceeds one, the numéraires are not an e-process with respect to (ℱ_t) for s ≠ 1. … Moreover, the null distributions of X^2 are absolutely continuous with respect to Q_2. For s ≠ 1, Proposition S1(i) and (S16) therefore give Γ_2 > 0, and Proposition 1 gives Γ_T ≥ Γ_2 > 0 for every T ≥ 2. In particular, the minimax regret is positive for s > 1, although Proposition 4 bounds it by log s.'

Equations

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

theorem LogOptimal.Paper.sec_notep_holds : sec_notep

def LogOptimal.Paper.eq_enlarge : Prop

Equation (S17) (eq:enlarge, Section S2.4). 'It follows from Lemma S2 that X^t and (X_1, Y_2, …, Y_t) are functions of each other in the Gaussian location model. Therefore, for t ≥ 1, ℱ_t = 𝒢_t ∨ σ(X_1) (S17).'

Equations

• LogOptimal.Paper.eq_enlarge = ∀ (t : ℕ), 1 ≤ t → ↑(LogOptimal.dataFiltration ℝ) t = ↑LogOptimal.helmertFiltration t ⊔ MeasurableSpace.comap (fun (x : ℕ → ℝ) => x 0) inferInstance

theorem LogOptimal.Paper.eq_enlarge_holds : eq_enlarge

def LogOptimal.Paper.prop_enlarge : Prop

Proposition S3 (prop:enlarge). '(i) For every θ ∈ ℝ, X_1 = θ − ∑_{i≥2} Y_i/{i(i − 1)}^{1/2} almost surely under P_θ. (ii) Let θ ∈ ℝ and t ≥ 1. Under P_θ, the conditional distribution of X_1 given 𝒢_t is N[θ − ∑_{i=2}^t Y_i/{i(i − 1)}^{1/2}, 1/t], and I(X_1; Y^t) = ½ log t. (iii) Let (E_t) be a process with values in [0, ∞] that is adapted to (𝒢_t). Then sup_τ E_θ(E_τ) is the same for every θ ∈ ℝ, where τ ranges over the stopping times of (ℱ_t). In particular, (E_t) is an e-process for 𝒫 if and only if it is an e-process for {P_θ} for some θ ∈ ℝ.' The series of (i) converges as the limit of its partial sums. In (ii), the conditional distribution given 𝒢_t is the conditional distribution given Y^t, whose i-th coordinate is Y_{i+2}.

Equations

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

theorem LogOptimal.Paper.prop_enlarge_holds : prop_enlarge

def LogOptimal.Paper.sec_enlarge_suprema : Prop

The two suprema of the stopped numéraires (Section S2.4). 'By Propositions 2 and S3(iii), for every θ ∈ ℝ, sup_τ E_θ(E*_{τ∧T}) equals 1 when τ ranges over the stopping times of (𝒢_t) and equals η_T when τ ranges over the stopping times of (ℱ_t).'

Equations

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

theorem LogOptimal.Paper.sec_enlarge_suprema_holds : sec_enlarge_suprema

def LogOptimal.Paper.prop_simple : Prop

Proposition S4 (prop:simple). 'Let s > 0, μ ∈ ℝ, and T ≥ 0, and let Q_μ replace Q in (2) and (3). (i) If s ≤ 1, then E*_t = ∏_{i=1}^t ℓ(X_i − μ) and E_{Q_μ}(log E*_t) = tκ for t ≥ 0. The process (E*_t)_{t≥0} is a test supermartingale with respect to (ℱ_t). Hence, Γ_T = 0. (ii) If s > 1, then E*_t = ∏_{i=2}^t ℓ(Y_i) for t ≥ 1, as in Proposition 2. Consequently, Γ_T ≤ log η_T ≤ log s, where η_T is the quantity (4) of Section 4.' Γ_T is the minimax regret for Q_μ, with the numéraires of (i) or (ii).

Equations

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

theorem LogOptimal.Paper.prop_simple_holds : prop_simple

def LogOptimal.Paper.sec_simple : Prop

The measure P*_t of a simple alternative and the mixing variance (Section S2.5). 'For s ≤ 1, the measure P*_t in (2) is the single null distribution P_{μ,t} at every horizon t. … This mixing variance is nonnegative at every horizon t ≥ 1 if and only if ρ² ≥ 1 − s², the condition of Section 4. With ρ = 0, the alternative of Section 4 is Q_μ with μ = 0. This condition then reduces to s ≥ 1.'

Equations

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

theorem LogOptimal.Paper.sec_simple_holds : sec_simple

def LogOptimal.Paper.prop_smallrho : Prop

Proposition S5 (prop:smallrho). 'Let s ∈ (0, 1) and ρ > 0, and let Q = ∫ Q_μ N(0, ρ²)(dμ) as in Section 4, without the condition ρ² ≥ 1 − s². Then Γ_T/log log T → 1 − s² and log η_T/log log T → 1 − s² as T → ∞.' The numéraires Es t of Q are any numéraires; they are not explicit at the first horizons when ρ² < 1 − s². They exist by Larsson, Ramdas and Ruf (2025, Theorem 2.6), the hypothesis of the first conjunct, so that the second is not vacuous.

Equations

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

theorem LogOptimal.Paper.prop_smallrho_holds : prop_smallrho

def LogOptimal.Paper.sec_frontier : Prop

When the minimax regret tends to infinity (Section S2.5). 'With ρ = 0, in contrast, Proposition S4(i) gives Γ_T = 0 for every T. Among the alternatives Q_μ and their mixtures over the location, Γ_T tends to infinity exactly for the mixtures with s < 1 and ρ > 0, however small ρ is.' The first conjunct treats the alternatives Q_μ, the second the mixtures Q with ρ ≥ 0, which are Q_μ with μ = 0 when ρ = 0.

Equations

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

theorem LogOptimal.Paper.sec_frontier_holds : sec_frontier

def LogOptimal.Paper.prop_plugin : Prop

Proposition S6 (prop:plugin). 'Let s < 1. The process (Ẽ_t)_{t≥0} with Ẽ_t = ∏_{i=2}^t ℓ(X_i − X̄_{i−1}) is a test supermartingale with respect to (ℱ_t) under every P_θ, and, for t ≥ 1 and T ≥ 1, R_t(Ẽ_t) = {(1 − s²)/2} ∑_{i=1}^{t−1} i^{-1}, Γ_T ≤ {(1 − s²)/2}(1 + log T). For every μ and t ≥ 1, moreover, R^μ_t(Ẽ_t) = κ + R_t(Ẽ_t), with R^μ_t as in Theorem 1.'

Equations

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

theorem LogOptimal.Paper.prop_plugin_holds : prop_plugin

Sections S3 and S4: numerical results and methods

def LogOptimal.Paper.sec_adjuster : Prop

The adjuster (Section S3). 'Since the numéraires form a test martingale with respect to (𝒢_t), we apply the adjuster A(e) = (e − 1 − log e)/(log e)² of Choe and Ramdas (2026, Section 2.3) to their running maximum and obtain an e-process with respect to (ℱ_t).' The adjuster is adjusterMix, with A(1) = 1/2 (Section S4), and the e-lifting theorem of Choe and Ramdas is the hypothesis ChoeRamdasTheorem2.

Equations

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

theorem LogOptimal.Paper.sec_adjuster_holds : sec_adjuster

def LogOptimal.Paper.sec_methods_snell : Prop

E-processes stopped at T and dominating supermartingales (Section S4). 'For each null parameter θ, we define the Snell envelope of a process (E_t) adapted to (ℱ_t) … by the recursion of Section 2, with (E_t) in place of (E*_t). As in Section 2, it is the smallest θ-supermartingale that dominates (E_t) on the binary tree of depth T (Peskir and Shiryaev, 2006, Theorem 1.2). Therefore, (E_t) is an e-process for the five null distributions if and only if, for each θ, some θ-supermartingale (Ψ^θ_t) with Ψ^θ_t ≥ E_t on the tree has initial value Ψ^θ_0 ≤ 1.' The statement holds for every 𝒳 and every null, for a process with finite values stopped at T, as in the proof of Proposition S1(i); the supermartingale property is required up to T.

Equations

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

theorem LogOptimal.Paper.sec_methods_snell_holds : sec_methods_snell

def LogOptimal.Paper.sec_methods_mixture : Prop

A density against a mixture of null distributions (Section S4). 'Since P*_t is also a mixture of null distributions, it is the measure in (2).' In Section S4, P*_t is a mixture of null distributions of X^t, and dQ_t/dP*_t is an e-variable. The statement is the general fact behind this sentence, which the proof of Proposition 2 also uses: an e-variable E = dQ_t/dP*_t, with P*_t a mixture of null distributions of X^t, is the numéraire, and P*_t is the measure in (2). The mixture is given by a probability measure π and a kernel κ into the null, as in the definition of ℬ.

Equations

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

theorem LogOptimal.Paper.sec_methods_mixture_holds : sec_methods_mixture