The random walk in the proof of Lemma S3

This file proves the bound on the random walk (S_t) of Lemma 2 in the proof of Lemma S3 (Section S1.6 of the supplementary material). The random walk is realized under stdGaussSeq on the space of its increments, and pr denotes probability. Let s ∈ (0, 1), a = 1 − s², q ∈ (1, 1/a), and M = max[1, max_{1 ≤ t ≤ T} exp{aS_t²/(2t)}]. Then h_t ≤ M for 0 ≤ t ≤ T, and E(M) ≤ N'^{aq}/(1 − aq) ≤ exp[aq log(2 + 2 log T/log q) + log{1/(1 − aq)}], where N = 1 + ⌊log T/log q⌋ and N' = 2N ≤ 2 + 2 log T/log q. Together with Lemma 2(ii), which gives η_T = sup_τ E(h_{τ∧T}), these bounds give Lemma S3 (log_le_of_le_iSup_lintegral_reward).

• walkMax s T: the maximum M, as a function of the increments of the random walk;
• walkBlock q T k: the block B_k = {t ≤ T : q^k ≤ t < q^{k+1}};
• walkBlockCount q T: the number N = 1 + ⌊log T/log q⌋; the blocks B_k with k ≥ N are empty (walkBlock_eq_empty);
• submartingale_exp_mul_walk: (exp(cS_t))_{t ≥ 0} is a submartingale for every c ∈ ℝ;
• measure_exists_le_walk_le: eq. (S5), by Doob's maximal inequality (maximal_ineq);
• measure_exists_le_abs_walk_le: eq. (S5) with |S_t| in place of S_t and an additional factor 2;
• measure_walkBlock_le: eq. (S6);
• measure_exists_le_sq_walk_div_le: the union bound over the nonempty blocks;
• lt_walkMax_iff and measure_lt_walkMax_le: for x ≥ 1, M > x exactly when max_{1 ≤ t ≤ T} S_t²/t > (2/a) log x, and pr(M > x) ≤ min{1, 2N x^{−1/(aq)}};
• lintegral_walkMax_eq, one_add_lintegral_min_rpow, and lintegral_walkMax_le: E(M) = 1 + ∫_1^∞ pr(M > x) dx ≤ 1 + ∫_1^∞ min(1, N'x^{−p}) dx = pN'^{1/p}/(p − 1) with p = 1/(aq), so that E(M) ≤ N'^{aq}/(1 − aq);
• log_lintegral_walkMax_le: log E(M) ≤ aq log(2 + 2 log T/log q) + log{1/(1 − aq)};
• iSup_lintegral_reward_le_lintegral_walkMax and log_le_of_le_iSup_lintegral_reward: sup_τ E(h_{τ∧T}) ≤ E(M), so that every η ≤ sup_τ E(h_{τ∧T}) satisfies the bound of Lemma S3.

We prove eq. (S5) for −S_t by Doob's maximal inequality applied to the submartingale exp(−xS_t/u). In the paper, it follows from eq. (S5) for S_t by symmetry. The statements hold for every T ≥ 0, with log 0 = 0 as in Mathlib, while Lemma S3 assumes T ≥ 1.

The increments of the random walk

The submartingale exp(cS_t)

theorem LogOptimal.integrable_exp_mul_walk (c : ℝ) (t : ℕ) : MeasureTheory.Integrable (fun (ω : ℕ → ℝ) => Real.exp (c * walk t ω)) stdGaussSeq

theorem LogOptimal.integral_exp_mul_walk (c : ℝ) (t : ℕ) : ∫ (ω : ℕ → ℝ), Real.exp (c * walk t ω) ∂stdGaussSeq = Real.exp (↑t * c ^ 2 / 2)

Since S_t is the sum of t independent N(0, 1) increments, E{exp(cS_t)} = exp(tc²/2).

theorem LogOptimal.submartingale_exp_mul_walk (c : ℝ) : MeasureTheory.Submartingale (fun (t : ℕ) (ω : ℕ → ℝ) => Real.exp (c * walk t ω)) walkFiltration stdGaussSeq

For every c ∈ ℝ, (exp(cS_t))_{t ≥ 0} is a submartingale with respect to the filtration generated by (S_t). For an event A of this filtration at time t, the increment S_{t+1} − S_t is N(0, 1) and independent of 1(A) exp(cS_t), so that E{1(A) exp(cS_{t+1})} = E{1(A) exp(cS_t)} exp(c²/2) ≥ E{1(A) exp(cS_t)}.

Doob's maximal inequality, eq. (S5)

theorem LogOptimal.measure_exists_le_mul_walk_le (c y : ℝ) (u : ℕ) : stdGaussSeq {ω : ℕ → ℝ | ∃ t ≤ u, y ≤ c * walk t ω} ≤ ENNReal.ofReal (Real.exp (↑u * c ^ 2 / 2 - y))

Doob's maximal inequality applied to the submartingale exp(cS_t): for all c, y ∈ ℝ, pr(max_{t ≤ u} cS_t ≥ y) ≤ e^{−y} E{exp(cS_u)} = exp(uc²/2 − y).

theorem LogOptimal.measure_exists_le_walk_le {x : ℝ} (hx : 0 ≤ x) {u : ℕ} (hu : 1 ≤ u) : stdGaussSeq {ω : ℕ → ℝ | ∃ t ≤ u, x ≤ walk t ω} ≤ ENNReal.ofReal (Real.exp (-x ^ 2 / (2 * ↑u)))

Eq. (S5): for x ≥ 0 and u ≥ 1, pr(max_{t ≤ u} S_t ≥ x) ≤ exp{−x²/(2u)}, by Doob's maximal inequality applied to the submartingale exp(xS_t/u).

theorem LogOptimal.measure_exists_le_neg_walk_le {x : ℝ} (hx : 0 ≤ x) {u : ℕ} (hu : 1 ≤ u) : stdGaussSeq {ω : ℕ → ℝ | ∃ t ≤ u, x ≤ -walk t ω} ≤ ENNReal.ofReal (Real.exp (-x ^ 2 / (2 * ↑u)))

Eq. (S5) for −S_t: for x ≥ 0 and u ≥ 1, pr{max_{t ≤ u} (−S_t) ≥ x} ≤ exp{−x²/(2u)}, by Doob's maximal inequality applied to the submartingale exp(−xS_t/u).

theorem LogOptimal.measure_exists_le_abs_walk_le {x : ℝ} (hx : 0 ≤ x) {u : ℕ} (hu : 1 ≤ u) : stdGaussSeq {ω : ℕ → ℝ | ∃ t ≤ u, x ≤ |walk t ω|} ≤ ENNReal.ofReal (2 * Real.exp (-x ^ 2 / (2 * ↑u)))

Eq. (S5) with |S_t| in place of S_t and an additional factor 2: for x ≥ 0 and u ≥ 1, pr(max_{t ≤ u} |S_t| ≥ x) ≤ 2 exp{−x²/(2u)}.

The blocks, eq. (S6), and the union bound

noncomputable def LogOptimal.walkBlock (q : ℝ) (T k : ℕ) : Finset ℕ

The block B_k = {t ≤ T : q^k ≤ t < q^{k+1}} of times of the proof of Lemma S3.

Equations

• LogOptimal.walkBlock q T k = {t ∈ Finset.range (T + 1) | q ^ k ≤ ↑t ∧ ↑t < q ^ (k + 1)}

noncomputable def LogOptimal.walkBlockCount (q : ℝ) (T : ℕ) : ℕ

The number N = 1 + ⌊log T/log q⌋ of the proof of Lemma S3. For q > 1, the blocks B_k with k ≥ N are empty (walkBlock_eq_empty). The floor is taken in ℕ; it agrees with the integer floor of the paper since log T/log q ≥ 0 for T ≥ 1 and q > 1.

Equations

• LogOptimal.walkBlockCount q T = 1 + ⌊Real.log ↑T / Real.log q⌋₊

theorem LogOptimal.walkBlock_eq_empty {q : ℝ} (hq : 1 < q) {T k : ℕ} (hk : walkBlockCount q T ≤ k) : walkBlock q T k = ∅

For q > 1, the block B_k is empty for k ≥ N: an element t of B_k satisfies q^k ≤ t ≤ T, so that k ≤ log T/log q.

theorem LogOptimal.mem_walkBlock_floor {q : ℝ} (hq : 1 < q) {T t : ℕ} (ht : 1 ≤ t) (htT : t ≤ T) : t ∈ walkBlock q T ⌊Real.log ↑t / Real.log q⌋₊

Every t with 1 ≤ t ≤ T lies in the block B_k with k = ⌊log t/log q⌋.

theorem LogOptimal.measure_walkBlock_le {q : ℝ} (hq : 1 < q) (T k : ℕ) {z : ℝ} (hz : 0 ≤ z) : stdGaussSeq {ω : ℕ → ℝ | ∃ t ∈ walkBlock q T k, z ^ 2 ≤ walk t ω ^ 2 / ↑t} ≤ ENNReal.ofReal (2 * Real.exp (-z ^ 2 / (2 * q)))

Eq. (S6): for z ≥ 0, pr(max_{t ∈ B_k} S_t²/t ≥ z²) ≤ pr(max_{t ≤ u} |S_t| ≥ zm^{1/2}) ≤ 2 exp{−z²m/(2u)} ≤ 2 exp{−z²/(2q)}, where m and u are the smallest and the largest elements of a nonempty block B_k, and u/m < q. If B_k is empty, the event is empty.

theorem LogOptimal.measure_exists_le_sq_walk_div_le {q : ℝ} (hq : 1 < q) (T : ℕ) {z : ℝ} (hz : 0 ≤ z) : stdGaussSeq {ω : ℕ → ℝ | ∃ t ∈ Finset.Icc 1 T, z ^ 2 ≤ walk t ω ^ 2 / ↑t} ≤ ENNReal.ofReal (2 * ↑(walkBlockCount q T) * Real.exp (-z ^ 2 / (2 * q)))

The union bound in eq. (S6) over the nonempty blocks: for z ≥ 0, pr(max_{1 ≤ t ≤ T} S_t²/t ≥ z²) ≤ 2N exp{−z²/(2q)}. Every t with 1 ≤ t ≤ T lies in the block B_k with k = ⌊log t/log q⌋, and k < N since this block is nonempty.

The maximum M and its tail

noncomputable def LogOptimal.walkMax (s : ℝ) (T : ℕ) (ω : ℕ → ℝ) : ℝ

The maximum M = max[1, max_{1 ≤ t ≤ T} exp{aS_t²/(2t)}] of the proof of Lemma S3, with a = 1 − s², as a function of the increments ω of the random walk: the maximum over 0 ≤ t ≤ T of the terms 1 for t = 0 and exp{aS_t²/(2t)} for t ≥ 1.

Equations

• LogOptimal.walkMax s T ω = (Finset.range (T + 1)).sup' ⋯ fun (t : ℕ) => if t = 0 then 1 else Real.exp ((1 - s ^ 2) * LogOptimal.walk t ω ^ 2 / (2 * ↑t))

theorem LogOptimal.measurable_walkMax (s : ℝ) (T : ℕ) : Measurable (walkMax s T)

theorem LogOptimal.one_le_walkMax (s : ℝ) (T : ℕ) (ω : ℕ → ℝ) : 1 ≤ walkMax s T ω

theorem LogOptimal.reward_le_walkMax {s : ℝ} (hs : s ≤ 1) {T t : ℕ} (ht : t ≤ T) (ω : ℕ → ℝ) : reward s t ω ≤ walkMax s T ω

Since s ≤ 1, h_t ≤ M for 0 ≤ t ≤ T.

theorem LogOptimal.lt_walkMax_iff {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (T : ℕ) {x : ℝ} (hx : 1 ≤ x) (ω : ℕ → ℝ) : x < walkMax s T ω ↔ ∃ t ∈ Finset.Icc 1 T, 2 / (1 - s ^ 2) * Real.log x < walk t ω ^ 2 / ↑t

For x ≥ 1, M > x exactly when max_{1 ≤ t ≤ T} S_t²/t > (2/a) log x, with a = 1 − s².

theorem LogOptimal.measure_lt_walkMax_le {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (T : ℕ) {q : ℝ} (hq : 1 < q) {x : ℝ} (hx : 1 ≤ x) : stdGaussSeq {ω : ℕ → ℝ | x < walkMax s T ω} ≤ ENNReal.ofReal (min 1 (2 * ↑(walkBlockCount q T) * x ^ (-(1 / ((1 - s ^ 2) * q)))))

For x ≥ 1, pr(M > x) ≤ min{1, 2N x^{−1/(aq)}}, with a = 1 − s²: by lt_walkMax_iff, the union bound with z² = (2/a) log x applies.

The expectation of M

theorem LogOptimal.lintegral_walkMax_eq (s : ℝ) (T : ℕ) : ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (walkMax s T ω) ∂stdGaussSeq = 1 + ∫⁻ (x : ℝ) in Set.Ioi 1, stdGaussSeq {ω : ℕ → ℝ | x < walkMax s T ω}

Since M ≥ 1, the layer-cake formula E(M) = ∫_0^∞ pr(M > x) dx gives E(M) = 1 + ∫_1^∞ pr(M > x) dx.

theorem LogOptimal.one_add_lintegral_min_rpow {N' p : ℝ} (hN' : 1 ≤ N') (hp : 1 < p) : 1 + ∫⁻ (x : ℝ) in Set.Ioi 1, ENNReal.ofReal (min 1 (N' * x ^ (-p))) = ENNReal.ofReal (p * N' ^ (1 / p) / (p - 1))

For N' ≥ 1 and p > 1, 1 + ∫_1^∞ min(1, N'x^{−p}) dx = pN'^{1/p}/(p − 1): the integrand equals one on (1, x₀] and N'x^{−p} on (x₀, ∞), where x₀ = N'^{1/p}.

theorem LogOptimal.lintegral_walkMax_le {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (T : ℕ) {q : ℝ} (hq : 1 < q) (hqa : q < 1 / (1 - s ^ 2)) : ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (walkMax s T ω) ∂stdGaussSeq ≤ ENNReal.ofReal ((2 * ↑(walkBlockCount q T)) ^ ((1 - s ^ 2) * q) / (1 - (1 - s ^ 2) * q))

E(M) ≤ N'^{aq}/(1 − aq), with a = 1 − s² and N' = 2N. With p = 1/(aq) > 1, lintegral_walkMax_eq, measure_lt_walkMax_le, and one_add_lintegral_min_rpow give E(M) = 1 + ∫_1^∞ pr(M > x) dx ≤ 1 + ∫_1^∞ min(1, N'x^{−p}) dx = pN'^{1/p}/(p − 1), and pN'^{1/p}/(p − 1) = N'^{aq}/(1 − aq).

theorem LogOptimal.lintegral_walkMax_le_exp {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (T : ℕ) {q : ℝ} (hq : 1 < q) (hqa : q < 1 / (1 - s ^ 2)) : ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (walkMax s T ω) ∂stdGaussSeq ≤ ENNReal.ofReal (Real.exp ((1 - s ^ 2) * q * Real.log (2 + 2 * Real.log ↑T / Real.log q) + Real.log (1 / (1 - (1 - s ^ 2) * q))))

Since N' ≤ 2 + 2 log T/log q, E(M) ≤ exp[aq log(2 + 2 log T/log q) + log{1/(1 − aq)}], with a = 1 − s².

theorem LogOptimal.log_lintegral_walkMax_le {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (T : ℕ) {q : ℝ} (hq : 1 < q) (hqa : q < 1 / (1 - s ^ 2)) : (∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (walkMax s T ω) ∂stdGaussSeq).log ≤ ↑((1 - s ^ 2) * q * Real.log (2 + 2 * Real.log ↑T / Real.log q) + Real.log (1 / (1 - (1 - s ^ 2) * q)))

log E(M) ≤ aq log(2 + 2 log T/log q) + log{1/(1 − aq)}, with a = 1 − s², the right-hand side of Lemma S3.

The supremum of Lemma 2(ii)

theorem LogOptimal.iSup_lintegral_reward_le_lintegral_walkMax {s : ℝ} (hs : s ≤ 1) (T : ℕ) : ⨆ (τ : (ℕ → ℝ) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime walkFiltration τ), ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (reward s (truncTime τ T ω) ω) ∂stdGaussSeq ≤ ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (walkMax s T ω) ∂stdGaussSeq

Since h_t ≤ M for 0 ≤ t ≤ T, sup_τ E(h_{τ∧T}) ≤ E(M), where τ ranges over the stopping times of the filtration generated by (S_t), as in Lemma 2(ii).

theorem LogOptimal.log_le_of_le_iSup_lintegral_reward {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {T : ℕ} {q : ℝ} (hq : 1 < q) (hqa : q < 1 / (1 - s ^ 2)) {η : ENNReal} (hη : η ≤ ⨆ (τ : (ℕ → ℝ) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime walkFiltration τ), ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (reward s (truncTime τ T ω) ω) ∂stdGaussSeq) : η.log ≤ ↑((1 - s ^ 2) * q * Real.log (2 + 2 * Real.log ↑T / Real.log q) + Real.log (1 / (1 - (1 - s ^ 2) * q)))

The bound of Lemma S3 for every η ≤ sup_τ E(h_{τ∧T}). Since Lemma 2(ii) gives η_T = sup_τ E(h_{τ∧T}), the case η = η_T is Lemma S3.