The Helmert basis, Lemma S2(i) and (ii), the maximal invariant, and eq. (10)

This file proves the algebraic parts of Lemma S2 of the supplementary material, following its proof, and two consequences. Let t ≥ 1, let ω₁ = t^{-1/2}(1, …, 1), and, for 2 ≤ i ≤ t, let ω_i = {i(i − 1)}^{-1/2}(1, …, 1, 1 − i, 0, …, 0) with i − 1 leading ones. These vectors are the rows of a Helmert matrix and form an orthonormal basis of ℝ^t, with ⟨ω₁, x⟩ = t^{1/2} x̄_t and ⟨ω_i, x⟩ = −y_i. In Lean, the vectors are indexed by j : Fin t, and helmertRow t j is the vector ω_{j+1}.

• helmertCoeff j k: the coordinate k of (1, …, 1, −j, 0, …, 0), with j leading ones;
• pathVec t x: the vector x^t = (x₁, …, x_t) of EuclideanSpace ℝ (Fin t) given by a path;
• helmertRow t j: the vector ω_{j+1}, and helmertBasis t the orthonormal basis (ω₁, …, ω_t);
• inner_helmertRow_zero and inner_helmertRow_of_ne_zero: ⟨ω₁, x⟩ = t^{1/2} x̄_t and ⟨ω_{j+1}, x⟩ = −y_{j+1} for j ≥ 1;
• runningMean_linear and helmertY_linear: the map x ↦ (t^{1/2} x̄_t, y₂, …, y_t) is linear;
• sq_sqrt_mul_runningMean_add_sum_sq_helmertY: this map preserves the Euclidean norm (Lemma S2(i));
• helmertY_add_const: the values y_i do not change when the same constant is added to every x_i, since ω_i is orthogonal to (1, …, 1) for i ≥ 2;
• sum_sq_sub_eq: ∑_{i=1}^t (x_i − m)² = t(x̄_t − m)² + ∑_{i=2}^t y_i² (Lemma S2(i));
• runningMean_eq_add_helmertY: x̄_t = x̄_{t−1} + y_t/{t(t − 1)}^{1/2} (Lemma S2(ii));
• helmertY_eq_iff_exists_add_const: Y^t = (Y₂, …, Y_t) is a maximal invariant under the translations x ↦ (x₁ + m, …, x_t + m) (Section 4.1), and sec4_maximal_invariant_translation the first claim of the statement sec4_maximal_invariant;
• dataFiltration_eq_helmertFiltration_sup and eq_enlarge_proof: eq. (10), ℱ_t = 𝒢_t ∨ σ(X₁) for t ≥ 1 (Section S2.4).

Linearity

theorem LogOptimal.runningMean_linear (t : ℕ) (a b : ℝ) (x x' : ℕ → ℝ) : (runningMean t fun (i : ℕ) => a * x i + b * x' i) = a * runningMean t x + b * runningMean t x'

theorem LogOptimal.helmertY_linear (i : ℕ) (a b : ℝ) (x x' : ℕ → ℝ) : (helmertY i fun (j : ℕ) => a * x j + b * x' j) = a * helmertY i x + b * helmertY i x'

theorem LogOptimal.runningMean_add_const {t : ℕ} (ht : t ≠ 0) (x : ℕ → ℝ) (m : ℝ) : (runningMean t fun (i : ℕ) => x i + m) = runningMean t x + m

The Helmert vectors

noncomputable def LogOptimal.helmertCoeff (j k : ℕ) : ℝ

The coordinate k of the vector (1, …, 1, −j, 0, …, 0) with j leading ones. Up to the factor {j(j + 1)}^{-1/2}, it is the Helmert vector ω_{j+1} of the proof of Lemma S2.

Equations

• LogOptimal.helmertCoeff j k = if k < j then 1 else if k = j then -↑j else 0

theorem LogOptimal.sum_helmertCoeff_mul_eq_ite (x : ℕ → ℝ) (j n : ℕ) : ∑ k ∈ Finset.range n, helmertCoeff j k * x k = if n ≤ j then ∑ k ∈ Finset.range n, x k else ∑ k ∈ Finset.range j, x k - ↑j * x j

theorem LogOptimal.sum_helmertCoeff_mul (x : ℕ → ℝ) {j n : ℕ} (hjn : j < n) : ∑ k ∈ Finset.range n, helmertCoeff j k * x k = ∑ k ∈ Finset.range j, x k - ↑j * x j

theorem LogOptimal.sum_helmertCoeff (j n : ℕ) : ∑ k ∈ Finset.range n, helmertCoeff j k = if n ≤ j then ↑n else 0

noncomputable def LogOptimal.pathVec (t : ℕ) (x : ℕ → ℝ) : EuclideanSpace ℝ (Fin t)

