The distribution of (X̄_t, Y^t) under mixtures, and the density dQ_t/dP*_t

This file computes, following the proof of Proposition 2 of the paper (Section S1.4), the distribution of the running mean X̄_t and of the vector Y^t = (Y₂, …, Y_t) under the null distributions, the alternatives, and their mixtures over the location, and deduces the density of Q_t with respect to a mixture of null distributions of X^t. The paper integrates eq. (S2) over the mixing distributions; here the same computation is done on the distribution of (X̄_t, Y^t), which is a product by Lemma S2(iii), and is pulled back to X^t through the injective linear map x^t ↦ (x̄_t, y₂, …, y_t).

• ∫ N(θ, b) N(m, a)(dθ) = N(m, a + b), the convolution of normal distributions (private);
• meanHelmertPair t: the pair (X̄_t, Y^t), and map_meanHelmertPair_infinitePi and map_meanHelmertPair_bind its distribution under N(m, v)^{⊗∞} and under the mixtures ∫ N(m, v)^{⊗∞} ν(dm), the product of ∫ N(m, v/t) ν(dm) and N(0, v)^{⊗(t−1)};
• meanHelmertFin t: the same map on ℝ^t, and measurableEmbedding_meanHelmertFin: it is a measurable embedding, since it is linear and injective;
• pi_gaussianReal_eq_withDensity_lik: N(0, s²)^{⊗n} has density ∏_j ℓ(u_j) with respect to N(0, 1)^{⊗n};
• marginal_bind_altDist_eq_withDensity: if the mixtures of N(θ, 1/t) and of N(μ, s²/t) coincide, then the distribution of X^t under ∫ Q_μ ν'(dμ) has density ∏_{i=2}^t ℓ(y_i) with respect to the mixture ∫ P_{θ,t} ν(dθ);
• marginal_mixAlt_eq_withDensity and marginal_altDist_eq_withDensity_of_one_le: the two cases used for Propositions 2 and S4(ii), with the mixing distributions N{0, ρ² − (1 − s²)/t} and N{μ, (s² − 1)/t};
• altDist_map_helmertY_eq_gaussianReal, mixAlt_map_helmertY_eq_gaussianReal, map_helmertVec_altDist_eq_pi, map_helmertVec_mixAlt_eq_pi, map_helmertVec_nullDist_eq_pi: under every Q_μ and under Q, Y_i ∼ N(0, s²) and Y^t ∼ N(0, s²)^{⊗(t−1)}, while Y^t ∼ N(0, 1)^{⊗(t−1)} under every P_θ;
• sec4_mixture_mean_proof and sec4_maximal_invariant_proof: the claims of Section 4.1 on the running mean under P*_t and on the likelihood ratio of the maximal invariant.

Mixtures of normal distributions

The pair (X̄_t, Y^t)

noncomputable def LogOptimal.meanHelmertPair (t : ℕ) (x : ℕ → ℝ) : ℝ × (Fin (t - 1) → ℝ)

The pair (X̄_t, Y^t) of the running mean and of the vector Y^t = (Y₂, …, Y_t).

Equations

• LogOptimal.meanHelmertPair t x = (LogOptimal.runningMean t x, LogOptimal.helmertVec t x)

theorem LogOptimal.measurable_meanHelmertPair (t : ℕ) : Measurable (meanHelmertPair t)

theorem LogOptimal.map_meanHelmertPair_infinitePi {t : ℕ} (ht : 1 ≤ t) (m : ℝ) (v : NNReal) : MeasureTheory.Measure.map (meanHelmertPair t) (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) for the pair: under N(m, v)^{⊗∞} and for t ≥ 1, the distribution of (X̄_t, Y^t) is the product of N(m, v/t) and N(0, v)^{⊗(t−1)}.

theorem LogOptimal.map_meanHelmertPair_bind {t : ℕ} (ht : 1 ≤ t) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν] (v : NNReal) : MeasureTheory.Measure.map (meanHelmertPair t) (ν.bind fun (m : ℝ) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v) = (ν.bind fun (m : ℝ) => ProbabilityTheory.gaussianReal m (v / ↑t)).prod (MeasureTheory.Measure.pi fun (x : Fin (t - 1)) => ProbabilityTheory.gaussianReal 0 v)

