Lemma S6: the lower bound for fixed K

This file proves Lemma S6 of the supplementary material from inequality (S8) of Lemma S4 (lem_fixedk_of_lbmix), following its proof. Let t = t_k = r^k, γ² = ρ² + s², and D_k(x) = {2(c + 1)t^{-1/2}|x̄_t| + (c + 1)²t^{-1}}/(2γ²).

• lb_gaussianReal_abs_ge_le: a N(0, v) variable has absolute value at least x ≥ 0 with probability at most exp{−x²/(2v)}, since φ₁(u + x) ≤ exp(−x²/2)φ₁(u) for u, x ≥ 0 and N(0, 1) is symmetric;
• lb_map_pi_gaussianReal_sum_mul: under N(0, v)^{⊗n}, ∑_m b_m y_m ∼ N(0, v ∑_m b_m²);
• lbWc, lbWy_eq_sum, and sum_lbWc_sq_le_one: W_{jk}(y) = ∑_{i=t_j+1}^{t_k} b_i y_i with b_i = t_j^{1/2}{i(i − 1)}^{-1/2}, and ∑_i b_i² = t_j(1/t_j − 1/t_k) ≤ 1;
• lb_mixAlt_map_helmertVec and lb_mixAlt_map_runningMean: under Q, Y^t ∼ N(0, s²)^{⊗(t−1)} and X̄_t ∼ N(0, ρ² + s²/t);
• mixAlt_abs_lbW_ge_le and mixAlt_compl_lbA_le: under Q, W_{jk}(Y^t) is normal with variance at most s², so that Q(Y^t ∉ A_k) ≤ K exp{−c'²/(2s²)} by a union bound over j < k;
• lb_integral_abs_runningMean_mixAlt_le: E_Q(|X̄_t|) ≤ (ρ² + s²/t)^{1/2} ≤ γ;
• log_lbJ_ge: log{(K + 1)J_k} ≥ β − (β − β')1(Y^t ∉ A_k) − D_k, by Lemma S5;
• eIntegral_log_lbJ_ge: E_Q[log{(K + 1)J_k}] ≥ β − (β − β')K exp{−c'²/(2s²)} − (c + 1)/(γ t^{1/2}) − (c + 1)²/(2γ²t);
• lem_fixedk_of_lbmix: Lemma S6, (S8) implies (S9), with ∑_k r^{−k/2} ≤ 2 and ∑_k r^{−k} ≤ 4/3 for r ≥ 4.

The proof of Lemma S6 states that W_{jk}(Y^t) ∼ N{0, s²(1 − t_j/t)} under Q; we use only that it is normal with variance s² ∑_i b_i² ≤ s², which gives the same tail bound.

The Gaussian tail

theorem LogOptimal.lb_gaussianReal_abs_ge_le {v : NNReal} (hv : v ≠ 0) {x : ℝ} (hx : 0 ≤ x) : (ProbabilityTheory.gaussianReal 0 v) {w : ℝ | x ≤ |w|} ≤ ENNReal.ofReal (Real.exp (-x ^ 2 / (2 * ↑v)))

The Gaussian tail: for v > 0 and x ≥ 0, a N(0, v) variable has absolute value at least x with probability at most exp{−x²/(2v)}.

Linear combinations of independent Gaussian variables

theorem LogOptimal.lb_map_pi_gaussianReal_sum_mul (v : NNReal) (n : ℕ) (b : Fin n → ℝ) : MeasureTheory.Measure.map (fun (y : Fin n → ℝ) => ∑ m : Fin n, b m * y m) (MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.gaussianReal 0 v) = ProbabilityTheory.gaussianReal 0 ((∑ m : Fin n, b m ^ 2).toNNReal * v)

Under N(0, v)^{⊗n}, ∑_m b_m y_m ∼ N(0, v ∑_m b_m²), by induction on n: the measure N(0, v)^{⊗(n+1)} is the product of its first factor and N(0, v)^{⊗n}, and N(0, v₁) ∗ N(0, v₂) = N(0, v₁ + v₂).

W_{jk} as a linear combination of the y_i

noncomputable def LogOptimal.lbWc (r j k i : ℕ) : ℝ

The coefficient b_i = t_j^{1/2}{i(i − 1)}^{-1/2} of y_i in W_{jk}(y) for t_j < i ≤ t_k, and zero otherwise.

Equations

• LogOptimal.lbWc r j k i = if r ^ j < i ∧ i ≤ r ^ k then √(↑r ^ j) / √(↑i * (↑i - 1)) else 0

theorem LogOptimal.lbWc_eq_zero {r j k i : ℕ} (hi : i ∉ Finset.Ioc (r ^ j) (r ^ k)) : lbWc r j k i = 0

theorem LogOptimal.lbWy_eq_sum {r : ℕ} (hr : 1 ≤ r) (j k : ℕ) (y : Fin (r ^ k - 1) → ℝ) : lbWy r j k y = ∑ m : Fin (r ^ k - 1), lbWc r j k (↑m + 2) * y m

W_{jk}(y) = ∑_m b_{m+2} y_{m+2}.

theorem LogOptimal.sum_lbWc_sq_le_one {r : ℕ} (hr : 1 ≤ r) {j k : ℕ} (hjk : j ≤ k) : ∑ m : Fin (r ^ k - 1), lbWc r j k (↑m + 2) ^ 2 ≤ 1

∑_i b_i² = t_j(1/t_j − 1/t_k) ≤ 1: the variance of W_{jk}(Y^t) is at most s².

The distributions of Y^t and X̄_t under Q

theorem LogOptimal.lb_mixAlt_map_helmertVec {t : ℕ} (ht : 1 ≤ t) (s ρ : ℝ) : MeasureTheory.Measure.map (helmertVec t) (mixAlt s ρ) = MeasureTheory.Measure.pi fun (x : Fin (t - 1)) => ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal

Under Q, Y^t ∼ N(0, s²)^{⊗(t−1)}.

theorem LogOptimal.lb_mixAlt_map_runningMean {t : ℕ} (ht : 1 ≤ t) (s ρ : ℝ) : MeasureTheory.Measure.map (runningMean t) (mixAlt s ρ) = ProbabilityTheory.gaussianReal 0 (ρ ^ 2 + s ^ 2 / ↑t).toNNReal

Under Q, X̄_t ∼ N(0, ρ² + s²/t).

theorem LogOptimal.mixAlt_abs_lbW_ge_le {s : ℝ} (hs : 0 < s) (ρ : ℝ) {r : ℕ} (hr : 1 ≤ r) {j k : ℕ} (hjk : j ≤ k) {c' : ℝ} (hc' : 0 < c') : (mixAlt s ρ) {x : ℕ → ℝ | c' ≤ |lbW r j k x|} ≤ ENNReal.ofReal (Real.exp (-c' ^ 2 / (2 * s ^ 2)))

Under Q, W_{jk}(Y^t) ∼ N(0, s² ∑_i b_i²) with ∑_i b_i² ≤ 1, so that Q(|W_{jk}| ≥ c') ≤ exp{−c'²/(2s²)} for c' > 0 (proof of Lemma S6).

theorem LogOptimal.mixAlt_compl_lbA_le {s : ℝ} (hs : 0 < s) (ρ : ℝ) {r : ℕ} (hr : 1 ≤ r) {K k : ℕ} (hk : k ≤ K) {c' : ℝ} (hc' : 0 < c') : (mixAlt s ρ) (lbA r k c')ᶜ ≤ ↑K * ENNReal.ofReal (Real.exp (-c' ^ 2 / (2 * s ^ 2)))

Union bound (proof of Lemma S6): Q(Y^t ∉ A_k) ≤ K exp{−c'²/(2s²)} for k ≤ K.

theorem LogOptimal.lb_integrable_abs_runningMean_mixAlt {t : ℕ} (ht : 1 ≤ t) (s ρ : ℝ) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => |runningMean t x|) (mixAlt s ρ)

theorem LogOptimal.lb_integral_abs_runningMean_mixAlt_le {t : ℕ} (ht : 1 ≤ t) {s ρ : ℝ} (hs : 0 < s) : ∫ (x : ℕ → ℝ), |runningMean t x| ∂mixAlt s ρ ≤ √(ρ ^ 2 + s ^ 2)

E_Q(|X̄_t|) ≤ (ρ² + s²/t)^{1/2} ≤ γ, since X̄_t ∼ N(0, ρ² + s²/t) under Q and |a| ≤ (a² + v)/(2v^{1/2}) (proof of Lemma S6).

Lemma S6

theorem LogOptimal.measurableSet_lbA (r k : ℕ) (c' : ℝ) : MeasurableSet (lbA r k c')

theorem LogOptimal.log_lbJ_ge {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {r K : ℕ} {c : ℝ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hc : 0 < c) (hc' : 0 < lbCPrime r c) {k : ℕ} (hk : k ≤ K) (x : ℕ → ℝ) : lbBeta s ρ K c - (lbBeta s ρ K c - lbBetaPrime s ρ) * (lbA r k (lbCPrime r c))ᶜ.indicator 1 x - (2 * (c + 1) * |runningMean (r ^ k) x| / √↑(r ^ k) + (c + 1) ^ 2 / ↑(r ^ k)) / (2 * (ρ ^ 2 + s ^ 2)) ≤ Real.log ((↑K + 1) * lbJ s ρ r K c k x)

The pointwise bound of Lemma S6: on A_k, Lemma S5(ii) and (iii) give log{(K + 1)J_k} ≥ β − D_k; on its complement, Lemma S5(i) gives log{(K + 1)J_k} ≥ β'. Both give log{(K + 1)J_k} ≥ β − (β − β')1(Y^t ∉ A_k) − D_k.

theorem LogOptimal.integrable_lbA_indicator (s ρ : ℝ) (r k : ℕ) (c' : ℝ) : MeasureTheory.Integrable ((lbA r k c')ᶜ.indicator 1) (mixAlt s ρ)

theorem LogOptimal.eIntegral_log_lbJ_ge {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {r K : ℕ} {c : ℝ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hc : 0 < c) (hc' : 0 < lbCPrime r c) (hβ : lbBetaPrime s ρ ≤ lbBeta s ρ K c) {k : ℕ} (hk : k ≤ K) : ↑(lbBeta s ρ K c - (lbBeta s ρ K c - lbBetaPrime s ρ) * ↑K * Real.exp (-lbCPrime r c ^ 2 / (2 * s ^ 2)) - (c + 1) / (√(ρ ^ 2 + s ^ 2) * √↑(r ^ k)) - (c + 1) ^ 2 / (2 * (ρ ^ 2 + s ^ 2) * ↑(r ^ k))) ≤ eIntegral (mixAlt s ρ) fun (x : ℕ → ℝ) => (ENNReal.ofReal ((↑K + 1) * lbJ s ρ r K c k x)).log

The expectation in the proof of Lemma S6: since β ≥ β', Q(Y^t ∉ A_k) ≤ K exp{−c'²/(2s²)}, and E_Q(|X̄_t|) ≤ γ, E_Q[log{(K + 1)J_k}] ≥ β − (β − β')K exp{−c'²/(2s²)} − (c + 1)/(γt^{1/2}) − (c + 1)²/(2γ²t).

theorem LogOptimal.lb_sqrt_pow {x : ℝ} (hx : 0 ≤ x) (k : ℕ) : √(x ^ k) = √x ^ k

theorem LogOptimal.lem_fixedk_of_lbmix {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {r K : ℕ} {c : ℝ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hc : 0 < c) {Γ : EReal} (hS8 : (↑(↑K + 1)⁻¹ * ∑ k ∈ Finset.range (K + 1), eIntegral (mixAlt s ρ) fun (x : ℕ → ℝ) => (ENNReal.ofReal ((↑K + 1) * lbJ s ρ r K c k x)).log) ≤ Γ) (hc' : 0 < lbCPrime r c) (hβ : lbBetaPrime s ρ ≤ lbBeta s ρ K c) : ↑(lbBeta s ρ K c - (lbBeta s ρ K c - lbBetaPrime s ρ) * ↑K * Real.exp (-lbCPrime r c ^ 2 / (2 * s ^ 2)) - (2 * (c + 1) / √(ρ ^ 2 + s ^ 2) + 2 * (c + 1) ^ 2 / (3 * √(ρ ^ 2 + s ^ 2) ^ 2)) / (↑K + 1)) ≤ Γ

Lemma S6 (lem:fixedk, Lower bound for fixed K), from inequality (S8) of Lemma S4: if c' > 0 and β ≥ β', then every Γ that satisfies (S8) satisfies (S9), Γ ≥ β − (β − β')K exp{−c'²/(2s²)} − {2(c + 1)/γ + 2(c + 1)²/(3γ²)}/(K + 1).