Change of measure from P_θ to Q_θ

This file prepares the proof of Lemma 2(ii) of the paper (Section S1.5).

• dataFiltration_eq_comap: ℱ_t is generated by the map x ↦ x^t.
• lintegral_altDist_eq: since L^θ_t is the density of Q_θ with respect to P_θ on ℱ_t, E_{Q_θ}(H) = E_θ(L^θ_t H) for every ℱ_t-measurable H ≥ 0.
• lintegral_altDist_truncTime: the same identity at a stopping time τ ∧ T, E_{Q_θ}(G_{τ∧T}) = E_θ(L^θ_{τ∧T} G_{τ∧T}) for an adapted (G_t).
• altDist_map_increments: under Q_θ, the increments (X_i − θ)/s of S_t = ∑_{i ≤ t} (X_i − θ)/s are independent N(0, 1) variables.
• walkFiltration_eq: the filtration generated by the random walk (S_t) is the filtration generated by its increments.
• changeFactor_eq_reward and lintegral_changeFactor_eq: the factor g_t = s exp{(1 − s²)t(X̄_t − θ)²/(2s²)} of the proof of Lemma 2 is the reward h_t of the random walk, and E_{Q_θ}(g_{τ∧T}) = E(h_{τ̂∧T}) for the stopping time τ̂ = τ ∘ Ψ of the random walk, where Ψ maps the increments to the observations.

The data filtration is generated by X^t

theorem LogOptimal.dataFiltration_eq_comap {𝒳 : Type u_1} [MeasurableSpace 𝒳] (t : ℕ) : ↑(dataFiltration 𝒳) t = MeasurableSpace.comap (fun (x : ℕ → 𝒳) (i : Fin t) => x ↑i) MeasurableSpace.pi

theorem LogOptimal.measurable_restrict_fin {𝒳 : Type u_1} [MeasurableSpace 𝒳] (t : ℕ) : Measurable fun (x : ℕ → 𝒳) (i : Fin t) => x ↑i

The density of Q_θ with respect to P_θ on ℱ_t

theorem LogOptimal.measurable_likProcess (s θ : ℝ) (t : ℕ) : Measurable (likProcess s θ t)

theorem LogOptimal.altDist_apply_eq_withDensity {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) {A : Set (ℕ → ℝ)} (hA : MeasurableSet A) : (altDist s θ) A = ((nullDist θ).withDensity fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s θ t x)) A

theorem LogOptimal.trim_altDist_eq {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) : (altDist s θ).trim ⋯ = ((nullDist θ).withDensity fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s θ t x)).trim ⋯

theorem LogOptimal.lintegral_altDist_eq {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) {H : (ℕ → ℝ) → ENNReal} (hH : Measurable H) : ∫⁻ (x : ℕ → ℝ), H x ∂altDist s θ = ∫⁻ (x : ℕ → ℝ), ENNReal.ofReal (likProcess s θ t x) * H x ∂nullDist θ

Change of measure on ℱ_t: E_{Q_θ}(H) = E_θ(L^θ_t H) for every ℱ_t-measurable H ≥ 0, since L^θ_t is the likelihood ratio of Q_θ against P_θ on ℱ_t.

The change of measure at a stopping time

theorem LogOptimal.measurableSet_truncTime_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {τ : (ℕ → 𝒳) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) τ) (T t : ℕ) : MeasurableSet {x : ℕ → 𝒳 | truncTime τ T x = t}

