The upper bound of Proposition 3(i)

This file proves the upper bound in Proposition 3(i) of the paper, following its proof in Section S1.6: for fixed q ∈ (1, 1/a), with a = 1 − s², log(2 + 2 log T/log q) = log log T + O(1), and Lemma S3 gives limsup_{T→∞} log η_T/log log T ≤ aq; letting q → 1 replaces aq by a. We write the step log(2 + 2 log T/log q) = log log T + O(1) as the bound log(2 + 2 log T/log q) ≤ log log T + log(2 + 2/log q) for T ≥ 3, and the limit q → 1 as the choice, for each b > a, of a q with aq < b.

• log_eta_le_mul_log_log_add: log η_T ≤ aq log log T + aq log(2 + 2/log q) + log{1/(1 − aq)} for T ≥ 3;
• eventually_log_eta_lt: for every b > 1 − s², eventually log η_T < b log log T;
• eta_gaussNumeraire_lt_top_of_lt_one: η_T < ∞ for T ≥ 1.

theorem LogOptimal.log_two_add_le_log_log_add {q : ℝ} (hq : 1 < q) {T : ℕ} (hT : 3 ≤ T) : Real.log (2 + 2 * Real.log ↑T / Real.log q) ≤ Real.log (Real.log ↑T) + Real.log (2 + 2 / Real.log q)

For T ≥ 3 and q > 1, log(2 + 2 log T/log q) ≤ log log T + log(2 + 2/log q), since log T ≥ 1.

theorem LogOptimal.log_eta_le_mul_log_log_add {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {q : ℝ} (hq : 1 < q) (hqa : q < 1 / (1 - s ^ 2)) {T : ℕ} (hT : 3 ≤ T) : (eta gaussNull (gaussNumeraire s) T).log ≤ ↑((1 - s ^ 2) * q * Real.log (Real.log ↑T) + ((1 - s ^ 2) * q * Real.log (2 + 2 / Real.log q) + Real.log (1 / (1 - (1 - s ^ 2) * q))))

Lemma S3 with log(2 + 2 log T/log q) ≤ log log T + log(2 + 2/log q): for T ≥ 3, log η_T ≤ aq log log T + aq log(2 + 2/log q) + log{1/(1 − aq)}, with a = 1 − s².

theorem LogOptimal.eventually_log_eta_lt {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {b : ℝ} (hb : 1 - s ^ 2 < b) : ∀ᶠ (T : ℕ) in Filter.atTop, (eta gaussNull (gaussNumeraire s) T).log < ↑(b * Real.log (Real.log ↑T))

For every b > 1 − s², eventually log η_T < b log log T: the upper bound in Proposition 3(i).

theorem LogOptimal.eta_gaussNumeraire_lt_top_of_lt_one {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {T : ℕ} (hT : 1 ≤ T) : eta gaussNull (gaussNumeraire s) T < ⊤

η_T < ∞ for T ≥ 1, by Lemma S3.