The density in the proof of Lemma S4

This file computes, following the proof of Lemma S4 of the supplementary material, the density with respect to Q of the part of the mixture P̄ that stops at t = t_k = r^k. Let π = N(0, γ²) with γ² = ρ² + s², ξ_t = 1/(K + 1), and let τ' be the stopping rule of Section S1.6. Since the randomized rule stops at t with probability ½ 1(τ' = t) + ½ ξ_t given (θ, X), the restriction of P̄ to {t} × ℝ^t is ∫ {½ 1(τ' = t) + ½ ξ_t} P_θ π(dθ). We show that this measure has density J_k/Π_t with respect to Q on ℱ_t, where Π_t = ∏_{i=2}^t ℓ(Y_i) is the numéraire E*_t of Proposition 2 when ρ² ≥ 1 − s². As in the paper, densities are written as functions of (x̄_t, y).

• lb_gaussianPDFReal_mul_eq and lb_lintegral_gaussianPDFReal_conv: by completing the square, ∫ φ_v(a − θ)φ_w(θ) dθ = φ_{v+w}(a);
• lb_lintegral_comp_mul_sub and lb_gaussianPDFReal_div_sqrt: the substitution z = c(a − θ), and φ_{1/t}(t^{-1/2}z) = t^{1/2}φ₁(z);
• dataFiltration_le_comap_lb: ℱ_t is generated by (X̄_t, Y^t), by Lemma S2(ii);
• lbJy, lbJ_eq_lbJy, and measurable_lbJy: J_k as a function of (x̄_t, y);
• lb_pi_gaussianReal_eq_withDensity: N(0, s²)^{⊗n} has density ∏_m ℓ(y_m) with respect to N(0, 1)^{⊗n};
• lb_lintegral_theta_eq: for fixed (x̄_t, y), the substitution θ = x̄_t − t^{-1/2}z gives ∫ {½ 1(t^{1/2}(x̄_t − θ) ∈ 𝒵_k(y)) + ½ ξ_t} φ_{1/t}(x̄_t − θ)φ_{γ²}(θ) dθ = φ_{ρ²+s²/t}(x̄_t) J_k;
• lb_lintegral_nullDist_eq and lb_lintegral_mixAlt_eq: integrals of functions of (X̄_t, Y^t) under P_θ and under Q, by Lemma S2(iii);
• lb_lintegral_mixture_left and lb_lintegral_mixture_right: both sides of the density identity equal ∫∫ F(a, y) φ_{ρ²+s²/t}(a) J_k(a, y) da N(0, 1)^{⊗(t−1)}(dy);
• lb_lintegral_mixture_eq: for every ℱ_t-measurable f ≥ 0, ∫ E_θ[{½ 1(τ' = t) + ½ ξ_t} f] π(dθ) = E_Q(f J_k/Π_t).

Gaussian identities

theorem LogOptimal.lb_gaussianPDFReal_mul_eq {v w : ℝ} (hv : 0 < v) (hw : 0 < w) (a θ : ℝ) : ProbabilityTheory.gaussianPDFReal 0 v.toNNReal (a - θ) * ProbabilityTheory.gaussianPDFReal 0 w.toNNReal θ = ProbabilityTheory.gaussianPDFReal 0 (v + w).toNNReal a * ProbabilityTheory.gaussianPDFReal (a * w / (v + w)) (v * w / (v + w)).toNNReal θ

Completing the square: φ_v(a − θ)φ_w(θ) = φ_{v+w}(a)φ_{vw/(v+w)}(θ − aw/(v + w)).

theorem LogOptimal.lb_lintegral_gaussianPDFReal_conv {v w : ℝ} (hv : 0 < v) (hw : 0 < w) (a : ℝ) : ∫⁻ (θ : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 v.toNNReal (a - θ)) * ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 w.toNNReal θ) = ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (v + w).toNNReal a)

Convolution of Gaussian densities: ∫ φ_v(a − θ)φ_w(θ) dθ = φ_{v+w}(a).

theorem LogOptimal.lb_lintegral_comp_mul_sub {c : ℝ} (hc : 0 < c) (a : ℝ) {H : ℝ → ENNReal} (hH : Measurable H) : ∫⁻ (θ : ℝ), H (c * (a - θ)) = ENNReal.ofReal c⁻¹ * ∫⁻ (z : ℝ), H z

The substitution z = c(a − θ) for c > 0.

theorem LogOptimal.lb_gaussianPDFReal_div_sqrt {t : ℝ} (ht : 0 < t) (z : ℝ) : ProbabilityTheory.gaussianPDFReal 0 (1 / t).toNNReal (z / √t) = √t * ProbabilityTheory.gaussianPDFReal 0 1 z

φ_{1/t}(t^{-1/2}z) = t^{1/2}φ₁(z) for t > 0.

ℱ_t is generated by (X̄_t, Y^t)

theorem LogOptimal.lb_measurable_runningMean_comap {t j : ℕ} (hj : 1 ≤ j) (hjt : j ≤ t) : Measurable (runningMean j)

By Lemma S2(ii), x̄_j = x̄_t − ∑_{i=j+1}^t y_i/{i(i − 1)}^{1/2} for 1 ≤ j ≤ t is a function of (x̄_t, Y^t).

theorem LogOptimal.lb_measurable_coord_comap {t i : ℕ} (hi : i < t) : Measurable fun (x : ℕ → ℝ) => x i

theorem LogOptimal.dataFiltration_le_comap_lb (t : ℕ) : ↑(dataFiltration ℝ) t ≤ MeasurableSpace.comap (fun (x : ℕ → ℝ) => (runningMean t x, helmertVec t x)) inferInstance

ℱ_t ≤ σ(X̄_t, Y^t): every observation X_{i+1} = (i + 1)X̄_{i+1} − iX̄_i, i < t, is a function of (X̄_t, Y^t).

J_k and Π_t as functions of (x̄_t, y)

noncomputable def LogOptimal.lbJy (s ρ : ℝ) (r K : ℕ) (c : ℝ) (k : ℕ) (p : ℝ × (Fin (r ^ k - 1) → ℝ)) : ℝ

The function J_k of eq. (S7) as a function of (x̄_t, y), with t = t_k = r^k and y = (y₂, …, y_t).

Equations

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

theorem LogOptimal.lbJ_eq_lbJy {r : ℕ} (hr : 1 ≤ r) (s ρ : ℝ) (K : ℕ) (c : ℝ) (k : ℕ) (x : ℕ → ℝ) : lbJ s ρ r K c k x = lbJy s ρ r K c k (runningMean (r ^ k) x, helmertVec (r ^ k) x)

theorem LogOptimal.measurable_lbJy (s ρ : ℝ) (r K : ℕ) (c : ℝ) (k : ℕ) : Measurable (lbJy s ρ r K c k)

theorem LogOptimal.lb_prod_Icc_eq_prod_fin {t : ℕ} (ht : 1 ≤ t) (f : ℕ → ℝ) : ∏ i ∈ Finset.Icc 2 t, f i = ∏ m : Fin (t - 1), f (↑m + 2)

theorem LogOptimal.lb_prod_lik_helmertY_eq {t : ℕ} (ht : 1 ≤ t) (s : ℝ) (x : ℕ → ℝ) : ∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x) = ∏ m : Fin (t - 1), lik s (helmertVec t x m)

theorem LogOptimal.lb_pi_gaussianReal_eq_withDensity {s : ℝ} (hs : s ≠ 0) (n : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal) = (MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.gaussianReal 0 1).withDensity fun (y : Fin n → ℝ) => ENNReal.ofReal (∏ m : Fin n, lik s (y m))

N(0, s²)^{⊗n} has density ∏_m ℓ(y_m) with respect to N(0, 1)^{⊗n}.

The integral over θ

theorem LogOptimal.lb_integrable_pdf_mul_pdf (g : NNReal) (a T : ℝ) : MeasureTheory.Integrable (fun (z : ℝ) => ProbabilityTheory.gaussianPDFReal 0 1 z * ProbabilityTheory.gaussianPDFReal 0 g (a - z / √T)) MeasureTheory.volume

theorem LogOptimal.lb_lintegral_theta_eq {s ρ : ℝ} (hs : 0 < s) (hρ : 0 < ρ) {r : ℕ} (hr : 1 ≤ r) (K : ℕ) (c : ℝ) (k : ℕ) (a : ℝ) (y : Fin (r ^ k - 1) → ℝ) : ∫⁻ (θ : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (ρ ^ 2 + s ^ 2).toNNReal θ) * (ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (1 / ↑(r ^ k)).toNNReal (a - θ)) * (2⁻¹ * (lbZsety r k c y).indicator 1 (√↑(r ^ k) * (a - θ)) + 2⁻¹ * ENNReal.ofReal (1 / (↑K + 1)))) = ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (ρ ^ 2 + s ^ 2 / ↑(r ^ k)).toNNReal a * lbJy s ρ r K c k (a, y))