theorem LogOptimal.lintegral_altDist_truncTime {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (T : ℕ) {G : ℕ → (ℕ → ℝ) → ENNReal} (hG : ∀ (t : ℕ), Measurable (G t)) {τ : (ℕ → ℝ) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ) : ∫⁻ (x : ℕ → ℝ), G (truncTime τ T x) x ∂altDist s θ = ∫⁻ (x : ℕ → ℝ), ENNReal.ofReal (likProcess s θ (truncTime τ T x) x) * G (truncTime τ T x) x ∂nullDist θ

Change of measure at a stopping time: for an adapted (G_t) with values in [0, ∞] and a stopping time τ of (ℱ_t), E_{Q_θ}(G_{τ∧T}) = E_θ(L^θ_{τ∧T} G_{τ∧T}).

The random walk of the increments

noncomputable def LogOptimal.increments (s θ : ℝ) (x : ℕ → ℝ) : ℕ → ℝ

The increments (X_i − θ)/s of the random walk S_t = ∑_{i ≤ t} (X_i − θ)/s.

Equations

• LogOptimal.increments s θ x i = (x i - θ) / s

noncomputable def LogOptimal.fromIncrements (s θ : ℝ) (ω : ℕ → ℝ) : ℕ → ℝ

The inverse of increments: X_i = θ + s ω_i.

Equations

• LogOptimal.fromIncrements s θ ω i = θ + s * ω i

theorem LogOptimal.measurable_increments (s θ : ℝ) : Measurable (increments s θ)

theorem LogOptimal.measurable_fromIncrements (s θ : ℝ) : Measurable (fromIncrements s θ)

theorem LogOptimal.fromIncrements_increments {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (x : ℕ → ℝ) : fromIncrements s θ (increments s θ x) = x

theorem LogOptimal.increments_fromIncrements {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (ω : ℕ → ℝ) : increments s θ (fromIncrements s θ ω) = ω

theorem LogOptimal.altDist_map_increments {s : ℝ} (hs : 0 < s) (θ : ℝ) : MeasureTheory.Measure.map (increments s θ) (altDist s θ) = stdGaussSeq

Under Q_θ, the increments (X_i − θ)/s are independent N(0, 1) variables.

theorem LogOptimal.walkFiltration_eq : walkFiltration = dataFiltration ℝ

The filtration generated by the random walk (S_t) is the filtration generated by its increments.

Stopping times of the random walk

theorem LogOptimal.comap_le_dataFiltration {𝒳 : Type u_1} {𝒴 : Type u_2} [MeasurableSpace 𝒳] [MeasurableSpace 𝒴] {Φ : (ℕ → 𝒳) → ℕ → 𝒴} {t : ℕ} (hΦ : ∀ i < t, Measurable fun (x : ℕ → 𝒳) => Φ x i) : MeasurableSpace.comap Φ (↑(dataFiltration 𝒴) t) ≤ ↑(dataFiltration 𝒳) t

theorem LogOptimal.isStoppingTime_comp {𝒳 : Type u_1} {𝒴 : Type u_2} [MeasurableSpace 𝒳] [MeasurableSpace 𝒴] {Φ : (ℕ → 𝒳) → ℕ → 𝒴} (hΦ : ∀ (t i : ℕ), i < t → Measurable fun (x : ℕ → 𝒳) => Φ x i) {τ : (ℕ → 𝒴) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration 𝒴) τ) : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) fun (x : ℕ → 𝒳) => τ (Φ x)

A stopping time composed with a map that preserves every ℱ_t is a stopping time.

theorem LogOptimal.measurable_increments_coord (s θ : ℝ) (t i : ℕ) : i < t → Measurable fun (x : ℕ → ℝ) => increments s θ x i

theorem LogOptimal.measurable_fromIncrements_coord (s θ : ℝ) (t i : ℕ) : i < t → Measurable fun (ω : ℕ → ℝ) => fromIncrements s θ ω i

The factor g_t and the reward h_t

noncomputable def LogOptimal.changeFactor (s θ : ℝ) (t : ℕ) (x : ℕ → ℝ) : ℝ

The factor g_t of the proof of Lemma 2: g_0 = 1 and g_t = s exp{(1 − s²)t(X̄_t − θ)²/(2s²)} for t ≥ 1.

Equations

• LogOptimal.changeFactor s θ t x = if t = 0 then 1 else s * Real.exp ((1 - s ^ 2) * ↑t * (LogOptimal.runningMean t x - θ) ^ 2 / (2 * s ^ 2))

theorem LogOptimal.walk_increments {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) (x : ℕ → ℝ) (ht : t ≠ 0) : walk t (increments s θ x) = ↑t * (runningMean t x - θ) / s

theorem LogOptimal.changeFactor_eq_reward {s : ℝ} (hs : s ≠ 0) (θ : ℝ) (t : ℕ) (x : ℕ → ℝ) : changeFactor s θ t x = reward s t (increments s θ x)

theorem LogOptimal.measurable_reward (s : ℝ) (t : ℕ) : Measurable (reward s t)

theorem LogOptimal.measurable_reward_pair (s : ℝ) : Measurable fun (p : ℕ × (ℕ → ℝ)) => reward s p.1 p.2

theorem LogOptimal.measurable_truncTime {𝒳 : Type u_1} [MeasurableSpace 𝒳] {τ : (ℕ → 𝒳) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) τ) (T : ℕ) : Measurable (truncTime τ T)

theorem LogOptimal.lintegral_changeFactor_eq {s : ℝ} (hs : 0 < s) (θ : ℝ) (T : ℕ) {τ : (ℕ → ℝ) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ) : ∫⁻ (x : ℕ → ℝ), ENNReal.ofReal (changeFactor s θ (truncTime τ T x) x) ∂altDist s θ = ∫⁻ (ω : ℕ → ℝ), ENNReal.ofReal (reward s (truncTime (fun (ω : ℕ → ℝ) => τ (fromIncrements s θ ω)) T ω) ω) ∂stdGaussSeq

Transfer to the random walk: for a stopping time τ of (ℱ_t), E_{Q_θ}(g_{τ∧T}) = E(h_{τ̂∧T}), where τ̂ = τ ∘ Ψ is a stopping time of the filtration of the increments of the random walk and Ψ maps the increments to the observations.