The Snell envelope

This file proves the claims of Section 2 of the paper on the Snell envelope (Λ^P_t)_{0≤t≤T} of (E*_{t∧T})_{t≥0} under a null distribution P, from the finite-horizon optimal stopping theorem of Peskir and Shiryaev (2006, Theorem 1.2), which enters as the hypothesis PeskirShiryaevTheorem12. The reward (E*_t)_{0≤t≤T} is nonnegative, adapted, and P-integrable, since E_P(E*_t) ≤ 1, and finite P-almost surely, so that its real part has the same stopped expectations. Since ℱ₀ is trivial, Λ^P_0 is constant.

• Setting.snellEnvelope_spec: the properties of (Λ^P_t) for P ∈ 𝒫;
• sec2_snell_proof: the claims of Section 2, with η_T = sup_{P∈𝒫} Λ^P_0.

theorem LogOptimal.Setting.snellEnvelope_spec {𝒳 : Type u} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hPS : PeskirShiryaevTheorem12) (hS : Setting 𝔓 Q Es) (T : ℕ) {P : MeasureTheory.Measure (ℕ → 𝒳)} (hP : P ∈ 𝔓) : (∀ t ≤ T, MeasureTheory.StronglyMeasurable (snellEnvelope P Es T t) ∧ MeasureTheory.Integrable (snellEnvelope P Es T t) P) ∧ (∀ t < T, P[snellEnvelope P Es T (t + 1) | ↑(dataFiltration 𝒳) t] ≤ᵐ[P] snellEnvelope P Es T t) ∧ (∀ t ≤ T, (fun (x : ℕ → 𝒳) => (Es t x).toReal) ≤ᵐ[P] snellEnvelope P Es T t) ∧ (∀ (U : ℕ → (ℕ → 𝒳) → ℝ), MeasureTheory.Adapted (dataFiltration 𝒳) U → (∀ (t : ℕ), MeasureTheory.Integrable (U t) P) → (∀ t < T, P[U (t + 1) | ↑(dataFiltration 𝒳) t] ≤ᵐ[P] U t) → (∀ t ≤ T, (fun (x : ℕ → 𝒳) => (Es t x).toReal) ≤ᵐ[P] U t) → ∀ t ≤ T, snellEnvelope P Es T t ≤ᵐ[P] U t) ∧ ∀ (x : ℕ → 𝒳), ENNReal.ofReal (snellEnvelope P Es T 0 x) = ⨆ (τ : (ℕ → 𝒳) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) τ), ∫⁻ (y : ℕ → 𝒳), Es (truncTime τ T y) y ∂P

The properties of the Snell envelope (Λ^P_t)_{0≤t≤T} of (E*_{t∧T})_{t≥0} under a null distribution P (Section 2), from Peskir and Shiryaev (2006, Theorem 1.2).

theorem LogOptimal.sec2_snell_proof : PeskirShiryaevTheorem12 → ∀ (𝒳 : Type u) [inst : MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal), Setting 𝔓 Q Es → ∀ (T : ℕ), (∀ P ∈ 𝔓, (∀ t ≤ T, MeasureTheory.StronglyMeasurable (snellEnvelope P Es T t) ∧ MeasureTheory.Integrable (snellEnvelope P Es T t) P) ∧ (∀ t < T, P[snellEnvelope P Es T (t + 1) | ↑(dataFiltration 𝒳) t] ≤ᵐ[P] snellEnvelope P Es T t) ∧ (∀ t ≤ T, (fun (x : ℕ → 𝒳) => (Es t x).toReal) ≤ᵐ[P] snellEnvelope P Es T t) ∧ (∀ (U : ℕ → (ℕ → 𝒳) → ℝ), MeasureTheory.Adapted (dataFiltration 𝒳) U → (∀ (t : ℕ), MeasureTheory.Integrable (U t) P) → (∀ t < T, P[U (t + 1) | ↑(dataFiltration 𝒳) t] ≤ᵐ[P] U t) → (∀ t ≤ T, (fun (x : ℕ → 𝒳) => (Es t x).toReal) ≤ᵐ[P] U t) → ∀ t ≤ T, snellEnvelope P Es T t ≤ᵐ[P] U t) ∧ ∀ (x : ℕ → 𝒳), ENNReal.ofReal (snellEnvelope P Es T 0 x) = ⨆ (τ : (ℕ → 𝒳) → ℕ∞), ⨆ (_ : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) τ), ∫⁻ (y : ℕ → 𝒳), Es (truncTime τ T y) y ∂P) ∧ ∀ (x : ℕ → 𝒳), eta 𝔓 Es T = ⨆ P ∈ 𝔓, ENNReal.ofReal (snellEnvelope P Es T 0 x)