Under the mixture ∫ N(m, v)^{⊗∞} ν(dm) and for t ≥ 1, the distribution of (X̄_t, Y^t) is the product of the mixture ∫ N(m, v/t) ν(dm) and of N(0, v)^{⊗(t−1)}.

The map x^t ↦ (x̄_t, y₂, …, y_t) on ℝ^t

def LogOptimal.finToPath {t : ℕ} (y : Fin t → ℝ) (i : ℕ) : ℝ

The path that extends y ∈ ℝ^t by zeros.

Equations

• LogOptimal.finToPath y i = if h : i < t then y ⟨i, h⟩ else 0

theorem LogOptimal.finToPath_restrict {t : ℕ} (x : ℕ → ℝ) {i : ℕ} (hi : i < t) : finToPath (fun (j : Fin t) => x ↑j) i = x i

noncomputable def LogOptimal.meanHelmertFin (t : ℕ) (y : Fin t → ℝ) : ℝ × (Fin (t - 1) → ℝ)

The map x^t ↦ (x̄_t, y₂, …, y_t) on ℝ^t.

Equations

• LogOptimal.meanHelmertFin t y = LogOptimal.meanHelmertPair t (LogOptimal.finToPath y)

theorem LogOptimal.meanHelmertFin_restrict (t : ℕ) (x : ℕ → ℝ) : (meanHelmertFin t fun (i : Fin t) => x ↑i) = meanHelmertPair t x

noncomputable def LogOptimal.meanHelmertLinear (t : ℕ) : (Fin t → ℝ) →ₗ[ℝ] ℝ × (Fin (t - 1) → ℝ)

The map x^t ↦ (x̄_t, y₂, …, y_t) as a linear map.

Equations

• LogOptimal.meanHelmertLinear t = { toFun := LogOptimal.meanHelmertFin t, map_add' := ⋯, map_smul' := ⋯ }

theorem LogOptimal.ker_meanHelmertLinear (t : ℕ) : (meanHelmertLinear t).ker = ⊥

The map x^t ↦ (x̄_t, y₂, …, y_t) is injective: if y₂, …, y_t vanish, then x^t is constant by maximal invariance, and the constant is x̄_t.

theorem LogOptimal.measurableEmbedding_meanHelmertFin (t : ℕ) : MeasurableEmbedding (meanHelmertFin t)

The map x^t ↦ (x̄_t, y₂, …, y_t) is a measurable embedding, as an injective linear map on a finite-dimensional space.

theorem LogOptimal.map_marginal_meanHelmertFin (P : MeasureTheory.Measure (ℕ → ℝ)) (t : ℕ) : MeasureTheory.Measure.map (meanHelmertFin t) (marginal P t) = MeasureTheory.Measure.map (meanHelmertPair t) P

The density of Q_t with respect to a mixture of null distributions

