The distributions of (X̄_t, Y^t), and the stopping rule as a function of (Z_t, Y^t)

This file computes the distributions of (X̄_t, Y^t) under P_θ and under the mixture Q, writes W_{jk}, 𝒵_k, and p_k as functions of Y^t = (Y₂, …, Y_t), and proves the claims of Section S1.6 of the supplementary material after Lemma S5 (sec_lb_stopping_proof): under P_θ, Z_t = t^{1/2}(X̄_t − θ) ∼ N(0, 1) is independent of Y^t, so that p_k(Y^t) is the conditional probability that τ' = t given Y^t, where t = t_k = r^k.

• lb_map_runningMean_helmertVec: by Lemma S2(iii), the distribution of (X̄_t, Y^t) under N(m, v)^{⊗∞} is N(m, v/t) ⊗ N(0, v)^{⊗(t−1)};
• map_lbZ_helmertVec: the distribution of (Z_t, Y^t) under P_θ is N(0, 1) ⊗ N(0, 1)^{⊗(t−1)};
• lb_mixAlt_map_runningMean_helmertVec: by ∫ N(μ, v) N(0, w)(dμ) = N(0, w + v) (gaussianReal_bind_gaussianReal), the distribution of (X̄_t, Y^t) under Q is N(0, ρ² + s²/t) ⊗ N(0, s²)^{⊗(t−1)};
• lbYCoord, lbWy, lbZsety: the coordinates y_i, the variables W_{jk}(y), and the sets 𝒵_k(y) as functions of the vector y = (y₂, …, y_t), with lbW_eq_lbWy and lbZset_eq_lbZsety;
• measurableSet_lbZsety: the set {(z, y) : z ∈ 𝒵_k(y)} is measurable;
• lbP_eq and measurable_lbP: p_k(Y^t) = N(0, 1){𝒵_k(Y^t)}, a function of Y^t;
• setOf_lbStoppingRule_eq: {τ' = t} = {Z_t ∈ 𝒵_k(Y^t)}, by Lemma S2(ii);
• lintegral_lbP_eq: E_θ{1(Y^t ∈ B)p_k(Y^t)} = P_θ(Y^t ∈ B, τ' = t);
• sec_lb_stopping_proof: the two claims of Section S1.6 after Lemma S5.

The distribution of (X̄_t, Y^t)

theorem LogOptimal.lb_measurable_helmertVec (t : ℕ) : Measurable (helmertVec t)

theorem LogOptimal.lb_map_runningMean_helmertVec {t : ℕ} (ht : 1 ≤ t) (m : ℝ) (v : NNReal) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) => (runningMean t x, helmertVec t x)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v) = (ProbabilityTheory.gaussianReal m (v / ↑t)).prod (MeasureTheory.Measure.pi fun (x : Fin (t - 1)) => ProbabilityTheory.gaussianReal 0 v)

Lemma S2(iii): under N(m, v)^{⊗∞}, the vector (X̄_t, Y^t) has distribution N(m, v/t) ⊗ N(0, v)^{⊗(t−1)} for t ≥ 1.

theorem LogOptimal.measurable_lbZ (θ : ℝ) (t : ℕ) : Measurable (lbZ θ t)

theorem LogOptimal.map_lbZ_helmertVec {t : ℕ} (ht : 1 ≤ t) (θ : ℝ) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) => (lbZ θ t x, helmertVec t x)) (nullDist θ) = (ProbabilityTheory.gaussianReal 0 1).prod (MeasureTheory.Measure.pi fun (x : Fin (t - 1)) => ProbabilityTheory.gaussianReal 0 1)

Under P_θ, Z_t = t^{1/2}(X̄_t − θ) ∼ N(0, 1) and Y^t ∼ N(0, 1)^{⊗(t−1)} are independent: the distribution of (Z_t, Y^t) is N(0, 1) ⊗ N(0, 1)^{⊗(t−1)} for t ≥ 1.

The distribution of (X̄_t, Y^t) under the mixture Q

theorem LogOptimal.lb_measurable_runningMean_helmertVec (t : ℕ) : Measurable fun (x : ℕ → ℝ) => (runningMean t x, helmertVec t x)

The Gaussian mixture ∫ N(μ, v) N(0, w)(dμ) is N(0, w + v), the convolution N(0, w) ∗ N(0, v).

theorem LogOptimal.lb_mixAlt_map_runningMean_helmertVec {t : ℕ} (ht : 1 ≤ t) (s ρ : ℝ) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) => (runningMean t x, helmertVec t x)) (mixAlt s ρ) = (ProbabilityTheory.gaussianReal 0 (ρ ^ 2 + s ^ 2 / ↑t).toNNReal).prod (MeasureTheory.Measure.pi fun (x : Fin (t - 1)) => ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal)

Under the mixture Q = ∫ Q_μ N(0, ρ²)(dμ), the vector (X̄_t, Y^t) has distribution N(0, ρ² + s²/t) ⊗ N(0, s²)^{⊗(t−1)} for t ≥ 1: by Lemma S2(iii), Y^t has the same distribution under every Q_μ, and X̄_t ∼ N(μ, s²/t) is mixed over μ ∼ N(0, ρ²).

W_{jk} and 𝒵_k as functions of y = (y₂, …, y_t)

noncomputable def LogOptimal.lbYCoord (t i : ℕ) (y : Fin (t - 1) → ℝ) : ℝ

The coordinate y_i of the vector y = (y₂, …, y_t), indexed by Fin (t − 1), for 2 ≤ i ≤ t; the value for other i plays no role.

Equations

• LogOptimal.lbYCoord t i y = if h : i - 2 < t - 1 then y ⟨i - 2, h⟩ else 0

