Lemma S2(iii): the distribution of the running mean and of the variables Y_i

This file proves Lemma S2(iii) of the supplementary material, following its proof: since the image of a normal distribution with covariance v times the identity under an orthogonal map is normal with the same covariance, Lemma S2(i) gives Lemma S2(iii). The orthogonal map is the Helmert map x ↦ (⟨ω₁, x⟩, …, ⟨ω_t, x⟩) = (t^{1/2} x̄_t, −y₂, …, −y_t) of Helmert.lean, and the invariance of the standard Gaussian measure under linear isometries is stdGaussian_map of Mathlib. The vector X^t ∼ N(m, v)^{⊗t} is written m + v^{1/2} Z^t with Z^t ∼ N(0, 1)^{⊗t}.

• helmertMap t: the Helmert map in coordinates;
• map_helmertMap_pi_gaussianReal: the Helmert map preserves N(0, 1)^{⊗t};
• infinitePi_map_fin: the distribution of X^t under ν^{⊗∞} is ν^{⊗t};
• gaussianReal_map_affine and infinitePi_gaussianReal_eq_map_affine: N(m, c²) and N(m, v)^{⊗∞} as images of N(0, 1) and N(0, 1)^{⊗∞} under affine maps;
• helmertFamily t: the family (X̄_t, Y₂, …, Y_t) indexed by Fin t, and map_helmertFamily its distribution under N(m, v)^{⊗∞}, a product measure;
• iIndepFun_helmertFamily: under N(m, v)^{⊗∞}, the variables X̄_t, Y₂, …, Y_t are independent, with X̄_t ∼ N(m, v/t) and Y_i ∼ N(0, v);
• lem_orth_proof: Lemma S2.

The Helmert map preserves the standard Gaussian measure

noncomputable def LogOptimal.helmertMap (t : ℕ) (y : Fin t → ℝ) : Fin t → ℝ

The Helmert map y ↦ (⟨ω₁, y⟩, …, ⟨ω_t, y⟩) of ℝ^t, the coordinates of y in the Helmert basis.

Equations

• LogOptimal.helmertMap t y = ((LogOptimal.helmertBasis t).repr (WithLp.toLp 2 y)).ofLp

theorem LogOptimal.helmertMap_apply (t : ℕ) (y : Fin t → ℝ) (j : Fin t) : helmertMap t y j = inner ℝ (helmertRow t j) (WithLp.toLp 2 y)

theorem LogOptimal.measurable_helmertMap (t : ℕ) : Measurable (helmertMap t)

theorem LogOptimal.map_helmertMap_pi_gaussianReal (t : ℕ) : MeasureTheory.Measure.map (helmertMap t) (MeasureTheory.Measure.pi fun (x : Fin t) => ProbabilityTheory.gaussianReal 0 1) = MeasureTheory.Measure.pi fun (x : Fin t) => ProbabilityTheory.gaussianReal 0 1

The orthogonal Helmert map preserves the standard Gaussian measure N(0, 1)^{⊗t}.

Finite-dimensional distributions of N(m, v)^{⊗∞}

theorem LogOptimal.infinitePi_map_fin (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν] (t : ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) (k : Fin t) => x ↑k) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ν) = MeasureTheory.Measure.pi fun (x : Fin t) => ν

The distribution of X^t = (X₁, …, X_t) under ν^{⊗∞} is ν^{⊗t}.

theorem LogOptimal.gaussianReal_map_affine (m c : ℝ) : MeasureTheory.Measure.map (fun (z : ℝ) => m + c * z) (ProbabilityTheory.gaussianReal 0 1) = ProbabilityTheory.gaussianReal m ⟨c ^ 2, ⋯⟩

The image of N(0, 1) under z ↦ m + c z is N(m, c²).

theorem LogOptimal.infinitePi_gaussianReal_eq_map_affine (m : ℝ) (v : NNReal) : (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v) = MeasureTheory.Measure.map (fun (z : ℕ → ℝ) (i : ℕ) => m + √↑v * z i) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal 0 1)

N(m, v)^{⊗∞} is the image of N(0, 1)^{⊗∞} under z ↦ m + v^{1/2} z.

Lemma S2(iii)

theorem LogOptimal.runningMean_affine {t : ℕ} (ht : t ≠ 0) (m c : ℝ) (z : ℕ → ℝ) : (runningMean t fun (k : ℕ) => m + c * z k) = m + c * runningMean t z

theorem LogOptimal.helmertY_affine {i : ℕ} (hi : 2 ≤ i) (m c : ℝ) (z : ℕ → ℝ) : (helmertY i fun (k : ℕ) => m + c * z k) = c * helmertY i z

noncomputable def LogOptimal.helmertFamily (t : ℕ) (i : Fin t) : (ℕ → ℝ) → ℝ

The family (X̄_t, Y₂, …, Y_t) of Lemma S2(iii), indexed by Fin t.

Equations

• LogOptimal.helmertFamily t i = if ↑i = 0 then LogOptimal.runningMean t else LogOptimal.helmertY (↑i + 1)

theorem LogOptimal.measurable_helmertFamily (t : ℕ) (i : Fin t) : Measurable (helmertFamily t i)