The vector x^t = (x₁, …, x_t) of EuclideanSpace ℝ (Fin t) given by the first t coordinates of a path x.

Equations

• LogOptimal.pathVec t x = WithLp.toLp 2 fun (k : Fin t) => x ↑k

noncomputable def LogOptimal.helmertPath (t j k : ℕ) : ℝ

The Helmert vector ω_{j+1} of the proof of Lemma S2 as a path: t^{-1/2}(1, 1, …) for j = 0, and {j(j + 1)}^{-1/2}(1, …, 1, −j, 0, …) with j leading ones for j ≥ 1.

Equations

• LogOptimal.helmertPath t j k = if j = 0 then (√↑t)⁻¹ else (√(↑j * (↑j + 1)))⁻¹ * LogOptimal.helmertCoeff j k

noncomputable def LogOptimal.helmertRow (t : ℕ) (j : Fin t) : EuclideanSpace ℝ (Fin t)

The Helmert vector ω_{j+1} of the proof of Lemma S2, in EuclideanSpace ℝ (Fin t): ω₁ = t^{-1/2}(1, …, 1) and ω_{j+1} = {j(j + 1)}^{-1/2}(1, …, 1, −j, 0, …, 0) with j leading ones for 1 ≤ j < t.

Equations

• LogOptimal.helmertRow t j = LogOptimal.pathVec t (LogOptimal.helmertPath t ↑j)

theorem LogOptimal.inner_pathVec (t : ℕ) (x y : ℕ → ℝ) : inner ℝ (pathVec t x) (pathVec t y) = ∑ k ∈ Finset.range t, x k * y k

theorem LogOptimal.inner_helmertRow_pathVec (t : ℕ) (j : Fin t) (x : ℕ → ℝ) : inner ℝ (helmertRow t j) (pathVec t x) = if ↑j = 0 then (√↑t)⁻¹ * ∑ k ∈ Finset.range t, x k else (√(↑↑j * (↑↑j + 1)))⁻¹ * (∑ k ∈ Finset.range ↑j, x k - ↑↑j * x ↑j)

theorem LogOptimal.inner_helmertRow_zero {t : ℕ} (ht : 0 < t) (x : ℕ → ℝ) : inner ℝ (helmertRow t ⟨0, ht⟩) (pathVec t x) = √↑t * runningMean t x

theorem LogOptimal.inner_helmertRow_of_ne_zero {t : ℕ} (j : Fin t) (hj : ↑j ≠ 0) (x : ℕ → ℝ) : inner ℝ (helmertRow t j) (pathVec t x) = -helmertY (↑j + 1) x

Orthonormality

theorem LogOptimal.inner_helmertRow (t : ℕ) (i j : Fin t) : inner ℝ (helmertRow t i) (helmertRow t j) = if i = j then 1 else 0

theorem LogOptimal.orthonormal_helmertRow (t : ℕ) : Orthonormal ℝ (helmertRow t)

noncomputable def LogOptimal.helmertBasis (t : ℕ) : OrthonormalBasis (Fin t) ℝ (EuclideanSpace ℝ (Fin t))

The orthonormal basis (ω₁, …, ω_t) of Helmert vectors of the proof of Lemma S2 (Lancaster, 1965).

Equations

• LogOptimal.helmertBasis t = OrthonormalBasis.mk ⋯ ⋯

theorem LogOptimal.helmertBasis_apply (t : ℕ) (j : Fin t) : (helmertBasis t) j = helmertRow t j

theorem LogOptimal.helmertBasis_repr_apply (t : ℕ) (v : EuclideanSpace ℝ (Fin t)) (j : Fin t) : ((helmertBasis t).repr v).ofLp j = inner ℝ (helmertRow t j) v

Lemma S2(i) and (ii)

theorem LogOptimal.sum_sq_inner_helmertRow (t : ℕ) (x : ℕ → ℝ) : ∑ j : Fin t, inner ℝ (helmertRow t j) (pathVec t x) ^ 2 = ∑ k ∈ Finset.range t, x k ^ 2

The orthogonality of the Helmert basis gives ∑_j ⟨ω_j, x⟩² = ∑_{i=1}^t x_i².

theorem LogOptimal.sum_Icc_two_eq_sum_fin {t : ℕ} (f : ℕ → ℝ) : ∑ i ∈ Finset.Icc 2 (t + 1), f i = ∑ j : Fin t, f (↑j + 2)

theorem LogOptimal.sq_sqrt_mul_runningMean_add_sum_sq_helmertY {t : ℕ} (ht : 1 ≤ t) (x : ℕ → ℝ) : (√↑t * runningMean t x) ^ 2 + ∑ i ∈ Finset.Icc 2 t, helmertY i x ^ 2 = ∑ i ∈ Finset.range t, x i ^ 2