The integral over θ (proof of Lemma S4): for fixed (x̄_t, y) = (a, y), the substitution θ = a − t^{-1/2}z and ∫ φ_{1/t}(a − θ)φ_{γ²}(θ) dθ = φ_{γ²+1/t}(a) give ∫ {½ 1(t^{1/2}(a − θ) ∈ 𝒵_k(y)) + ½ ξ_t} φ_{1/t}(a − θ)φ_{γ²}(θ) dθ = φ_{ρ²+s²/t}(a) J_k.

The density of the stopped mixture with respect to Q

theorem LogOptimal.lb_lintegral_gaussianReal (θ : ℝ) {v : ℝ} (hv : 0 < v) (G : ℝ → ENNReal) : ∫⁻ (a : ℝ), G a ∂ProbabilityTheory.gaussianReal θ v.toNNReal = ∫⁻ (a : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 v.toNNReal (a - θ)) * G a

theorem LogOptimal.lb_indicator_lbZsety (r k : ℕ) (c z : ℝ) (y : Fin (r ^ k - 1) → ℝ) : (lbZsety r k c y).indicator 1 z = {p : ℝ × (Fin (r ^ k - 1) → ℝ) | p.1 ∈ lbZsety r k c p.2}.indicator 1 (z, y)

The section {z : (z, y) ∈ S} of S = {(z, y) : z ∈ 𝒵_k(y)} is 𝒵_k(y).

