Limits of ratios to log log T and the law of the iterated logarithm for the reward

The rates of Section 4.3 of the paper are limits, in [−∞, ∞], of ratios x_T/log log T. This file collects the elementary facts on these ratios that the proofs of Proposition 3, Theorem 1, and Proposition S5 use, and it proves the claim of Section 4.2 that the law of the iterated logarithm gives limsup_{t→∞} log h_t/log log t = 1 − s² almost surely for s < 1.

• tendsto_log_log_natCast: log log T → ∞, and log_log_natCast_pos: log log T > 0 for T ≥ 3;
• ereal_div_coe_lt_coe_iff, ereal_coe_lt_div_coe_iff: comparisons of x/d with a real b, for a real d > 0;
• tendsto_ereal_of_real_bounds, limsup_ereal_eq_of_real_bounds: a limit or an upper limit in [−∞, ∞] from real bounds;
• tendsto_div_log_log_of_bounds: x_T/log log T → L from bounds a log log T < x_T < b log log T that hold eventually for all reals a < L < b;
• eventually_lt_mul_sub_sqrt: for b > 0 and every C, eventually C < bx − 28x^{1/2};
• log_reward_div_eq: log h_t/log log t = log s/log log t + (1 − s²)a_t² for t ≥ 3, where a_t = S_t/(2t log log t)^{1/2};
• sec4_lil_proof: the law of the iterated logarithm for the reward h_t.

The function log log T

theorem LogOptimal.tendsto_log_log_natCast : Filter.Tendsto (fun (T : ℕ) => Real.log (Real.log ↑T)) Filter.atTop Filter.atTop

log log T → ∞ as T → ∞ over the natural numbers.

theorem LogOptimal.one_lt_log_natCast {T : ℕ} (hT : 3 ≤ T) : 1 < Real.log ↑T

log T > 1 for T ≥ 3.

theorem LogOptimal.log_log_natCast_pos {T : ℕ} (hT : 3 ≤ T) : 0 < Real.log (Real.log ↑T)

log log T > 0 for T ≥ 3.

theorem LogOptimal.log_log_natCast_le_log_log {t T : ℕ} (ht : 3 ≤ t) (htT : t ≤ T) : Real.log (Real.log ↑t) ≤ Real.log (Real.log ↑T)

log log T is nondecreasing on T ≥ 3.

Ratios in [−∞, ∞]

theorem LogOptimal.ereal_div_coe_lt_coe_iff {x : EReal} {b d : ℝ} (hd : 0 < d) : x / ↑d < ↑b ↔ x < ↑(b * d)

For a real d > 0, x/d < b exactly when x < bd.

theorem LogOptimal.ereal_coe_lt_div_coe_iff {x : EReal} {a d : ℝ} (hd : 0 < d) : ↑a < x / ↑d ↔ ↑(a * d) < x

For a real d > 0, a < x/d exactly when ad < x.

theorem LogOptimal.tendsto_ereal_of_real_bounds {u : ℕ → EReal} {L : ℝ} (hlow : ∀ a < L, ∀ᶠ (T : ℕ) in Filter.atTop, ↑a < u T) (hup : ∀ (b : ℝ), L < b → ∀ᶠ (T : ℕ) in Filter.atTop, u T < ↑b) : Filter.Tendsto u Filter.atTop (nhds ↑L)

A sequence in [−∞, ∞] tends to a real L if, for all reals a < L < b, it eventually lies between a and b.

theorem LogOptimal.limsup_ereal_eq_of_real_bounds {u : ℕ → EReal} {L : ℝ} (hfreq : ∀ a < L, ∃ᶠ (T : ℕ) in Filter.atTop, ↑a < u T) (hup : ∀ (b : ℝ), L < b → ∀ᶠ (T : ℕ) in Filter.atTop, u T < ↑b) : Filter.limsup u Filter.atTop = ↑L

The upper limit of a sequence in [−∞, ∞] is a real L if, for all reals a < L < b, the sequence exceeds a infinitely often and is eventually below b.

theorem LogOptimal.tendsto_div_log_log_of_bounds {x : ℕ → EReal} {L : ℝ} (hlow : ∀ a < L, ∀ᶠ (T : ℕ) in Filter.atTop, ↑(a * Real.log (Real.log ↑T)) < x T) (hup : ∀ (b : ℝ), L < b → ∀ᶠ (T : ℕ) in Filter.atTop, x T < ↑(b * Real.log (Real.log ↑T))) : Filter.Tendsto (fun (T : ℕ) => x T / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑L)

x_T/log log T → L in [−∞, ∞] if, for all reals a < L < b, eventually a log log T < x_T < b log log T.

theorem LogOptimal.eventually_lt_mul_sub_sqrt {b : ℝ} (hb : 0 < b) (C : ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, C < b * x - 28 * √x

For b > 0 and every C, eventually C < bx − 28x^{1/2} as x → ∞.

The law of the iterated logarithm for the reward

theorem LogOptimal.log_reward_div_eq {s : ℝ} (hs : 0 < s) {t : ℕ} (ht : 3 ≤ t) (ω : ℕ → ℝ) : Real.log (reward s t ω) / Real.log (Real.log ↑t) = Real.log s / Real.log (Real.log ↑t) + (1 - s ^ 2) * (walk t ω / √(2 * ↑t * Real.log (Real.log ↑t))) ^ 2

For t ≥ 3, log h_t/log log t = log s/log log t + (1 − s²)a_t², where a_t = S_t/(2t log log t)^{1/2}.

theorem LogOptimal.sec4_lil_proof : LawOfIteratedLogarithm → ∀ (s : ℝ), 0 < s → s < 1 → ∀ᵐ (ω : ℕ → ℝ) ∂stdGaussSeq, Filter.limsup (fun (t : ℕ) => ↑(Real.log (reward s t ω) / Real.log (Real.log ↑t))) Filter.atTop = ↑(1 - s ^ 2)