Lemma S5: lower bounds on J_k, and the stopping rule τ'

This file proves Lemma S5 of the supplementary material (lem_jk_proof), following its proof, and the facts on the stopping rule τ' of Section S1.6 that the proofs of Lemma S4 and of the claims after Lemma S5 use. Let t = t_k = r^k, γ² = ρ² + s², v₁ = ρ² + s²/t, and v₂ = γ² + 1/t, so that ρ² ≤ v₁ ≤ γ², v₁ ≤ v₂ ≤ γ² + 1, and J_k(x) = {2φ_{v₁}(x̄_t)}^{-1}{∫_{𝒵_k(y)} φ₁(z)φ_{γ²}(x̄_t − t^{-1/2}z) dz + ξ_t φ_{v₂}(x̄_t)}.

• lb_sqrt_div_mul_gaussianPDFReal_le: for 0 < v₁ ≤ v₂, φ_{v₂}/φ_{v₁} ≥ (v₁/v₂)^{1/2} pointwise, the inequality of the proof of part (i);
• lb_gaussianPDFReal_mul_exp_le: for |b| ≤ B, φ_v(a − b) ≥ φ_v(a) exp{−(2B|a| + B²)/(2v)}, the inequality of the proof of part (ii);
• measurableSet_lbZset and lbZset_subset: the set 𝒵_k(y) is measurable and contained in {z : c ≤ |z| ≤ c + 1};
• lbZset_eq_of_mem_lbA: on A_k, 𝒵_k(y) = {z : c ≤ |z| ≤ c + 1} (proof of part (iii));
• lbP_nonneg and two_mul_gaussianPDFReal_le_lbP: p_k ≥ 0, and p_k ≥ 2φ₁(c + 1) on A_k;
• lem_jk_proof: Lemma S5;
• lb_runningMean_eq_add_sum_helmertY and lbZ_pow_eq: by Lemma S2(ii), x̄_n = x̄_m + ∑_{i=m+1}^n y_i/{i(i − 1)}^{1/2}, so that Z_{t_j} = (t_j/t_k)^{1/2} Z_{t_k} − W_{jk}(Y^{t_k}) for j ≤ k;
• lbStoppingRule_eq_coe_iff: τ' = t_k exactly when Z_{t_k} ∈ 𝒵_k(Y^{t_k});
• lbStoppingRule_eq_of_mem_lbA: on {Y^{t_k} ∈ A_k}, τ' stops at t_k whenever c ≤ |Z_{t_k}| ≤ c + 1.

Inequalities between Gaussian densities

theorem LogOptimal.lb_gaussianPDFReal_le (v : NNReal) (x : ℝ) : ProbabilityTheory.gaussianPDFReal 0 v x ≤ (√(2 * Real.pi * ↑v))⁻¹

φ_v(x) ≤ (2πv)^{-1/2}.

theorem LogOptimal.lb_sqrt_div_mul_gaussianPDFReal_le {v₁ v₂ : ℝ} (h₁ : 0 < v₁) (h₁₂ : v₁ ≤ v₂) (x : ℝ) : √(v₁ / v₂) * ProbabilityTheory.gaussianPDFReal 0 v₁.toNNReal x ≤ ProbabilityTheory.gaussianPDFReal 0 v₂.toNNReal x

For 0 < v₁ ≤ v₂, φ_{v₂}/φ_{v₁} ≥ (v₁/v₂)^{1/2} pointwise (proof of Lemma S5(i)).

theorem LogOptimal.lb_gaussianPDFReal_mul_exp_le {v : ℝ} (hv : 0 < v) (a b B : ℝ) (hb : |b| ≤ B) : ProbabilityTheory.gaussianPDFReal 0 v.toNNReal a * Real.exp (-(2 * B * |a| + B ^ 2) / (2 * v)) ≤ ProbabilityTheory.gaussianPDFReal 0 v.toNNReal (a - b)

For |b| ≤ B, φ_v(a − b) ≥ φ_v(a) exp{−(2B|a| + B²)/(2v)}, since (a − b)² ≤ a² + 2B|a| + B² (proof of Lemma S5(ii)).

The set 𝒵_k(y) and the probability p_k(y)

theorem LogOptimal.measurableSet_lb_annulus (c : ℝ) : MeasurableSet {z : ℝ | c ≤ |z| ∧ |z| ≤ c + 1}

The annulus {z : c ≤ |z| ≤ c + 1}.

theorem LogOptimal.measurableSet_lbZset (r k : ℕ) (c : ℝ) (x : ℕ → ℝ) : MeasurableSet (lbZset r k c x)

theorem LogOptimal.lbZset_subset (r k : ℕ) (c : ℝ) (x : ℕ → ℝ) : lbZset r k c x ⊆ {z : ℝ | c ≤ |z| ∧ |z| ≤ c + 1}