noncomputable def LogOptimal.helmertAffine (t : ℕ) (m : ℝ) (v : NNReal) (j : Fin t) (w : ℝ) : ℝ

The affine map that sends the coordinates ⟨ω_j, z⟩ of a standard Gaussian vector z in the Helmert basis to (X̄_t, Y₂, …, Y_t) for X = m + v^{1/2} z: the shift m and the factor (v/t)^{1/2} for j = 0, and the factor −v^{1/2} for j ≥ 1.

Equations

• LogOptimal.helmertAffine t m v j w = (if ↑j = 0 then m else 0) + (if ↑j = 0 then √↑v / √↑t else -√↑v) * w

theorem LogOptimal.helmertFamily_affine {t : ℕ} (ht : 0 < t) (m : ℝ) (v : NNReal) (z : ℕ → ℝ) (j : Fin t) : (helmertFamily t j fun (k : ℕ) => m + √↑v * z k) = helmertAffine t m v j (helmertMap t (fun (k : Fin t) => z ↑k) j)

theorem LogOptimal.map_helmertFamily {t : ℕ} (ht : 0 < t) (m : ℝ) (v : NNReal) : MeasureTheory.Measure.map (fun (x : ℕ → ℝ) (j : Fin t) => helmertFamily t j x) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v) = MeasureTheory.Measure.pi fun (j : Fin t) => MeasureTheory.Measure.map (helmertAffine t m v j) (ProbabilityTheory.gaussianReal 0 1)

Lemma S2(iii), joint distribution: under N(m, v)^{⊗∞}, the distribution of (X̄_t, Y₂, …, Y_t) is the product of the images of N(0, 1) under the maps helmertAffine.

theorem LogOptimal.map_helmertAffine_zero {t : ℕ} (ht : 0 < t) (m : ℝ) (v : NNReal) : MeasureTheory.Measure.map (helmertAffine t m v ⟨0, ht⟩) (ProbabilityTheory.gaussianReal 0 1) = ProbabilityTheory.gaussianReal m (v / ↑t)

theorem LogOptimal.map_helmertAffine_of_ne_zero {t : ℕ} (m : ℝ) (v : NNReal) (j : Fin t) (hj : ↑j ≠ 0) : MeasureTheory.Measure.map (helmertAffine t m v j) (ProbabilityTheory.gaussianReal 0 1) = ProbabilityTheory.gaussianReal 0 v

theorem LogOptimal.iIndepFun_helmertFamily {t : ℕ} (ht : 0 < t) (m : ℝ) (v : NNReal) : ProbabilityTheory.iIndepFun (helmertFamily t) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v) ∧ MeasureTheory.Measure.map (runningMean t) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v) = ProbabilityTheory.gaussianReal m (v / ↑t) ∧ ∀ (i : ℕ), 2 ≤ i → i ≤ t → MeasureTheory.Measure.map (helmertY i) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v) = ProbabilityTheory.gaussianReal 0 v

Lemma S2(iii): if X ∼ N(m, v)^{⊗∞}, then X̄_t, Y₂, …, Y_t are independent, with X̄_t ∼ N(m, v/t) and Y_i ∼ N(0, v).

Lemma S2

theorem LogOptimal.lem_orth_proof (t : ℕ) : 2 ≤ t → ((∀ (a b : ℝ) (x x' : ℕ → ℝ), (runningMean t fun (i : ℕ) => a * x i + b * x' i) = a * runningMean t x + b * runningMean t x' ∧ ∀ (i : ℕ), 2 ≤ i → i ≤ t → (helmertY i fun (j : ℕ) => a * x j + b * x' j) = a * helmertY i x + b * helmertY i x') ∧ (∀ (x : ℕ → ℝ), (√↑t * runningMean t x) ^ 2 + ∑ i ∈ Finset.Icc 2 t, helmertY i x ^ 2 = ∑ i ∈ Finset.range t, x i ^ 2) ∧ (∀ (x : ℕ → ℝ) (m : ℝ) (i : ℕ), 2 ≤ i → i ≤ t → (helmertY i fun (j : ℕ) => x j + m) = helmertY i x) ∧ ∀ (x : ℕ → ℝ) (m : ℝ), ∑ i ∈ Finset.range t, (x i - m) ^ 2 = ↑t * (runningMean t x - m) ^ 2 + ∑ i ∈ Finset.Icc 2 t, helmertY i x ^ 2) ∧ (∀ (x : ℕ → ℝ), runningMean t x = runningMean (t - 1) x + helmertY t x / √(↑t * (↑t - 1))) ∧ ∀ (m : ℝ) (v : NNReal), 0 < v → have μ := MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal m v; have f := fun (i : Fin t) => if ↑i = 0 then runningMean t else helmertY (↑i + 1); ProbabilityTheory.iIndepFun f μ ∧ MeasureTheory.Measure.map (runningMean t) μ = ProbabilityTheory.gaussianReal m (v / ↑t) ∧ ∀ (i : ℕ), 2 ≤ i → i ≤ t → MeasureTheory.Measure.map (helmertY i) μ = ProbabilityTheory.gaussianReal 0 v