theorem LogOptimal.lbYCoord_helmertVec {t i : ℕ} (hi : 2 ≤ i) (hit : i ≤ t) (x : ℕ → ℝ) : lbYCoord t i (helmertVec t x) = helmertY i x

theorem LogOptimal.measurable_lbYCoord (t i : ℕ) : Measurable (lbYCoord t i)

noncomputable def LogOptimal.lbWy (r j k : ℕ) (y : Fin (r ^ k - 1) → ℝ) : ℝ

The variable W_{jk}(y) = t_j^{1/2} ∑_{i=t_j+1}^{t_k} y_i/{i(i − 1)}^{1/2} of Section S1.6, as a function of y = (y₂, …, y_t) with t = t_k = r^k.

Equations

• LogOptimal.lbWy r j k y = √(↑r ^ j) * ∑ i ∈ Finset.Ioc (r ^ j) (r ^ k), LogOptimal.lbYCoord (r ^ k) i y / √(↑i * (↑i - 1))

theorem LogOptimal.measurable_lbWy (r j k : ℕ) : Measurable (lbWy r j k)

theorem LogOptimal.lbW_eq_lbWy {r : ℕ} (hr : 1 ≤ r) (j k : ℕ) (x : ℕ → ℝ) : lbW r j k x = lbWy r j k (helmertVec (r ^ k) x)

noncomputable def LogOptimal.lbZsety (r k : ℕ) (c : ℝ) (y : Fin (r ^ k - 1) → ℝ) : Set ℝ

The set 𝒵_k(y) of Section S1.6, as a function of y = (y₂, …, y_t) with t = t_k = r^k.

Equations

• One or more equations did not get rendered due to their size.

theorem LogOptimal.lbZset_eq_lbZsety {r : ℕ} (hr : 1 ≤ r) (k : ℕ) (c : ℝ) (x : ℕ → ℝ) : lbZset r k c x = lbZsety r k c (helmertVec (r ^ k) x)

theorem LogOptimal.measurableSet_lbZsety (r k : ℕ) (c : ℝ) : MeasurableSet {p : ℝ × (Fin (r ^ k - 1) → ℝ) | p.1 ∈ lbZsety r k c p.2}

The set {(z, y) : z ∈ 𝒵_k(y)} is measurable.

theorem LogOptimal.measurableSet_lbZsety_section (r k : ℕ) (c : ℝ) (y : Fin (r ^ k - 1) → ℝ) : MeasurableSet (lbZsety r k c y)

theorem LogOptimal.lbP_eq {r : ℕ} (hr : 1 ≤ r) (k : ℕ) (c : ℝ) (x : ℕ → ℝ) : lbP r k c x = ((ProbabilityTheory.gaussianReal 0 1) (lbZsety r k c (helmertVec (r ^ k) x))).toReal

p_k(y) = ∫_{𝒵_k(y)} φ₁(z) dz = N(0, 1){𝒵_k(y)}.

theorem LogOptimal.measurable_lbP {r : ℕ} (hr : 1 ≤ r) (k : ℕ) (c : ℝ) : Measurable (lbP r k c)

theorem LogOptimal.setOf_lbStoppingRule_eq {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) (c θ : ℝ) : {x : ℕ → ℝ | lbStoppingRule r K c θ x = ↑(r ^ k)} = (fun (x : ℕ → ℝ) => (lbZ θ (r ^ k) x, helmertVec (r ^ k) x)) ⁻¹' {p : ℝ × (Fin (r ^ k - 1) → ℝ) | p.1 ∈ lbZsety r k c p.2}

{τ' = t} = {Z_t ∈ 𝒵_k(Y^t)} for t = t_k, by Lemma S2(ii).

Section S1.6: the stopping rule τ' and p_k(Y^t)

theorem LogOptimal.lbP_le_one {r : ℕ} (hr : 1 ≤ r) (k : ℕ) (c : ℝ) (x : ℕ → ℝ) : lbP r k c x ≤ 1

theorem LogOptimal.lintegral_lbP_eq {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) (c θ : ℝ) {B : Set (Fin (r ^ k - 1) → ℝ)} (hB : MeasurableSet B) : ∫⁻ (x : ℕ → ℝ) in helmertVec (r ^ k) ⁻¹' B, ENNReal.ofReal (lbP r k c x) ∂nullDist θ = ∫⁻ (x : ℕ → ℝ) in helmertVec (r ^ k) ⁻¹' B, ENNReal.ofReal ({x : ℕ → ℝ | lbStoppingRule r K c θ x = ↑(r ^ k)}.indicator 1 x) ∂nullDist θ

Under P_θ, for a measurable set B of values of Y^t, both E_θ{1(Y^t ∈ B)p_k(Y^t)} and P_θ(Y^t ∈ B, τ' = t) equal ∫_B N(0, 1){𝒵_k(y)} N(0, 1)^{⊗(t−1)}(dy), since Z_t ∼ N(0, 1) is independent of Y^t.

theorem LogOptimal.sec_lb_stopping_proof (r K : ℕ) (c θ : ℝ) : 4 ≤ r → 1 ≤ K → 0 < c → ∀ k ≤ K, have t := r ^ k; (nullDist θ)[{x : ℕ → ℝ | lbStoppingRule r K c θ x = ↑t}.indicator 1 | MeasurableSpace.comap (helmertVec t) inferInstance] =ᵐ[nullDist θ] lbP r k c ∧ (0 < lbCPrime r c → ∀ x ∈ lbA r k (lbCPrime r c), c ≤ |lbZ θ t x| → |lbZ θ t x| ≤ c + 1 → lbStoppingRule r K c θ x = ↑t)