The supremum η_T as the value of an optimal stopping problem

This file proves Lemma 2(ii) of the paper (Section S1.5) from the factorization of Lemma 2(i), E*_t = L^θ_t g_t, where g_t = s exp{(1 − s²)t(X̄_t − θ)²/(2s²)} (changeFactor).

• lintegral_gaussNumeraire_eq: for every θ and every stopping time τ of (ℱ_t), E_θ(E*_{τ∧T}) = E_{Q_θ}(g_{τ∧T}) = E(h_{τ̂∧T}), with τ̂ = τ ∘ Ψ.
• eta_eq_walkValue: η_T = sup_τ E(h_{τ∧T}) over the stopping times of the filtration generated by the random walk.

theorem LogOptimal.measurable_runningMean_dataFiltration (t : ℕ) : Measurable (runningMean t)

theorem LogOptimal.measurable_changeFactor_dataFiltration (s θ : ℝ) (t : ℕ) : Measurable fun (x : ℕ → ℝ) => ENNReal.ofReal (changeFactor s θ t x)

theorem LogOptimal.lintegral_gaussNumeraire_eq {s : ℝ} (hs : 0 < s) (hfac : ∀ (θ : ℝ) (t : ℕ) (x : ℕ → ℝ), gaussNumeraire s t x = ENNReal.ofReal (likProcess s θ t x * changeFactor s θ t x)) (θ : ℝ) (T : ℕ) {τ : (ℕ → ℝ) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ) : ∫⁻ (x : ℕ → ℝ), gaussNumeraire s (truncTime τ T x) x ∂nullDist θ = ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (reward s (truncTime (fun (ω : ℕ → ℝ) => τ (fromIncrements s θ ω)) T ω) ω) ∂stdGaussSeq

For every θ and every stopping time τ of (ℱ_t), the factorization E*_t = L^θ_t g_t gives E_θ(E*_{τ∧T}) = E_{Q_θ}(g_{τ∧T}) by the change of measure from P_θ to Q_θ, and then E(h_{τ̂∧T}) by the transfer to the random walk.

theorem LogOptimal.eta_eq_walkValue {s : ℝ} (hs : 0 < s) (hfac : ∀ (θ : ℝ) (t : ℕ) (x : ℕ → ℝ), gaussNumeraire s t x = ENNReal.ofReal (likProcess s θ t x * changeFactor s θ t x)) (T : ℕ) : eta gaussNull (gaussNumeraire s) T = walkValue s T

Lemma 2(ii), from the factorization of Lemma 2(i): η_T = sup_τ E(h_{τ∧T}), where τ ranges over the stopping times of the filtration generated by the random walk.