Lemma 2 (Change of measure) and Lemma S3 (Upper bound on η_T)

This file proves Lemma 2(i) of the paper, following its proof in Section S1.5: eq. (S2) with m = θ and v ∈ {s², 1} gives L^θ_t = {φ_{s²/t}(X̄_t − θ)/φ_{1/t}(X̄_t − θ)} ∏_{i=2}^t ℓ(Y_i) = s^{-1} exp{−(1 − s²)t(X̄_t − θ)²/(2s²)} E*_t. Together with eta_eq_walkValue, which derives Lemma 2(ii) from this factorization, it gives Lemma 2 (lem_identity_proof). With the bound on the random walk of Walk.lean, Lemma 2(ii) gives Lemma S3 (lem_upper_proof).

• gaussianPDFReal_div_gaussianPDFReal: φ_{s²/t}(z)/φ_{1/t}(z) = s^{-1} exp{−(1 − s²)tz²/(2s²)};
• likProcess_eq: L^θ_t = s^{-1} exp{−(1 − s²)t(X̄_t − θ)²/(2s²)} ∏_{i=2}^t ℓ(Y_i);
• gaussNumeraire_eq_mul: Lemma 2(i);
• gaussNumeraire_eq_likProcess_mul_changeFactor: the form E*_t = L^θ_t g_t, for every t ≥ 0;
• eta_gaussNumeraire_eq_walkValue: Lemma 2(ii);
• lem_identity_proof and lem_upper_proof.

theorem LogOptimal.gaussianPDFReal_div_gaussianPDFReal {s : ℝ} (hs : 0 < s) {t : ℕ} (ht : 1 ≤ t) (z : ℝ) : ProbabilityTheory.gaussianPDFReal 0 ((s ^ 2).toNNReal / ↑t) z / ProbabilityTheory.gaussianPDFReal 0 (1 / ↑t) z = s⁻¹ * Real.exp (-((1 - s ^ 2) * ↑t * z ^ 2 / (2 * s ^ 2)))

theorem LogOptimal.likProcess_eq {s : ℝ} (hs : 0 < s) (θ : ℝ) {t : ℕ} (ht : 1 ≤ t) (x : ℕ → ℝ) : likProcess s θ t x = s⁻¹ * Real.exp (-((1 - s ^ 2) * ↑t * (runningMean t x - θ) ^ 2 / (2 * s ^ 2))) * ∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x)

theorem LogOptimal.gaussNumeraire_eq_mul {s : ℝ} (hs : 0 < s) (θ : ℝ) {t : ℕ} (ht : 1 ≤ t) (x : ℕ → ℝ) : gaussNumeraire s t x = ENNReal.ofReal (s * likProcess s θ t x * Real.exp ((1 - s ^ 2) * ↑t * (runningMean t x - θ) ^ 2 / (2 * s ^ 2)))

Lemma 2(i).

theorem LogOptimal.gaussNumeraire_eq_likProcess_mul_changeFactor {s : ℝ} (hs : 0 < s) (θ : ℝ) (t : ℕ) (x : ℕ → ℝ) : gaussNumeraire s t x = ENNReal.ofReal (likProcess s θ t x * changeFactor s θ t x)

Lemma 2(i) in the form E*_t = L^θ_t g_t of the proof of Lemma 2(ii), for every t ≥ 0.

theorem LogOptimal.eta_gaussNumeraire_eq_walkValue {s : ℝ} (hs : 0 < s) (T : ℕ) : eta gaussNull (gaussNumeraire s) T = walkValue s T

Lemma 2(ii): η_T = sup_τ E(h_{τ∧T}).

theorem LogOptimal.lem_identity_proof (s : ℝ) : 0 < s → (∀ (θ : ℝ) (t : ℕ), 1 ≤ t → ∀ (x : ℕ → ℝ), gaussNumeraire s t x = ENNReal.ofReal (s * likProcess s θ t x * Real.exp ((1 - s ^ 2) * ↑t * (runningMean t x - θ) ^ 2 / (2 * s ^ 2)))) ∧ ∀ (T : ℕ), eta gaussNull (gaussNumeraire s) T = ⨆ (τ : (ℕ → ℝ) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime walkFiltration τ), ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (reward s (truncTime τ T ω) ω) ∂stdGaussSeq

theorem LogOptimal.lem_upper_proof (s : ℝ) : 0 < s → s < 1 → ∀ (T : ℕ) (q : ℝ), 1 ≤ T → 1 < q → q < 1 / (1 - s ^ 2) → (eta gaussNull (gaussNumeraire s) T).log ≤ ↑((1 - s ^ 2) * q * Real.log (2 + 2 * Real.log ↑T / Real.log q) + Real.log (1 / (1 - (1 - s ^ 2) * q)))

Lemma S3: by Lemma 2(ii), η_T ≤ E(M), and Walk.lean bounds E(M).