The random walk when `s ≥ 1` #

This file proves the statements on the random walk (S_t) of Lemma 2 that the proof of Proposition 4 (Section S1.8 of the paper) uses.

reward_le: if s ≥ 1, then h_t ≤ s for every t.
firstSmall ε: the stopping time τ_ε, the first t ≥ 1 with S_t² ≤ εt.
ae_tendsto_sq_div: (S_{t+1} − S_t)²/t → 0 almost surely, by the strong law of large numbers.
frequently_signChange: under the law of the iterated logarithm, the random walk changes sign infinitely often.
ae_firstSmall_lt_top: τ_ε < ∞ almost surely.
lintegral_reward_firstSmall_ge: E(h_{τ_ε ∧ T}) ≥ s exp{−(s² − 1)ε/2} P(τ_ε ≤ T), eq. (S10).
tendsto_walkValue: the value sup_τ E(h_{τ∧T}) of the stopping problem tends to s.

The reward when `s ≥ 1` #

source

theorem LogOptimal.reward_nonneg {s : ℝ} (hs : 0 ≤ s) (t : ℕ) (ω : ℕ → ℝ) :

0 ≤ reward s t ω

source

theorem LogOptimal.reward_le {s : ℝ} (hs : 1 ≤ s) (t : ℕ) (ω : ℕ → ℝ) :

reward s t ω ≤ s

The stopping time `τ_ε` #

source

noncomputable def LogOptimal.firstSmall (ε : ℝ) (ω : ℕ → ℝ) :

ℕ∞

The stopping time τ_ε of the proof of Proposition 4: the first t ≥ 1 with S_t² ≤ εt, or ∞ if there is none.

Equations

LogOptimal.firstSmall ε ω = if h : ∃ (t : ℕ), 1 ≤ t ∧ LogOptimal.walk t ω ^ 2 ≤ ε * ↑t then ↑(Nat.find h) else ⊤

Instances For

source

theorem LogOptimal.firstSmall_le_iff (ε : ℝ) (ω : ℕ → ℝ) (t : ℕ) :

firstSmall ε ω ≤ ↑t ↔ ∃ u ≤ t, 1 ≤ u ∧ walk u ω ^ 2 ≤ ε * ↑u

source

theorem LogOptimal.firstSmall_lt_top_iff (ε : ℝ) (ω : ℕ → ℝ) :

firstSmall ε ω < ⊤ ↔ ∃ (t : ℕ), 1 ≤ t ∧ walk t ω ^ 2 ≤ ε * ↑t

source

theorem LogOptimal.firstSmall_spec {ε : ℝ} {ω : ℕ → ℝ} {u : ℕ} (hu : firstSmall ε ω = ↑u) :

1 ≤ u ∧ walk u ω ^ 2 ≤ ε * ↑u

source

theorem LogOptimal.isStoppingTime_firstSmall (ε : ℝ) :

MeasureTheory.IsStoppingTime walkFiltration (firstSmall ε)

Sign changes and small increments #

source

theorem LogOptimal.walk_succ (t : ℕ) (ω : ℕ → ℝ) :

walk (t + 1) ω = walk t ω + ω t

source

theorem LogOptimal.ae_tendsto_sq_div :

∀ᵐ (ω : ℕ → ℝ) ∂stdGaussSeq , Filter.Tendsto (fun (t : ℕ) => ω t ^ 2 / ↑t) Filter.atTop (nhds 0)

(S_{t+1} − S_t)²/t → 0 almost surely, by the strong law of large numbers applied to the squared increments.

source

theorem LogOptimal.frequently_pos_neg (hLIL : LawOfIteratedLogarithm) :

∀ᵐ (ω : ℕ → ℝ) ∂stdGaussSeq , (∃ᶠ (t : ℕ) in Filter.atTop , 0 < walk t ω) ∧ ∃ᶠ (t : ℕ) in Filter.atTop , walk t ω < 0

Under the law of the iterated logarithm, the random walk takes positive values and negative values infinitely often.

source

theorem LogOptimal.frequently_signChange {ω : ℕ → ℝ} (hpos : ∃ᶠ (t : ℕ) in Filter.atTop , 0 < walk t ω) (hneg : ∃ᶠ (t : ℕ) in Filter.atTop , walk t ω < 0) :

∃ᶠ (t : ℕ) in Filter.atTop , walk t ω * walk (t + 1) ω ≤ 0

If the random walk takes positive values and negative values infinitely often, then it changes sign infinitely often: S_t S_{t+1} ≤ 0 for infinitely many t.

source

theorem LogOptimal.abs_le_abs_sub_of_mul_nonpos {a b : ℝ} (h : a * b ≤ 0) :

|b| ≤ |b - a|

source

theorem LogOptimal.ae_firstSmall_lt_top (hLIL : LawOfIteratedLogarithm) {ε : ℝ} (hε : 0 < ε) :

∀ᵐ (ω : ℕ → ℝ) ∂stdGaussSeq , firstSmall ε ω < ⊤

Under the law of the iterated logarithm, τ_ε < ∞ almost surely for every ε > 0.

The value of the stopping problem #

source

theorem LogOptimal.lintegral_reward_firstSmall_ge {s : ℝ} (hs : 1 ≤ s) (ε : ℝ) (T : ℕ) :

ENNReal.ofReal (s * Real.exp (-((s ^ 2 - 1) * ε) / 2)) * stdGaussSeq {ω : ℕ → ℝ | firstSmall ε ω ≤ ↑T} ≤ ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (reward s (truncTime (firstSmall ε) T ω) ω) ∂stdGaussSeq

The lower bound (S10): E(h_{τ_ε ∧ T}) ≥ s exp{−(s² − 1)ε/2} P(τ_ε ≤ T) for s ≥ 1.

source

noncomputable def LogOptimal.walkValue (s : ℝ) (T : ℕ) :

ENNReal

The value sup_τ E(h_{τ∧T}) of the stopping problem of Lemma 2(ii), where τ ranges over the stopping times of the filtration generated by the random walk.

Equations