Lemma S2(i), orthogonality: the map x ↦ (t^{1/2} x̄_t, y₂, …, y_t) preserves the Euclidean norm.

theorem LogOptimal.pathVec_const (t : ℕ) (ht : 0 < t) (m : ℝ) : (pathVec t fun (x : ℕ) => m) = (m * √↑t) • helmertRow t ⟨0, ht⟩

The constant path 1 is t^{1/2} ω₁.

theorem LogOptimal.pathVec_add (t : ℕ) (x y : ℕ → ℝ) : (pathVec t fun (k : ℕ) => x k + y k) = pathVec t x + pathVec t y

theorem LogOptimal.helmertY_add_const (x : ℕ → ℝ) (m : ℝ) {i : ℕ} (hi : 2 ≤ i) : (helmertY i fun (j : ℕ) => x j + m) = helmertY i x

Lemma S2(i), invariance: since ω_i is orthogonal to (1, …, 1) for i ≥ 2, the values y_i do not change when the same constant is added to every x_i.

theorem LogOptimal.sum_sq_sub_eq {t : ℕ} (ht : 1 ≤ t) (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

Lemma S2(i): ∑_{i=1}^t (x_i − m)² = t(x̄_t − m)² + ∑_{i=2}^t y_i² for every m ∈ ℝ, from the orthogonality applied to (x₁ − m, …, x_t − m).

theorem LogOptimal.runningMean_eq_add_helmertY {t : ℕ} (ht : 2 ≤ t) (x : ℕ → ℝ) : runningMean t x = runningMean (t - 1) x + helmertY t x / √(↑t * (↑t - 1))

Lemma S2(ii): x̄_t = x̄_{t−1} + y_t/{t(t − 1)}^{1/2} for t ≥ 2, from the identity x̄_t = x̄_{t−1} + (x_t − x̄_{t−1})/t.

The maximal invariant

theorem LogOptimal.runningMean_congr {t : ℕ} {x x' : ℕ → ℝ} (h : ∀ k < t, x k = x' k) : runningMean t x = runningMean t x'

theorem LogOptimal.helmertY_congr {i : ℕ} (hi : 1 ≤ i) {x x' : ℕ → ℝ} (h : ∀ k < i, x k = x' k) : helmertY i x = helmertY i x'

theorem LogOptimal.helmertY_eq_iff_exists_add_const (t : ℕ) (x x' : ℕ → ℝ) : (∀ (i : ℕ), 2 ≤ i → i ≤ t → helmertY i x = helmertY i x') ↔ ∃ (m : ℝ), ∀ i < t, x' i = x i + m

Maximal invariance (Section 4.1): Y^t = (Y₂, …, Y_t) takes the same value at x and x' exactly when x'^t is a translation of x^t. If the values agree, the difference x'^t − x^t is orthogonal to ω₂, …, ω_t, so its expansion in the Helmert basis is a multiple of ω₁, a constant vector.

The data filtration as an initial enlargement, eq. (10)

theorem LogOptimal.measurable_helmertY_dataFiltration {t i : ℕ} (hi : 1 ≤ i) (hit : i ≤ t) : Measurable (helmertY i)

theorem LogOptimal.measurable_helmertY_helmertFiltration {t i : ℕ} (hi : 2 ≤ i) (hit : i ≤ t) : Measurable (helmertY i)

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

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

theorem LogOptimal.measurable_coord_helmertFiltration_sup {t k : ℕ} (hk : k < t) : Measurable fun (x : ℕ → ℝ) => x k

theorem LogOptimal.dataFiltration_eq_helmertFiltration_sup {t : ℕ} (ht : 1 ≤ t) : ↑(dataFiltration ℝ) t = ↑helmertFiltration t ⊔ MeasurableSpace.comap (fun (x : ℕ → ℝ) => x 0) inferInstance

Equation (10): it follows from Lemma S2 that X^t and (X₁, Y₂, …, Y_t) are functions of each other, so that ℱ_t = 𝒢_t ∨ σ(X₁) for t ≥ 1.

theorem LogOptimal.eq_enlarge_proof (t : ℕ) : 1 ≤ t → ↑(dataFiltration ℝ) t = ↑helmertFiltration t ⊔ MeasurableSpace.comap (fun (x : ℕ → ℝ) => x 0) inferInstance

theorem LogOptimal.sec4_maximal_invariant_translation (t : ℕ) (x x' : ℕ → ℝ) : (∀ (i : ℕ), 2 ≤ i → i ≤ t → helmertY i x = helmertY i x') ↔ ∃ (m : ℝ), ∀ i < t, x' i = x i + m