The products ∏_{i=2}^t ℓ(Y_i) form a test martingale with respect to (𝒢_t)

This file proves the last claim of Proposition 2, following its proof: under P_θ, the Y_i are independent N(0, 1) variables by Lemma S2(iii), and E{ℓ(Z)} = 1 for Z ∼ N(0, 1). The products ∏_{i=2}^t ℓ(Y_i), t ≥ 0, therefore form a test martingale with respect to (𝒢_t).

• nullDist_map_helmertY and integral_lik_helmertY: under P_θ, Y_i ∼ N(0, 1) and E_θ{ℓ(Y_i)} = 1 for i ≥ 2;
• indep_helmertY_helmertFiltration: under P_θ, Y_{t+1} is independent of 𝒢_t for t ≥ 1;
• prop_numeraire_testMartingale: the test martingale of Proposition 2.

theorem LogOptimal.integrable_lik {s : ℝ} (hs : 0 < s) : MeasureTheory.Integrable (lik s) (ProbabilityTheory.gaussianReal 0 1)

theorem LogOptimal.nullDist_map_helmertY (θ : ℝ) {i : ℕ} (hi : 2 ≤ i) : MeasureTheory.Measure.map (helmertY i) (nullDist θ) = ProbabilityTheory.gaussianReal 0 1

Under P_θ, Y_i ∼ N(0, 1) for i ≥ 2 (Lemma S2(iii)).

theorem LogOptimal.integrable_lik_helmertY {s : ℝ} (hs : 0 < s) (θ : ℝ) {i : ℕ} (hi : 2 ≤ i) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => lik s (helmertY i x)) (nullDist θ)

theorem LogOptimal.integral_lik_helmertY {s : ℝ} (hs : 0 < s) (θ : ℝ) {i : ℕ} (hi : 2 ≤ i) : ∫ (x : ℕ → ℝ), lik s (helmertY i x) ∂nullDist θ = 1

theorem LogOptimal.helmertFamily_of_ne_zero {t : ℕ} (j : Fin t) (hj : ↑j ≠ 0) : helmertFamily t j = helmertY (↑j + 1)

theorem LogOptimal.indep_helmertY_helmertFiltration (θ : ℝ) {t : ℕ} (ht : 1 ≤ t) : ProbabilityTheory.Indep (MeasurableSpace.comap (helmertY (t + 1)) inferInstance) (↑helmertFiltration t) (nullDist θ)

Under P_θ, Y_{t+1} is independent of 𝒢_t = σ(Y₂, …, Y_t) for t ≥ 1, since X̄_{t+1}, Y₂, …, Y_{t+1} are independent by Lemma S2(iii).

theorem LogOptimal.prop_numeraire_testMartingale (s : ℝ) : 0 < s → IsTestMartingale gaussNull helmertFiltration fun (t : ℕ) (x : ℕ → ℝ) => ∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x)

Proposition 2, last claim: under every P_θ, the products E*_t = ∏_{i=2}^t ℓ(Y_i), t ≥ 0, form a test martingale with respect to (𝒢_t).