theorem LogOptimal.lbZset_eq_of_mem_lbA {r k : ℕ} (hr : 1 ≤ r) {c : ℝ} {x : ℕ → ℝ} (hx : x ∈ lbA r k (lbCPrime r c)) : lbZset r k c x = {z : ℝ | c ≤ |z| ∧ |z| ≤ c + 1}

On the event A_k = {y : max_{j<k} |W_{jk}(y)| < c'} with c' = c − (c + 1)r^{-1/2} > 0, no earlier horizon removes a point of the annulus from 𝒵_k(y) (proof of Lemma S5(iii)): for j < k and c ≤ |z| ≤ c + 1, |(t_j/t)^{1/2}z − W_{jk}(y)| < (c + 1)r^{-1/2} + c' = c.

theorem LogOptimal.lbP_nonneg (r k : ℕ) (c : ℝ) (x : ℕ → ℝ) : 0 ≤ lbP r k c x

theorem LogOptimal.volume_lb_annulus {c : ℝ} (hc : 0 ≤ c) : MeasureTheory.volume {z : ℝ | c ≤ |z| ∧ |z| ≤ c + 1} = 2

The annulus {z : c ≤ |z| ≤ c + 1} has Lebesgue measure two for c ≥ 0.

theorem LogOptimal.two_mul_gaussianPDFReal_le_lbP {r k : ℕ} (hr : 1 ≤ r) {c : ℝ} (hc : 0 < c) {x : ℕ → ℝ} (hx : x ∈ lbA r k (lbCPrime r c)) : 2 * ProbabilityTheory.gaussianPDFReal 0 1 (c + 1) ≤ lbP r k c x

Lemma S5(iii): on A_k, p_k(y) = ∫_{c ≤ |z| ≤ c+1} φ₁(z) dz ≥ 2φ₁(c + 1).

Lemma S5

theorem LogOptimal.lem_jk_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 < ρ → ∀ (r K : ℕ) (c : ℝ), 4 ≤ r → 1 ≤ K → 0 < c → ∀ k ≤ K, ∀ (x : ℕ → ℝ), have t := r ^ k; have γ := √(ρ ^ 2 + s ^ 2); (0 < lbJ s ρ r K c k x ∧ lbBetaPrime s ρ ≤ Real.log ((↑K + 1) * lbJ s ρ r K c k x)) ∧ ρ / (2 * γ) * Real.exp (-(2 * (c + 1) * |runningMean t x| / √↑t + (c + 1) ^ 2 / ↑t) / (2 * γ ^ 2)) * lbP r k c x ≤ lbJ s ρ r K c k x ∧ (0 < lbCPrime r c → x ∈ lbA r k (lbCPrime r c) → 2 * ProbabilityTheory.gaussianPDFReal 0 1 (c + 1) ≤ lbP r k c x)

The stopping rule τ'

theorem LogOptimal.lb_runningMean_eq_add_sum_helmertY {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) (x : ℕ → ℝ) : runningMean n x = runningMean m x + ∑ i ∈ Finset.Ioc m n, helmertY i x / √(↑i * (↑i - 1))

By Lemma S2(ii), x̄_n = x̄_m + ∑_{i=m+1}^n y_i/{i(i − 1)}^{1/2} for 1 ≤ m ≤ n.

theorem LogOptimal.lbZ_pow_eq {r : ℕ} (hr : 1 ≤ r) {j k : ℕ} (hjk : j ≤ k) (θ : ℝ) (x : ℕ → ℝ) : lbZ θ (r ^ j) x = √(↑r ^ j / ↑r ^ k) * lbZ θ (r ^ k) x - lbW r j k x

Z_{t_j} = (t_j/t_k)^{1/2} Z_{t_k} − W_{jk}(Y^{t_k}) for j ≤ k, by Lemma S2(ii) (proof of Lemma S4).

theorem LogOptimal.lbStoppingRule_eq_coe_iff {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) (c θ : ℝ) (x : ℕ → ℝ) : lbStoppingRule r K c θ x = ↑(r ^ k) ↔ lbZ θ (r ^ k) x ∈ lbZset r k c x

τ' = t_k exactly when Z_{t_k} ∈ 𝒵_k(Y^{t_k}): the rule stops at t_k when c ≤ |Z_{t_k}| ≤ c + 1 and c ≤ |Z_{t_j}| ≤ c + 1 fails for every j < k, and Z_{t_j} = (t_j/t_k)^{1/2} Z_{t_k} − W_{jk}(Y^{t_k}) (proof of Lemma S4).

theorem LogOptimal.lbStoppingRule_eq_of_mem_lbA {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) {c : ℝ} (θ : ℝ) {x : ℕ → ℝ} (hx : x ∈ lbA r k (lbCPrime r c)) (h₁ : c ≤ |lbZ θ (r ^ k) x|) (h₂ : |lbZ θ (r ^ k) x| ≤ c + 1) : lbStoppingRule r K c θ x = ↑(r ^ k)

The stopping rule on A_k (Section S1.6, after Lemma S5): if c' > 0, Y^t ∈ A_k, and c ≤ |Z_t| ≤ c + 1, then τ' = t for t = t_k.