theorem LogOptimal.pi_gaussianReal_eq_withDensity_lik {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 (u : Fin n → ℝ) => ENNReal.ofReal (∏ j : Fin n, lik s (u j))

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

theorem LogOptimal.measurable_ofReal_prod_lik (s : ℝ) (n : ℕ) : Measurable fun (u : Fin n → ℝ) => ENNReal.ofReal (∏ j : Fin n, lik s (u j))

theorem LogOptimal.measurable_ofReal_prod_lik_snd (s : ℝ) (n : ℕ) : Measurable fun (w : ℝ × (Fin n → ℝ)) => ENNReal.ofReal (∏ j : Fin n, lik s (w.2 j))

theorem LogOptimal.marginal_bind_altDist_eq_withDensity {s : ℝ} (hs : s ≠ 0) {t : ℕ} (ht : 1 ≤ t) (ν ν' : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure ν'] (hνν' : (ν.bind fun (θ : ℝ) => ProbabilityTheory.gaussianReal θ (1 / ↑t)) = ν'.bind fun (μ : ℝ) => ProbabilityTheory.gaussianReal μ ((s ^ 2).toNNReal / ↑t)) : marginal (ν'.bind (altDist s)) t = (ν.bind fun (θ : ℝ) => marginal (nullDist θ) t).withDensity fun (y : Fin t → ℝ) => ENNReal.ofReal (∏ j : Fin (t - 1), lik s ((meanHelmertFin t y).2 j))

The density of Q_t (proof of Proposition 2): if the mixtures ∫ N(θ, 1/t) ν(dθ) and ∫ N(μ, s²/t) ν'(dμ) coincide, then the distribution of X^t under ∫ Q_μ ν'(dμ) has density ∏_{i=2}^t ℓ(y_i) with respect to the mixture ∫ P_{θ,t} ν(dθ). Indeed, the distributions of (X̄_t, Y^t) under the two measures are the products of the same first factor with N(0, s²)^{⊗(t−1)} and N(0, 1)^{⊗(t−1)}.

theorem LogOptimal.prod_Icc_two_eq_prod_fin (t : ℕ) (f : ℕ → ℝ) : ∏ i ∈ Finset.Icc 2 t, f i = ∏ j : Fin (t - 1), f (↑j + 2)

∏_{i=2}^t f(i) = ∏_{j=0}^{t−2} f(j + 2), the product over the coordinates of Y^t.

theorem LogOptimal.gaussNumeraire_eq_comp (s : ℝ) (t : ℕ) (x : ℕ → ℝ) : gaussNumeraire s t x = ENNReal.ofReal (∏ j : Fin (t - 1), lik s ((meanHelmertFin t fun (i : Fin t) => x ↑i).2 j))

E*_t = ∏_{i=2}^t ℓ(Y_i) is the function y ↦ ∏_{i=2}^t ℓ(y_i) of X^t.

theorem LogOptimal.measurable_ofReal_prod_lik_meanHelmertFin (s : ℝ) (t : ℕ) : Measurable fun (y : Fin t → ℝ) => ENNReal.ofReal (∏ j : Fin (t - 1), lik s ((meanHelmertFin t y).2 j))

theorem LogOptimal.mixVar_nonneg {s ρ : ℝ} (hρ : 1 - s ^ 2 ≤ ρ ^ 2) {t : ℕ} (ht : 1 ≤ t) : 0 ≤ ρ ^ 2 - (1 - s ^ 2) / ↑t

For ρ² ≥ 1 − s², the mixing variance ρ² − (1 − s²)/t of P*_t is nonnegative for every t ≥ 1.

theorem LogOptimal.marginal_mixAlt_eq_withDensity {s ρ : ℝ} (hs : s ≠ 0) (hρ : 1 - s ^ 2 ≤ ρ ^ 2) {t : ℕ} (ht : 1 ≤ t) : marginal (mixAlt s ρ) t = ((ProbabilityTheory.gaussianReal 0 (ρ ^ 2 - (1 - s ^ 2) / ↑t).toNNReal).bind fun (θ : ℝ) => marginal (nullDist θ) t).withDensity fun (y : Fin t → ℝ) => ENNReal.ofReal (∏ j : Fin (t - 1), lik s ((meanHelmertFin t y).2 j))

The density of Q_t with respect to P*_t (Proposition 2): for ρ² ≥ 1 − s² and t ≥ 1, Q_t has density ∏_{i=2}^t ℓ(y_i) with respect to P*_t = ∫ P_{θ,t} N{0, ρ² − (1 − s²)/t}(dθ), since both mixtures of the running mean are N(0, ρ² + s²/t).

theorem LogOptimal.marginal_altDist_eq_withDensity_of_one_le {s : ℝ} (hs : 1 ≤ s) (μ : ℝ) {t : ℕ} (ht : 1 ≤ t) : marginal (altDist s μ) t = ((ProbabilityTheory.gaussianReal μ ((s ^ 2 - 1) / ↑t).toNNReal).bind fun (θ : ℝ) => marginal (nullDist θ) t).withDensity fun (y : Fin t → ℝ) => ENNReal.ofReal (∏ j : Fin (t - 1), lik s ((meanHelmertFin t y).2 j))

The density of Q_{μ,t} for s ≥ 1 (Proposition S4(ii)): Q_{μ,t} has density ∏_{i=2}^t ℓ(y_i) with respect to ∫ P_{θ,t} N{μ, (s² − 1)/t}(dθ), since both mixtures of the running mean are N(μ, s²/t).

The distributions of Y_i, Y^t, and X̄_t

theorem LogOptimal.altDist_map_helmertY_eq_gaussianReal (s μ : ℝ) {i : ℕ} (hi : 2 ≤ i) : MeasureTheory.Measure.map (helmertY i) (altDist s μ) = ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal

Under Q_μ, Y_i ∼ N(0, s²) for i ≥ 2 (Lemma S2(iii)).

theorem LogOptimal.mixAlt_map_helmertY_eq_gaussianReal (s ρ : ℝ) {i : ℕ} (hi : 2 ≤ i) : MeasureTheory.Measure.map (helmertY i) (mixAlt s ρ) = ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal

Under the mixture Q, Y_i ∼ N(0, s²) for i ≥ 2, since this holds under every Q_μ.

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

Under every P_θ and for t ≥ 1, Y^t ∼ N(0, 1)^{⊗(t−1)}.

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

Under every Q_μ and for t ≥ 1, Y^t ∼ N(0, s²)^{⊗(t−1)}.

theorem LogOptimal.map_helmertVec_mixAlt_eq_pi {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 the mixture Q and for t ≥ 1, Y^t ∼ N(0, s²)^{⊗(t−1)}.

The claims of Section 4.1

theorem LogOptimal.map_mean_mixAlt (s ρ : ℝ) {t : ℕ} (ht : 1 ≤ t) : MeasureTheory.Measure.map (fun (y : Fin t → ℝ) => (∑ i : Fin t, y i) / ↑t) (marginal (mixAlt s ρ) t) = ProbabilityTheory.gaussianReal 0 (ρ ^ 2 + s ^ 2 / ↑t).toNNReal

theorem LogOptimal.map_mean_mixNull {s ρ : ℝ} (hρ : 1 - s ^ 2 ≤ ρ ^ 2) {t : ℕ} (ht : 1 ≤ t) : MeasureTheory.Measure.map (fun (y : Fin t → ℝ) => (∑ i : Fin t, y i) / ↑t) ((ProbabilityTheory.gaussianReal 0 (ρ ^ 2 - (1 - s ^ 2) / ↑t).toNNReal).bind fun (θ : ℝ) => marginal (nullDist θ) t) = ProbabilityTheory.gaussianReal 0 (ρ ^ 2 + s ^ 2 / ↑t).toNNReal

theorem LogOptimal.sec4_mixture_mean_proof (s ρ : ℝ) : 0 < s → 0 ≤ ρ → 1 - s ^ 2 ≤ ρ ^ 2 → ∀ (t : ℕ), 1 ≤ t → MeasureTheory.Measure.map (fun (y : Fin t → ℝ) => (∑ i : Fin t, y i) / ↑t) ((ProbabilityTheory.gaussianReal 0 (ρ ^ 2 - (1 - s ^ 2) / ↑t).toNNReal).bind fun (θ : ℝ) => marginal (nullDist θ) t) = MeasureTheory.Measure.map (fun (y : Fin t → ℝ) => (∑ i : Fin t, y i) / ↑t) (marginal (mixAlt s ρ) t) ∧ MeasureTheory.Measure.map (fun (y : Fin t → ℝ) => (∑ i : Fin t, y i) / ↑t) (marginal (mixAlt s ρ) t) = ProbabilityTheory.gaussianReal 0 (ρ ^ 2 + s ^ 2 / ↑t).toNNReal

theorem LogOptimal.sec4_maximal_invariant_proof : (∀ (t : ℕ) (x x' : ℕ → ℝ), (∀ (i : ℕ), 2 ≤ i → i ≤ t → helmertY i x = helmertY i x') ↔ ∃ (m : ℝ), ∀ i < t, x' i = x i + m) ∧ ∀ (s ρ θ : ℝ), 0 < s → 0 ≤ ρ → 1 - s ^ 2 ≤ ρ ^ 2 → ∀ (t : ℕ), 1 ≤ t → MeasureTheory.Measure.map (helmertVec t) (mixAlt s ρ) = (MeasureTheory.Measure.map (helmertVec t) (nullDist θ)).withDensity fun (y : Fin (t - 1) → ℝ) => ENNReal.ofReal (∏ i : Fin (t - 1), lik s (y i))