theorem LogOptimal.lb_lintegral_nullDist_eq {t : ℕ} (ht : 1 ≤ t) (θ : ℝ) {Φ : ℝ × (Fin (t - 1) → ℝ) → ENNReal} (hΦ : Measurable Φ) : ∫⁻ (x : ℕ → ℝ), Φ (runningMean t x, helmertVec t x) ∂nullDist θ = ∫⁻ (y : Fin (t - 1) → ℝ), ∫⁻ (a : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (1 / ↑t).toNNReal (a - θ)) * Φ (a, y) ∂MeasureTheory.Measure.pi fun (x : Fin (t - 1)) => ProbabilityTheory.gaussianReal 0 1

Under P_θ, by Lemma S2(iii), integrals of functions of (X̄_t, Y^t) are integrals against φ_{1/t}(x̄_t − θ) dx̄_t N(0, 1)^{⊗(t−1)}(dy).

theorem LogOptimal.lb_lintegral_mixAlt_eq {s : ℝ} (hs : 0 < s) (ρ : ℝ) {t : ℕ} (ht : 1 ≤ t) {Φ : ℝ × (Fin (t - 1) → ℝ) → ENNReal} (hΦ : Measurable Φ) : ∫⁻ (x : ℕ → ℝ), Φ (runningMean t x, helmertVec t x) ∂mixAlt s ρ = ∫⁻ (y : Fin (t - 1) → ℝ), ENNReal.ofReal (∏ m : Fin (t - 1), lik s (y m)) * ∫⁻ (a : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (ρ ^ 2 + s ^ 2 / ↑t).toNNReal a) * Φ (a, y) ∂MeasureTheory.Measure.pi fun (x : Fin (t - 1)) => ProbabilityTheory.gaussianReal 0 1

Under Q, integrals of functions of (X̄_t, Y^t) are integrals against φ_{ρ²+s²/t}(x̄_t) dx̄_t N(0, s²)^{⊗(t−1)}(dy), and N(0, s²)^{⊗(t−1)} has density ∏_m ℓ(y_m) with respect to N(0, 1)^{⊗(t−1)}.

theorem LogOptimal.lb_lintegral_mixture_left {s ρ : ℝ} (hs : 0 < s) (hρ : 0 < ρ) {r : ℕ} (hr : 1 ≤ r) (K : ℕ) (c : ℝ) (k : ℕ) {F : ℝ × (Fin (r ^ k - 1) → ℝ) → ENNReal} (hF : Measurable F) : ∫⁻ (θ : ℝ), ∫⁻ (x : ℕ → ℝ), (2⁻¹ * (lbZsety r k c (helmertVec (r ^ k) x)).indicator 1 (√↑(r ^ k) * (runningMean (r ^ k) x - θ)) + 2⁻¹ * ENNReal.ofReal (1 / (↑K + 1))) * F (runningMean (r ^ k) x, helmertVec (r ^ k) x) ∂nullDist θ ∂ProbabilityTheory.gaussianReal 0 (ρ ^ 2 + s ^ 2).toNNReal = ∫⁻ (y : Fin (r ^ k - 1) → ℝ), ∫⁻ (a : ℝ), F (a, y) * ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (ρ ^ 2 + s ^ 2 / ↑(r ^ k)).toNNReal a * lbJy s ρ r K c k (a, y)) ∂MeasureTheory.Measure.pi fun (x : Fin (r ^ k - 1)) => ProbabilityTheory.gaussianReal 0 1

The left-hand side of the density identity (proof of Lemma S4): for measurable F, ∫ E_θ[{½ 1(t^{1/2}(X̄_t − θ) ∈ 𝒵_k(Y^t)) + ½ ξ_t} F(X̄_t, Y^t)] π(dθ) = ∫∫ F(a, y) φ_{ρ²+s²/t}(a) J_k(a, y) da N(0, 1)^{⊗(t−1)}(dy), by Fubini's theorem and lb_lintegral_theta_eq.

theorem LogOptimal.lb_lintegral_mixture_right {s : ℝ} (hs : 0 < s) (ρ : ℝ) {r : ℕ} (hr : 1 ≤ r) (K : ℕ) (c : ℝ) (k : ℕ) {F : ℝ × (Fin (r ^ k - 1) → ℝ) → ENNReal} (hF : Measurable F) : ∫⁻ (x : ℕ → ℝ), F (runningMean (r ^ k) x, helmertVec (r ^ k) x) * (ENNReal.ofReal (lbJ s ρ r K c k x) / ENNReal.ofReal (∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x))) ∂mixAlt s ρ = ∫⁻ (y : Fin (r ^ k - 1) → ℝ), ∫⁻ (a : ℝ), F (a, y) * ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 (ρ ^ 2 + s ^ 2 / ↑(r ^ k)).toNNReal a * lbJy s ρ r K c k (a, y)) ∂MeasureTheory.Measure.pi fun (x : Fin (r ^ k - 1)) => ProbabilityTheory.gaussianReal 0 1

The right-hand side of the density identity (proof of Lemma S4): for measurable F, E_Q{F(X̄_t, Y^t) J_k/Π_t} = ∫∫ F(a, y) φ_{ρ²+s²/t}(a) J_k(a, y) da N(0, 1)^{⊗(t−1)}(dy), since Π_t = ∏_{i=2}^t ℓ(Y_i) is the density of N(0, s²)^{⊗(t−1)} with respect to N(0, 1)^{⊗(t−1)}.

theorem LogOptimal.lb_indicator_lbStoppingRule_eq {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) (c θ : ℝ) (x : ℕ → ℝ) : {x : ℕ → ℝ | lbStoppingRule r K c θ x = ↑(r ^ k)}.indicator 1 x = (lbZsety r k c (helmertVec (r ^ k) x)).indicator 1 (√↑(r ^ k) * (runningMean (r ^ k) x - θ))

1(τ' = t) = 1{t^{1/2}(X̄_t − θ) ∈ 𝒵_k(Y^t)} for t = t_k, by Lemma S2(ii).

theorem LogOptimal.lb_lintegral_mixture_eq {s ρ : ℝ} (hs : 0 < s) (hρ : 0 < ρ) {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) (c : ℝ) {f : (ℕ → ℝ) → ENNReal} (hf : Measurable f) : ∫⁻ (θ : ℝ), ∫⁻ (x : ℕ → ℝ), (2⁻¹ * {x : ℕ → ℝ | lbStoppingRule r K c θ x = ↑(r ^ k)}.indicator 1 x + 2⁻¹ * ENNReal.ofReal (1 / (↑K + 1))) * f x ∂nullDist θ ∂ProbabilityTheory.gaussianReal 0 (ρ ^ 2 + s ^ 2).toNNReal = ∫⁻ (x : ℕ → ℝ), f x * (ENNReal.ofReal (lbJ s ρ r K c k x) / ENNReal.ofReal (∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x))) ∂mixAlt s ρ

The density in the proof of Lemma S4: for every ℱ_t-measurable f ≥ 0, with t = t_k = r^k, π = N(0, γ²), and ξ_t = 1/(K + 1), ∫ E_θ[{½ 1(τ' = t) + ½ ξ_t} f] π(dθ) = E_Q(f J_k/Π_t). Both sides equal ∫∫ F(a, y) φ_{ρ²+s²/t}(a) J_k(a, y) da N(0, 1)^{⊗(t−1)}(dy) with f = F(X̄_t, Y^t).