From 1da2451ff57e37064463750bb671fc99833f14d1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 11:02:30 +0100 Subject: [PATCH 1/3] =?UTF-8?q?feat:=20the=20discrete-time=20Snell=20envel?= =?UTF-8?q?ope=20of=20an=20=E2=84=9D=E2=89=A50=E2=88=9E-valued=20process?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define `ProbabilityTheory.snellEnvelope E ℱ P n`, the essential supremum over the bounded stopping times τ ≥ n of the conditional Lebesgue expectations `P⁻[E τ|ℱ n]`, and prove that it is adapted, dominates an adapted process, is an ℝ≥0∞-valued supermartingale, is below every ℝ≥0∞-valued supermartingale that dominates the process, has expectation ⨆ τ, ∫⁻ E τ ∂P at time 0, is a test supermartingale when these expectations are at most 1, and agrees a.e. with the essential supremum of the real conditional expectations under finite expectations. Add the general lemmas `condLExp_piecewise` and `condLExp_ae_le_iff_forall_setLIntegral_le`. Co-Authored-By: Claude Code --- .../Function/ConditionalLExpectation.lean | 78 +++++ .../Probability/Martingale/SnellEnvelope.lean | 271 ++++++++++++++++++ 2 files changed, 349 insertions(+) create mode 100644 LMLExplore/MeasureTheory/Function/ConditionalLExpectation.lean create mode 100644 LMLExplore/Probability/Martingale/SnellEnvelope.lean diff --git a/LMLExplore/MeasureTheory/Function/ConditionalLExpectation.lean b/LMLExplore/MeasureTheory/Function/ConditionalLExpectation.lean new file mode 100644 index 00000000..ac2f1fe4 --- /dev/null +++ b/LMLExplore/MeasureTheory/Function/ConditionalLExpectation.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.MeasureTheory.Function.ConditionalLExpectation + +/-! +# Comparison and pasting of conditional Lebesgue expectations + +Two facts about Mathlib's conditional expectation `P⁻[X|m]` of an `ℝ≥0∞`-valued function, which +needs no integrability or measurability of `X`: +* it is almost everywhere below an `m`-measurable function `Y` exactly when the set integrals of + `X` over `m`-measurable sets are below those of `Y`; +* it commutes with pasting two functions along an `m`-measurable set. + +The second fact makes the conditional expectations of the values of a process at the stopping +times after a given time a family directed upward, the step behind the Snell envelope of optimal +stopping. + +## Main statements + +* `MeasureTheory.condLExp_ae_le_iff_forall_setLIntegral_le`: comparison with an `m`-measurable + function through set integrals. +* `MeasureTheory.condLExp_piecewise`: `P⁻[s.piecewise X Y|m] =ᵐ[P] s.piecewise P⁻[X|m] P⁻[Y|m]` + for an `m`-measurable set `s`. +-/ + +public section + +open Set +open scoped ENNReal + +namespace MeasureTheory + +variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {P : Measure Ω} {X Y : Ω → ℝ≥0∞} + +/-- For a sub-σ-algebra `m` on which `P` is σ-finite and an `m`-measurable `Y`, the conditional +expectation `P⁻[X|m]` is almost everywhere below `Y` exactly when the integral of `X` over every +`m`-measurable set is at most that of `Y`. -/ +theorem condLExp_ae_le_iff_forall_setLIntegral_le (hm : m ≤ mΩ) [SigmaFinite (P.trim hm)] + (hY : Measurable[m] Y) : + P⁻[X|m] ≤ᵐ[P] Y ↔ ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, X ω ∂P ≤ ∫⁻ ω in s, Y ω ∂P := by + refine ⟨fun h s hs ↦ ?_, fun h ↦ ?_⟩ + · rw [← setLIntegral_condLExp hm P X hs] + exact lintegral_mono_ae (ae_restrict_of_ae h) + · refine ae_le_of_ae_le_trim (hm := hm) <| ae_le_of_forall_setLIntegral_le_of_sigmaFinite + (μ := P.trim hm) (measurable_condLExp _ _ _) fun s hs _ ↦ ?_ + rw [setLIntegral_condLExp_trim hm _ _ hs, setLIntegral_trim hm hY hs] + exact h s hs + +/-- The conditional expectation given `m` of two functions pasted along an `m`-measurable set is +almost everywhere the pasting of their conditional expectations. No measurability or +integrability of the functions is needed. -/ +theorem condLExp_piecewise (hm : m ≤ mΩ) [SigmaFinite (P.trim hm)] {s : Set Ω} + [DecidablePred (· ∈ s)] (hs : MeasurableSet[m] s) (X Y : Ω → ℝ≥0∞) : + P⁻[s.piecewise X Y|m] =ᵐ[P] s.piecewise P⁻[X|m] P⁻[Y|m] := by + refine (ae_eq_condLExp hm P _ + ((measurable_condLExp m P X).piecewise hs (measurable_condLExp m P Y)) fun t ht ↦ ?_).symm + have hs' : MeasurableSet s := hm s hs + have ht' : MeasurableSet t := hm t ht + -- Split `t` along `s`; on each part both sides reduce to one conditional expectation. + rw [← lintegral_inter_add_sdiff _ t hs', ← lintegral_inter_add_sdiff (s.piecewise X Y) t hs'] + congr 1 + · calc ∫⁻ ω in t ∩ s, s.piecewise P⁻[X|m] P⁻[Y|m] ω ∂P = ∫⁻ ω in t ∩ s, P⁻[X|m] ω ∂P := + setLIntegral_congr_fun (ht'.inter hs') fun ω hω ↦ piecewise_eq_of_mem _ _ _ hω.2 + _ = ∫⁻ ω in t ∩ s, X ω ∂P := setLIntegral_condLExp hm P X (ht.inter hs) + _ = ∫⁻ ω in t ∩ s, s.piecewise X Y ω ∂P := + (setLIntegral_congr_fun (ht'.inter hs') fun ω hω ↦ piecewise_eq_of_mem s X Y hω.2).symm + · calc ∫⁻ ω in t \ s, s.piecewise P⁻[X|m] P⁻[Y|m] ω ∂P = ∫⁻ ω in t \ s, P⁻[Y|m] ω ∂P := + setLIntegral_congr_fun (ht'.diff hs') fun ω hω ↦ piecewise_eq_of_notMem _ _ _ hω.2 + _ = ∫⁻ ω in t \ s, Y ω ∂P := setLIntegral_condLExp hm P Y (ht.diff hs) + _ = ∫⁻ ω in t \ s, s.piecewise X Y ω ∂P := + (setLIntegral_congr_fun (ht'.diff hs') fun ω hω ↦ piecewise_eq_of_notMem s X Y hω.2).symm + +end MeasureTheory diff --git a/LMLExplore/Probability/Martingale/SnellEnvelope.lean b/LMLExplore/Probability/Martingale/SnellEnvelope.lean new file mode 100644 index 00000000..719700d6 --- /dev/null +++ b/LMLExplore/Probability/Martingale/SnellEnvelope.lean @@ -0,0 +1,271 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LMLExplore.MeasureTheory.Function.ConditionalLExpectation +public import LMLExplore.MeasureTheory.Function.EssSupFamily +public import LMLExplore.Probability.Martingale.OptionalStopping +public import Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner + +/-! +# The Snell envelope in discrete time + +For a process `E : ℕ → Ω → ℝ≥0∞`, a filtration `ℱ` indexed by `ℕ` and a measure `P`, the +**Snell envelope** of `E` at time `n` is the essential supremum, over the bounded stopping times +`τ ≥ n` with values in `ℕ`, of the conditional expectations given `ℱ n` of the values `E τ` of +the process at `τ`. It is the value at time `n` of optimal stopping after `n`, and, for an adapted +process, the smallest `ℝ≥0∞`-valued supermartingale that dominates it. + +The conditional expectations are Mathlib's conditional Lebesgue expectations `P⁻[X|m]` of +`ℝ≥0∞`-valued functions, and the essential supremum is `MeasureTheory.essSupFamily`. Neither needs +integrability, so the Snell envelope is defined and is a supermartingale for every process. When +the values of the process have finite expectations, it agrees almost surely with the essential +supremum of the conditional expectations `P[(E τ).toReal|ℱ n]` of the real values +(`ProbabilityTheory.snellEnvelope_ae_eq_essSupFamily_condExp`). + +Its role in anytime-valid inference is the characterization of e-processes: an adapted process +whose values at all bounded stopping times have expectation at most `1` under `P` is dominated by +a test supermartingale for `P`, its Snell envelope [RRLK, Lemma 6, Appendix A]. + +The proofs follow the essential supremum description of the Snell envelope [FS16, Chapter 6]. The +family of conditional expectations at the bounded stopping times after `n` is directed upward, +since pasting two such stopping times along the set where one of their conditional expectations +is the larger gives another one. So the set integrals of the Snell envelope are the suprema of the +set integrals of the process at those stopping times, from which the supermartingale property and +the expectation at time `0` follow; minimality is optional stopping for bounded stopping times. + +## Main definitions + +* `ProbabilityTheory.snellEnvelope E ℱ P`: the Snell envelope of `E`. + +## Main statements + +* `ProbabilityTheory.condLExp_ae_le_snellEnvelope`, `ProbabilityTheory.snellEnvelope_ae_le`, + `ProbabilityTheory.snellEnvelope_ae_le_iff`: the Snell envelope at time `n` is the almost + everywhere least function above the conditional expectations at the bounded stopping times + after `n`. +* `ProbabilityTheory.ae_le_snellEnvelope`: the Snell envelope of an adapted process dominates it. +* `ProbabilityTheory.setLIntegral_snellEnvelope`: its integral over an `ℱ n`-measurable set is the + supremum of the integrals of the process at the bounded stopping times after `n`, and + `ProbabilityTheory.lintegral_snellEnvelope_zero`: its expectation at time `0` is + `⨆ τ, ∫⁻ E τ ∂P` over the bounded stopping times. +* `ProbabilityTheory.isENNSupermartingale_snellEnvelope`: it is an `ℝ≥0∞`-valued supermartingale, + and `ProbabilityTheory.IsENNSupermartingale.snellEnvelope_ae_le`: it is below every + `ℝ≥0∞`-valued supermartingale that dominates the process. +* `ProbabilityTheory.isTestSupermartingale_snellEnvelope`: it is a test supermartingale when the + expectations of the process at bounded stopping times are at most `1`. + +## References + +* [FS16] H. Föllmer and A. Schied, *Stochastic Finance: An Introduction in Discrete Time*, + 4th edition, De Gruyter, 2016, Chapter 6. +* [RRLK] A. Ramdas, J. Ruf, M. Larsson and W. M. Koolen, *Admissible anytime-valid sequential + inference must rely on nonnegative martingales*, arXiv:2009.03167v3, Lemma 6 and Appendix A. +-/ + +public section + +open MeasureTheory Filter Set +open scoped ENNReal + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {ℱ : Filtration ℕ mΩ} {P : Measure Ω} + {E M : ℕ → Ω → ℝ≥0∞} {τ : Ω → ℕ} {n N : ℕ} {h : Ω → ℝ≥0∞} + +/-- The **Snell envelope** of a process `E : ℕ → Ω → ℝ≥0∞` for a filtration `ℱ` and a measure +`P`: at time `n`, the essential supremum under `P`, over the stopping times `τ` with values in +`ℕ` that are at least `n` and bounded by a constant, of the conditional expectation +`P⁻[E τ|ℱ n]` of the value of the process at `τ`. -/ +noncomputable def snellEnvelope (E : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ) (P : Measure Ω) + (n : ℕ) : Ω → ℝ≥0∞ := + essSupFamily (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ + (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) P + +/-- The defining equation of `snellEnvelope`. -/ +theorem snellEnvelope_def (E : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ) (P : Measure Ω) (n : ℕ) : + snellEnvelope E ℱ P n = + essSupFamily (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ + (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) P := + (rfl) + +/-- The Snell envelope is adapted, for every process. -/ +theorem adapted_snellEnvelope (E : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ) (P : Measure Ω) : + Adapted ℱ (snellEnvelope E ℱ P) := fun _ ↦ + measurable_essSupFamily fun _ ↦ measurable_condLExp _ _ _ + +/-- The Snell envelope at time `n` dominates almost everywhere the conditional expectation given +`ℱ n` of the value of the process at every bounded stopping time `τ ≥ n`. -/ +theorem condLExp_ae_le_snellEnvelope [SigmaFiniteFiltration P ℱ] + (hτ : IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) (hnτ : ∀ ω, n ≤ τ ω) + (hτN : ∀ ω, τ ω ≤ N) : + P⁻[fun ω ↦ E (τ ω) ω|ℱ n] ≤ᵐ[P] snellEnvelope E ℱ P n := by + have := SigmaFinite.of_trim (μ := P) (ℱ.le n) + rw [snellEnvelope_def] + exact ae_le_essSupFamily (μ := P) + (fun τ ↦ (measurable_condLExp' (ℱ n) P fun ω ↦ E (τ.1 ω) ω).aemeasurable) + (⟨τ, hτ, hnτ, N, hτN⟩ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ + (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N}) + +/-- The Snell envelope at time `n` is almost everywhere below every function that dominates +almost everywhere the conditional expectations given `ℱ n` of the values of the process at the +bounded stopping times `τ ≥ n`. -/ +theorem snellEnvelope_ae_le + (hh : ∀ τ : Ω → ℕ, (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) → (∀ ω, n ≤ τ ω) → + (∃ N : ℕ, ∀ ω, τ ω ≤ N) → P⁻[fun ω ↦ E (τ ω) ω|ℱ n] ≤ᵐ[P] h) : + snellEnvelope E ℱ P n ≤ᵐ[P] h := + essSupFamily_ae_le fun τ ↦ hh τ.1 τ.2.1 τ.2.2.1 τ.2.2.2 + +/-- A function dominates the Snell envelope at time `n` almost everywhere exactly when it +dominates almost everywhere the conditional expectations given `ℱ n` of the values of the process +at the bounded stopping times `τ ≥ n`. -/ +theorem snellEnvelope_ae_le_iff [SigmaFiniteFiltration P ℱ] : + snellEnvelope E ℱ P n ≤ᵐ[P] h ↔ ∀ τ : Ω → ℕ, (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) → + (∀ ω, n ≤ τ ω) → (∃ N : ℕ, ∀ ω, τ ω ≤ N) → P⁻[fun ω ↦ E (τ ω) ω|ℱ n] ≤ᵐ[P] h := + ⟨fun hh _ hτ hnτ ⟨_, hτN⟩ ↦ (condLExp_ae_le_snellEnvelope hτ hnτ hτN).trans hh, + snellEnvelope_ae_le⟩ + +/-- The Snell envelope of an adapted process dominates it almost everywhere at every time. -/ +theorem ae_le_snellEnvelope [SigmaFiniteFiltration P ℱ] (hE : Adapted ℱ E) (n : ℕ) : + E n ≤ᵐ[P] snellEnvelope E ℱ P n := by + have h := condLExp_ae_le_snellEnvelope (E := E) (ℱ := ℱ) (P := P) (τ := fun _ ↦ n) (N := n) + (isStoppingTime_natCast n) (fun _ ↦ le_rfl) fun _ ↦ le_rfl + rwa [condLExp_eq_self (ℱ.le n) P (hE n)] at h + +/-- The conditional expectations given `ℱ n` of the values of a process at the bounded stopping +times `τ ≥ n` form a family directed upward almost everywhere: pasting two stopping times along +the `ℱ n`-measurable set where the first conditional expectation is the larger gives a bounded +stopping time `τ ≥ n` whose conditional expectation is the maximum of the two. -/ +private theorem directed_condLExp [SigmaFiniteFiltration P ℱ] (E : ℕ → Ω → ℝ≥0∞) (n : ℕ) : + Directed (· ≤ᵐ[P] ·) (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ + (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) := by + classical + rintro ⟨τ₁, hτ₁, hnτ₁, N₁, hτN₁⟩ ⟨τ₂, hτ₂, hnτ₂, N₂, hτN₂⟩ + set A := {ω | P⁻[fun ω ↦ E (τ₂ ω) ω|ℱ n] ω ≤ P⁻[fun ω ↦ E (τ₁ ω) ω|ℱ n] ω} + have hA : MeasurableSet[ℱ n] A := + measurableSet_le (measurable_condLExp _ _ _) (measurable_condLExp _ _ _) + have hτ : IsStoppingTime ℱ fun ω ↦ (A.piecewise τ₁ τ₂ ω : WithTop ℕ) := by + have h := hτ₁.piecewise_of_le hτ₂ (i := n) + (fun ω ↦ by rw [← Nat.cast_withTop]; exact_mod_cast hnτ₁ ω) + (fun ω ↦ by rw [← Nat.cast_withTop]; exact_mod_cast hnτ₂ ω) hA + convert h using 1 + funext ω + by_cases hω : ω ∈ A <;> simp [hω] + have hpw : (fun ω ↦ E (A.piecewise τ₁ τ₂ ω) ω) = + A.piecewise (fun ω ↦ E (τ₁ ω) ω) (fun ω ↦ E (τ₂ ω) ω) := by + funext ω + by_cases hω : ω ∈ A <;> simp [hω] + have h_eq := condLExp_piecewise (P := P) (ℱ.le n) hA (fun ω ↦ E (τ₁ ω) ω) (fun ω ↦ E (τ₂ ω) ω) + refine ⟨⟨A.piecewise τ₁ τ₂, hτ, fun ω ↦ ?_, max N₁ N₂, fun ω ↦ ?_⟩, ?_, ?_⟩ + · by_cases hω : ω ∈ A <;> simp [hω, hnτ₁, hnτ₂] + · by_cases hω : ω ∈ A <;> simp [hω, hτN₁, hτN₂] + · filter_upwards [h_eq] with ω hω + simp only [hpw, hω] + by_cases hωA : ω ∈ A + · rw [piecewise_eq_of_mem _ _ _ hωA] + · rw [piecewise_eq_of_notMem _ _ _ hωA] + exact (not_le.1 hωA).le + · filter_upwards [h_eq] with ω hω + simp only [hpw, hω] + by_cases hωA : ω ∈ A + · rw [piecewise_eq_of_mem _ _ _ hωA] + exact hωA + · rw [piecewise_eq_of_notMem _ _ _ hωA] + +/-- The integral of the Snell envelope at time `n` over an `ℱ n`-measurable set `s` is the +supremum of the integrals over `s` of the process at the bounded stopping times `τ ≥ n`. -/ +theorem setLIntegral_snellEnvelope [SigmaFiniteFiltration P ℱ] {s : Set Ω} + (hs : MeasurableSet[ℱ n] s) : + ∫⁻ ω in s, snellEnvelope E ℱ P n ω ∂P = + ⨆ (τ : Ω → ℕ) (_ : IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) (_ : ∀ ω, n ≤ τ ω) + (_ : ∃ N : ℕ, ∀ ω, τ ω ≤ N), ∫⁻ ω in s, E (τ ω) ω ∂P := by + have := SigmaFinite.of_trim (μ := P) (ℱ.le n) + rw [snellEnvelope_def, setLIntegral_essSupFamily_of_directed + (fun _ ↦ (measurable_condLExp' _ _ _).aemeasurable) (directed_condLExp (P := P) (ℱ := ℱ) E n)] + simp only [iSup_subtype, iSup_and, setLIntegral_condLExp (ℱ.le n) P _ hs] + +/-- The expectation of the Snell envelope at time `0` is the supremum of the expectations of the +process at the bounded stopping times. -/ +theorem lintegral_snellEnvelope_zero [SigmaFiniteFiltration P ℱ] : + ∫⁻ ω, snellEnvelope E ℱ P 0 ω ∂P = + ⨆ (τ : Ω → ℕ) (_ : IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) + (_ : ∃ N : ℕ, ∀ ω, τ ω ≤ N), ∫⁻ ω, E (τ ω) ω ∂P := by + simpa using setLIntegral_snellEnvelope (E := E) (P := P) (n := 0) MeasurableSet.univ + +/-- The Snell envelope of every process is an `ℝ≥0∞`-valued supermartingale. -/ +theorem isENNSupermartingale_snellEnvelope [SigmaFiniteFiltration P ℱ] (E : ℕ → Ω → ℝ≥0∞) : + IsENNSupermartingale (snellEnvelope E ℱ P) ℱ {P} := by + refine ⟨adapted_snellEnvelope E ℱ P, fun Q hQ n s hs ↦ ?_⟩ + rw [mem_singleton_iff.1 hQ, setLIntegral_snellEnvelope (ℱ.mono n.le_succ s hs), + setLIntegral_snellEnvelope hs] + -- The stopping times after `n + 1` are among those after `n`. + exact iSup₂_le fun τ hτ ↦ iSup₂_le fun hnτ hτN ↦ le_iSup₂_of_le τ hτ <| + le_iSup₂_of_le (fun ω ↦ n.le_succ.trans (hnτ ω)) hτN le_rfl + +/-- **Minimality of the Snell envelope.** The Snell envelope is almost everywhere below every +`ℝ≥0∞`-valued supermartingale that dominates the process almost everywhere at every time. -/ +theorem IsENNSupermartingale.snellEnvelope_ae_le [SigmaFiniteFiltration P ℱ] + (hM : IsENNSupermartingale M ℱ {P}) (hEM : ∀ n, E n ≤ᵐ[P] M n) (n : ℕ) : + snellEnvelope E ℱ P n ≤ᵐ[P] M n := by + refine ProbabilityTheory.snellEnvelope_ae_le fun τ hτ hnτ ⟨N, hτN⟩ ↦ ?_ + rw [condLExp_ae_le_iff_forall_setLIntegral_le (ℱ.le n) (hM.adapted n)] + intro s hs + have hEM' : ∀ᵐ ω ∂P, ∀ k, E k ω ≤ M k ω := ae_all_iff.2 hEM + calc ∫⁻ ω in s, E (τ ω) ω ∂P ≤ ∫⁻ ω in s, M (τ ω) ω ∂P := + lintegral_mono_ae (ae_restrict_of_ae (hEM'.mono fun ω hω ↦ hω (τ ω))) + _ ≤ ∫⁻ ω in s, M n ω ∂P := by + -- Optional stopping between the constant time `n` and `τ`. + have h := hM.setLIntegral_stoppedValueLimsup_le_of_le_const (mem_singleton P) + (isStoppingTime_natCast n) hτ (fun ω ↦ by exact_mod_cast hnτ ω) (N := N) + (fun ω ↦ by exact_mod_cast hτN ω) (s := s) + ((isStoppingTime_natCast n).le_measurableSpace_of_const_le + (fun _ ↦ (Nat.cast_withTop n).symm.le) s hs) + rwa [stoppedValueLimsup_natCast, stoppedValueLimsup_const] at h + +/-- The Snell envelope of a process whose expectations at the bounded stopping times are at most +`1` under `P` is a test supermartingale for `P`. -/ +theorem isTestSupermartingale_snellEnvelope [SigmaFiniteFiltration P ℱ] + (hE : ∀ τ : Ω → ℕ, (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) → + (∃ N : ℕ, ∀ ω, τ ω ≤ N) → ∫⁻ ω, E (τ ω) ω ∂P ≤ 1) : + IsTestSupermartingale (snellEnvelope E ℱ P) ℱ {P} := + ⟨isENNSupermartingale_snellEnvelope E, fun Q hQ ↦ by + rw [mem_singleton_iff.1 hQ, lintegral_snellEnvelope_zero] + exact iSup₂_le fun τ hτ ↦ iSup_le (hE τ hτ)⟩ + +/-- For a process of measurable functions with finite expectations, the Snell envelope agrees +almost everywhere with the essential supremum, over the bounded stopping times `τ ≥ n`, of the +conditional expectations `P[(E τ).toReal|ℱ n]` of the real values of the process at `τ`, the +form in which it is classically defined. -/ +theorem snellEnvelope_ae_eq_essSupFamily_condExp [SigmaFiniteFiltration P ℱ] + (hE : ∀ n, Measurable (E n)) (hE_int : ∀ n, ∫⁻ ω, E n ω ∂P ≠ ∞) (n : ℕ) : + snellEnvelope E ℱ P n =ᵐ[P] + essSupFamily (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ + (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ + fun ω ↦ ENNReal.ofReal (P[fun ω ↦ (E (τ.1 ω) ω).toReal|ℱ n] ω)) P := by + have := SigmaFinite.of_trim (μ := P) (ℱ.le n) + have h (τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ + (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N}) : + P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n] =ᵐ[P] + fun ω ↦ ENNReal.ofReal (P[fun ω ↦ (E (τ.1 ω) ω).toReal|ℱ n] ω) := by + obtain ⟨τ, hτ, -, N, hτN⟩ := τ + have hmeas : Measurable fun ω ↦ E (τ ω) ω := by + simpa using measurable_stoppedValueLimsup hE hτ.measurable' + -- The value at `τ ≤ N` is below the sum of the values at the times up to `N`. + have hle : ∫⁻ ω, E (τ ω) ω ∂P ≤ ∑ k ∈ Finset.range (N + 1), ∫⁻ ω, E k ω ∂P := by + rw [← lintegral_finsetSum (Finset.range (N + 1)) fun k _ ↦ hE k] + exact lintegral_mono fun ω ↦ Finset.single_le_sum (f := fun k ↦ E k ω) + (fun _ _ ↦ zero_le) (Finset.mem_range.2 (Nat.lt_succ_of_le (hτN ω))) + have hint : ∫⁻ ω, E (τ ω) ω ∂P ≠ ∞ := + ne_top_of_le_ne_top (ENNReal.sum_ne_top.2 fun k _ ↦ hE_int k) hle + filter_upwards [toReal_condLExp (ℱ n) hmeas.aemeasurable hint, + condLExp_ne_top (mΩ := ℱ n) hint] with ω h₁ h₂ + rw [← h₁, ENNReal.ofReal_toReal h₂] + rw [snellEnvelope_def] + exact (essSupFamily_mono_ae (fun _ ↦ integrable_condExp.aemeasurable.ennreal_ofReal) + fun τ ↦ (h τ).le).antisymm (essSupFamily_mono_ae + (fun _ ↦ (measurable_condLExp' _ _ _).aemeasurable) fun τ ↦ (h τ).symm.le) + +end ProbabilityTheory From 578a377410ffe000ad25561c565a9888f0da123f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 11:31:52 +0100 Subject: [PATCH 2/3] refactor: name the bounded stopping times after a time in the Snell envelope API MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Add `boundedStoppingTimesFrom ℱ n` with its membership, constant-time, antitonicity and pasting lemmas, and state the Snell envelope and its API over it. - Generalise `IsENNSupermartingale.snellEnvelope_ae_le` to supermartingales for a set `S` with `hP : P ∈ S`. - Extract `lintegral_stoppedValueLimsup_le_sum` into `StoppedValue.lean`. - Prove `isCondEVar_iff_condLExp_le` with `condLExp_ae_le_iff_forall_setLIntegral_le`. Co-Authored-By: Claude Code --- LMLExplore/EValues/CondEVariable.lean | 11 +- .../Probability/Martingale/SnellEnvelope.lean | 163 ++++++++++-------- .../Probability/Process/StoppedValue.lean | 21 +++ 3 files changed, 121 insertions(+), 74 deletions(-) diff --git a/LMLExplore/EValues/CondEVariable.lean b/LMLExplore/EValues/CondEVariable.lean index c13a6ffe..6e4aaec3 100644 --- a/LMLExplore/EValues/CondEVariable.lean +++ b/LMLExplore/EValues/CondEVariable.lean @@ -5,6 +5,7 @@ Authors: LMLExplore contributors -/ module +public import LMLExplore.MeasureTheory.Function.ConditionalLExpectation public import LMLExplore.MeasureTheory.Measure.WithDensity public import Mathlib.MeasureTheory.Function.ConditionalLExpectation public import Statlib.EValues.EVariable @@ -164,14 +165,12 @@ conditional e-variable given `m` exactly when it is measurable and its condition `P⁻[X|m]` is almost surely at most `1` under every `P ∈ S`. -/ theorem isCondEVar_iff_condLExp_le (hm : m ≤ mΩ) (hS : ∀ P ∈ S, SigmaFinite (P.trim hm)) : IsCondEVar X m S ↔ Measurable X ∧ ∀ P ∈ S, P⁻[X|m] ≤ᵐ[P] 1 := by + have h1 : Measurable[m] (1 : Ω → ℝ≥0∞) := @measurable_const _ _ _ m 1 refine ⟨fun hX ↦ ⟨hX.measurable, fun P hP ↦ ?_⟩, fun hX ↦ ⟨hX.1, fun P hP s hs ↦ ?_⟩⟩ <;> have := hS P hP - · refine ae_le_of_ae_le_trim (hm := hm) <| ae_le_of_forall_setLIntegral_le_of_sigmaFinite - (μ := P.trim hm) (measurable_condLExp _ _ _) fun s hs _ ↦ ?_ - rw [setLIntegral_condLExp_trim hm _ _ hs] - simpa [trim_measurableSet_eq hm hs] using hX.setLIntegral_le P hP s hs - · rw [← setLIntegral_condLExp hm P X hs] - simpa using lintegral_mono_ae (ae_restrict_of_ae (hX.2 P hP)) + · rw [condLExp_ae_le_iff_forall_setLIntegral_le hm h1] + simpa using hX.setLIntegral_le P hP + · simpa using (condLExp_ae_le_iff_forall_setLIntegral_le hm h1).1 (hX.2 P hP) s hs /-- When the restrictions to a sub-σ-algebra `m` of the members of `S` are σ-finite, `X` is an exact conditional e-variable given `m` exactly when it is measurable and its conditional diff --git a/LMLExplore/Probability/Martingale/SnellEnvelope.lean b/LMLExplore/Probability/Martingale/SnellEnvelope.lean index 719700d6..9b338834 100644 --- a/LMLExplore/Probability/Martingale/SnellEnvelope.lean +++ b/LMLExplore/Probability/Martingale/SnellEnvelope.lean @@ -39,6 +39,8 @@ the expectation at time `0` follow; minimality is optional stopping for bounded ## Main definitions +* `ProbabilityTheory.boundedStoppingTimesFrom ℱ n`: the bounded `ℕ`-valued stopping times after + `n`, which index the Snell envelope at time `n`. * `ProbabilityTheory.snellEnvelope E ℱ P`: the Snell envelope of `E`. ## Main statements @@ -74,22 +76,65 @@ open scoped ENNReal namespace ProbabilityTheory variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {ℱ : Filtration ℕ mΩ} {P : Measure Ω} - {E M : ℕ → Ω → ℝ≥0∞} {τ : Ω → ℕ} {n N : ℕ} {h : Ω → ℝ≥0∞} + {S : Set (Measure Ω)} {E M : ℕ → Ω → ℝ≥0∞} {τ τ₁ τ₂ : Ω → ℕ} {n : ℕ} {h : Ω → ℝ≥0∞} + +/-! ### Bounded stopping times after a time -/ + +/-- The **bounded stopping times after `n`** of a filtration `ℱ` indexed by `ℕ`: the stopping +times `τ` with values in `ℕ` that are at least `n` and bounded by a constant. -/ +def boundedStoppingTimesFrom (ℱ : Filtration ℕ mΩ) (n : ℕ) : Set (Ω → ℕ) := + {τ | (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) ∧ (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} + +/-- Membership in `boundedStoppingTimesFrom ℱ n`, unfolded. -/ +@[simp] +theorem mem_boundedStoppingTimesFrom_iff : + τ ∈ boundedStoppingTimesFrom ℱ n ↔ + (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) ∧ (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N := + Iff.rfl + +/-- The constant time `n` is a bounded stopping time after `n`. -/ +theorem const_mem_boundedStoppingTimesFrom (ℱ : Filtration ℕ mΩ) (n : ℕ) : + (fun _ : Ω ↦ n) ∈ boundedStoppingTimesFrom ℱ n := + ⟨isStoppingTime_natCast n, fun _ ↦ le_rfl, n, fun _ ↦ le_rfl⟩ + +/-- A bounded stopping time after a time `n` is a bounded stopping time after every earlier +time. -/ +theorem boundedStoppingTimesFrom_anti (ℱ : Filtration ℕ mΩ) : + Antitone (boundedStoppingTimesFrom ℱ) := fun _ _ hmn _ ⟨hτ, hnτ, hτN⟩ ↦ + ⟨hτ, fun ω ↦ hmn.trans (hnτ ω), hτN⟩ + +/-- Pasting two bounded stopping times after `n` along an `ℱ n`-measurable set gives a bounded +stopping time after `n`. -/ +theorem piecewise_mem_boundedStoppingTimesFrom {A : Set Ω} [DecidablePred (· ∈ A)] + (hA : MeasurableSet[ℱ n] A) (hτ₁ : τ₁ ∈ boundedStoppingTimesFrom ℱ n) + (hτ₂ : τ₂ ∈ boundedStoppingTimesFrom ℱ n) : + A.piecewise τ₁ τ₂ ∈ boundedStoppingTimesFrom ℱ n := by + obtain ⟨hτ₁, hnτ₁, N₁, hτN₁⟩ := hτ₁ + obtain ⟨hτ₂, hnτ₂, N₂, hτN₂⟩ := hτ₂ + refine ⟨?_, fun ω ↦ ?_, max N₁ N₂, fun ω ↦ ?_⟩ + · have h := hτ₁.piecewise_of_le hτ₂ (i := n) + (fun ω ↦ by rw [← Nat.cast_withTop]; exact_mod_cast hnτ₁ ω) + (fun ω ↦ by rw [← Nat.cast_withTop]; exact_mod_cast hnτ₂ ω) hA + convert h using 1 + funext ω + by_cases hω : ω ∈ A <;> simp [hω] + · by_cases hω : ω ∈ A <;> simp [hω, hnτ₁, hnτ₂] + · by_cases hω : ω ∈ A <;> simp [hω, hτN₁, hτN₂] + +/-! ### The Snell envelope -/ /-- The **Snell envelope** of a process `E : ℕ → Ω → ℝ≥0∞` for a filtration `ℱ` and a measure -`P`: at time `n`, the essential supremum under `P`, over the stopping times `τ` with values in -`ℕ` that are at least `n` and bounded by a constant, of the conditional expectation +`P`: at time `n`, the essential supremum under `P`, over the bounded stopping times `τ` after `n` +(`ProbabilityTheory.boundedStoppingTimesFrom ℱ n`), of the conditional expectation `P⁻[E τ|ℱ n]` of the value of the process at `τ`. -/ noncomputable def snellEnvelope (E : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ) (P : Measure Ω) (n : ℕ) : Ω → ℝ≥0∞ := - essSupFamily (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ - (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) P + essSupFamily (fun τ : boundedStoppingTimesFrom ℱ n ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) P /-- The defining equation of `snellEnvelope`. -/ theorem snellEnvelope_def (E : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ) (P : Measure Ω) (n : ℕ) : snellEnvelope E ℱ P n = - essSupFamily (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ - (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) P := + essSupFamily (fun τ : boundedStoppingTimesFrom ℱ n ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) P := (rfl) /-- The Snell envelope is adapted, for every process. -/ @@ -98,70 +143,57 @@ theorem adapted_snellEnvelope (E : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration measurable_essSupFamily fun _ ↦ measurable_condLExp _ _ _ /-- The Snell envelope at time `n` dominates almost everywhere the conditional expectation given -`ℱ n` of the value of the process at every bounded stopping time `τ ≥ n`. -/ +`ℱ n` of the value of the process at every bounded stopping time `τ` after `n`. -/ theorem condLExp_ae_le_snellEnvelope [SigmaFiniteFiltration P ℱ] - (hτ : IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) (hnτ : ∀ ω, n ≤ τ ω) - (hτN : ∀ ω, τ ω ≤ N) : + (hτ : τ ∈ boundedStoppingTimesFrom ℱ n) : P⁻[fun ω ↦ E (τ ω) ω|ℱ n] ≤ᵐ[P] snellEnvelope E ℱ P n := by have := SigmaFinite.of_trim (μ := P) (ℱ.le n) rw [snellEnvelope_def] exact ae_le_essSupFamily (μ := P) - (fun τ ↦ (measurable_condLExp' (ℱ n) P fun ω ↦ E (τ.1 ω) ω).aemeasurable) - (⟨τ, hτ, hnτ, N, hτN⟩ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ - (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N}) + (fun τ : boundedStoppingTimesFrom ℱ n ↦ + (measurable_condLExp' (ℱ n) P fun ω ↦ E (τ.1 ω) ω).aemeasurable) ⟨τ, hτ⟩ /-- The Snell envelope at time `n` is almost everywhere below every function that dominates almost everywhere the conditional expectations given `ℱ n` of the values of the process at the -bounded stopping times `τ ≥ n`. -/ +bounded stopping times `τ` after `n`. -/ theorem snellEnvelope_ae_le - (hh : ∀ τ : Ω → ℕ, (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) → (∀ ω, n ≤ τ ω) → - (∃ N : ℕ, ∀ ω, τ ω ≤ N) → P⁻[fun ω ↦ E (τ ω) ω|ℱ n] ≤ᵐ[P] h) : + (hh : ∀ τ ∈ boundedStoppingTimesFrom ℱ n, P⁻[fun ω ↦ E (τ ω) ω | ℱ n] ≤ᵐ[P] h) : snellEnvelope E ℱ P n ≤ᵐ[P] h := - essSupFamily_ae_le fun τ ↦ hh τ.1 τ.2.1 τ.2.2.1 τ.2.2.2 + essSupFamily_ae_le fun τ ↦ hh τ.1 τ.2 /-- A function dominates the Snell envelope at time `n` almost everywhere exactly when it dominates almost everywhere the conditional expectations given `ℱ n` of the values of the process -at the bounded stopping times `τ ≥ n`. -/ +at the bounded stopping times `τ` after `n`. -/ theorem snellEnvelope_ae_le_iff [SigmaFiniteFiltration P ℱ] : - snellEnvelope E ℱ P n ≤ᵐ[P] h ↔ ∀ τ : Ω → ℕ, (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) → - (∀ ω, n ≤ τ ω) → (∃ N : ℕ, ∀ ω, τ ω ≤ N) → P⁻[fun ω ↦ E (τ ω) ω|ℱ n] ≤ᵐ[P] h := - ⟨fun hh _ hτ hnτ ⟨_, hτN⟩ ↦ (condLExp_ae_le_snellEnvelope hτ hnτ hτN).trans hh, - snellEnvelope_ae_le⟩ + snellEnvelope E ℱ P n ≤ᵐ[P] h ↔ + ∀ τ ∈ boundedStoppingTimesFrom ℱ n, P⁻[fun ω ↦ E (τ ω) ω|ℱ n] ≤ᵐ[P] h := + ⟨fun hh _ hτ ↦ (condLExp_ae_le_snellEnvelope hτ).trans hh, snellEnvelope_ae_le⟩ /-- The Snell envelope of an adapted process dominates it almost everywhere at every time. -/ theorem ae_le_snellEnvelope [SigmaFiniteFiltration P ℱ] (hE : Adapted ℱ E) (n : ℕ) : E n ≤ᵐ[P] snellEnvelope E ℱ P n := by - have h := condLExp_ae_le_snellEnvelope (E := E) (ℱ := ℱ) (P := P) (τ := fun _ ↦ n) (N := n) - (isStoppingTime_natCast n) (fun _ ↦ le_rfl) fun _ ↦ le_rfl + have h := condLExp_ae_le_snellEnvelope (E := E) (P := P) + (const_mem_boundedStoppingTimesFrom ℱ n) rwa [condLExp_eq_self (ℱ.le n) P (hE n)] at h /-- The conditional expectations given `ℱ n` of the values of a process at the bounded stopping -times `τ ≥ n` form a family directed upward almost everywhere: pasting two stopping times along -the `ℱ n`-measurable set where the first conditional expectation is the larger gives a bounded -stopping time `τ ≥ n` whose conditional expectation is the maximum of the two. -/ +times `τ` after `n` form a family directed upward almost everywhere: pasting two stopping times +along the `ℱ n`-measurable set where the first conditional expectation is the larger gives a +bounded stopping time after `n` whose conditional expectation is the maximum of the two. -/ private theorem directed_condLExp [SigmaFiniteFiltration P ℱ] (E : ℕ → Ω → ℝ≥0∞) (n : ℕ) : - Directed (· ≤ᵐ[P] ·) (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ - (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) := by + Directed (· ≤ᵐ[P] ·) + (fun τ : boundedStoppingTimesFrom ℱ n ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) := by classical - rintro ⟨τ₁, hτ₁, hnτ₁, N₁, hτN₁⟩ ⟨τ₂, hτ₂, hnτ₂, N₂, hτN₂⟩ + rintro ⟨τ₁, hτ₁⟩ ⟨τ₂, hτ₂⟩ set A := {ω | P⁻[fun ω ↦ E (τ₂ ω) ω|ℱ n] ω ≤ P⁻[fun ω ↦ E (τ₁ ω) ω|ℱ n] ω} have hA : MeasurableSet[ℱ n] A := measurableSet_le (measurable_condLExp _ _ _) (measurable_condLExp _ _ _) - have hτ : IsStoppingTime ℱ fun ω ↦ (A.piecewise τ₁ τ₂ ω : WithTop ℕ) := by - have h := hτ₁.piecewise_of_le hτ₂ (i := n) - (fun ω ↦ by rw [← Nat.cast_withTop]; exact_mod_cast hnτ₁ ω) - (fun ω ↦ by rw [← Nat.cast_withTop]; exact_mod_cast hnτ₂ ω) hA - convert h using 1 - funext ω - by_cases hω : ω ∈ A <;> simp [hω] have hpw : (fun ω ↦ E (A.piecewise τ₁ τ₂ ω) ω) = A.piecewise (fun ω ↦ E (τ₁ ω) ω) (fun ω ↦ E (τ₂ ω) ω) := by funext ω by_cases hω : ω ∈ A <;> simp [hω] have h_eq := condLExp_piecewise (P := P) (ℱ.le n) hA (fun ω ↦ E (τ₁ ω) ω) (fun ω ↦ E (τ₂ ω) ω) - refine ⟨⟨A.piecewise τ₁ τ₂, hτ, fun ω ↦ ?_, max N₁ N₂, fun ω ↦ ?_⟩, ?_, ?_⟩ - · by_cases hω : ω ∈ A <;> simp [hω, hnτ₁, hnτ₂] - · by_cases hω : ω ∈ A <;> simp [hω, hτN₁, hτN₂] + refine ⟨⟨A.piecewise τ₁ τ₂, piecewise_mem_boundedStoppingTimesFrom hA hτ₁ hτ₂⟩, ?_, ?_⟩ · filter_upwards [h_eq] with ω hω simp only [hpw, hω] by_cases hωA : ω ∈ A @@ -176,24 +208,23 @@ private theorem directed_condLExp [SigmaFiniteFiltration P ℱ] (E : ℕ → Ω · rw [piecewise_eq_of_notMem _ _ _ hωA] /-- The integral of the Snell envelope at time `n` over an `ℱ n`-measurable set `s` is the -supremum of the integrals over `s` of the process at the bounded stopping times `τ ≥ n`. -/ +supremum of the integrals over `s` of the process at the bounded stopping times `τ` after `n`. -/ theorem setLIntegral_snellEnvelope [SigmaFiniteFiltration P ℱ] {s : Set Ω} (hs : MeasurableSet[ℱ n] s) : ∫⁻ ω in s, snellEnvelope E ℱ P n ω ∂P = - ⨆ (τ : Ω → ℕ) (_ : IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) (_ : ∀ ω, n ≤ τ ω) - (_ : ∃ N : ℕ, ∀ ω, τ ω ≤ N), ∫⁻ ω in s, E (τ ω) ω ∂P := by + ⨆ τ ∈ boundedStoppingTimesFrom ℱ n, ∫⁻ ω in s, E (τ ω) ω ∂P := by have := SigmaFinite.of_trim (μ := P) (ℱ.le n) rw [snellEnvelope_def, setLIntegral_essSupFamily_of_directed (fun _ ↦ (measurable_condLExp' _ _ _).aemeasurable) (directed_condLExp (P := P) (ℱ := ℱ) E n)] - simp only [iSup_subtype, iSup_and, setLIntegral_condLExp (ℱ.le n) P _ hs] + simp only [iSup_subtype, setLIntegral_condLExp (ℱ.le n) P _ hs] /-- The expectation of the Snell envelope at time `0` is the supremum of the expectations of the process at the bounded stopping times. -/ theorem lintegral_snellEnvelope_zero [SigmaFiniteFiltration P ℱ] : ∫⁻ ω, snellEnvelope E ℱ P 0 ω ∂P = - ⨆ (τ : Ω → ℕ) (_ : IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) - (_ : ∃ N : ℕ, ∀ ω, τ ω ≤ N), ∫⁻ ω, E (τ ω) ω ∂P := by - simpa using setLIntegral_snellEnvelope (E := E) (P := P) (n := 0) MeasurableSet.univ + ⨆ τ ∈ boundedStoppingTimesFrom ℱ 0, ∫⁻ ω, E (τ ω) ω ∂P := by + simpa only [Measure.restrict_univ] using + setLIntegral_snellEnvelope (E := E) (P := P) (n := 0) MeasurableSet.univ /-- The Snell envelope of every process is an `ℝ≥0∞`-valued supermartingale. -/ theorem isENNSupermartingale_snellEnvelope [SigmaFiniteFiltration P ℱ] (E : ℕ → Ω → ℝ≥0∞) : @@ -202,15 +233,15 @@ theorem isENNSupermartingale_snellEnvelope [SigmaFiniteFiltration P ℱ] (E : rw [mem_singleton_iff.1 hQ, setLIntegral_snellEnvelope (ℱ.mono n.le_succ s hs), setLIntegral_snellEnvelope hs] -- The stopping times after `n + 1` are among those after `n`. - exact iSup₂_le fun τ hτ ↦ iSup₂_le fun hnτ hτN ↦ le_iSup₂_of_le τ hτ <| - le_iSup₂_of_le (fun ω ↦ n.le_succ.trans (hnτ ω)) hτN le_rfl + exact biSup_mono fun _ hτ ↦ boundedStoppingTimesFrom_anti ℱ n.le_succ hτ -/-- **Minimality of the Snell envelope.** The Snell envelope is almost everywhere below every -`ℝ≥0∞`-valued supermartingale that dominates the process almost everywhere at every time. -/ +/-- **Minimality of the Snell envelope.** The Snell envelope for `P ∈ S` is almost everywhere +below every `ℝ≥0∞`-valued supermartingale for `S` that dominates the process almost everywhere +under `P` at every time. -/ theorem IsENNSupermartingale.snellEnvelope_ae_le [SigmaFiniteFiltration P ℱ] - (hM : IsENNSupermartingale M ℱ {P}) (hEM : ∀ n, E n ≤ᵐ[P] M n) (n : ℕ) : + (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) (hEM : ∀ n, E n ≤ᵐ[P] M n) (n : ℕ) : snellEnvelope E ℱ P n ≤ᵐ[P] M n := by - refine ProbabilityTheory.snellEnvelope_ae_le fun τ hτ hnτ ⟨N, hτN⟩ ↦ ?_ + refine ProbabilityTheory.snellEnvelope_ae_le fun τ ⟨hτ, hnτ, N, hτN⟩ ↦ ?_ rw [condLExp_ae_le_iff_forall_setLIntegral_le (ℱ.le n) (hM.adapted n)] intro s hs have hEM' : ∀ᵐ ω ∂P, ∀ k, E k ω ≤ M k ω := ae_all_iff.2 hEM @@ -218,7 +249,7 @@ theorem IsENNSupermartingale.snellEnvelope_ae_le [SigmaFiniteFiltration P ℱ] lintegral_mono_ae (ae_restrict_of_ae (hEM'.mono fun ω hω ↦ hω (τ ω))) _ ≤ ∫⁻ ω in s, M n ω ∂P := by -- Optional stopping between the constant time `n` and `τ`. - have h := hM.setLIntegral_stoppedValueLimsup_le_of_le_const (mem_singleton P) + have h := hM.setLIntegral_stoppedValueLimsup_le_of_le_const hP (isStoppingTime_natCast n) hτ (fun ω ↦ by exact_mod_cast hnτ ω) (N := N) (fun ω ↦ by exact_mod_cast hτN ω) (s := s) ((isStoppingTime_natCast n).le_measurableSpace_of_const_le @@ -228,36 +259,32 @@ theorem IsENNSupermartingale.snellEnvelope_ae_le [SigmaFiniteFiltration P ℱ] /-- The Snell envelope of a process whose expectations at the bounded stopping times are at most `1` under `P` is a test supermartingale for `P`. -/ theorem isTestSupermartingale_snellEnvelope [SigmaFiniteFiltration P ℱ] - (hE : ∀ τ : Ω → ℕ, (IsStoppingTime ℱ fun ω ↦ (τ ω : WithTop ℕ)) → - (∃ N : ℕ, ∀ ω, τ ω ≤ N) → ∫⁻ ω, E (τ ω) ω ∂P ≤ 1) : + (hE : ∀ τ ∈ boundedStoppingTimesFrom ℱ 0, ∫⁻ ω, E (τ ω) ω ∂P ≤ 1) : IsTestSupermartingale (snellEnvelope E ℱ P) ℱ {P} := ⟨isENNSupermartingale_snellEnvelope E, fun Q hQ ↦ by rw [mem_singleton_iff.1 hQ, lintegral_snellEnvelope_zero] - exact iSup₂_le fun τ hτ ↦ iSup_le (hE τ hτ)⟩ + exact iSup₂_le hE⟩ /-- For a process of measurable functions with finite expectations, the Snell envelope agrees -almost everywhere with the essential supremum, over the bounded stopping times `τ ≥ n`, of the -conditional expectations `P[(E τ).toReal|ℱ n]` of the real values of the process at `τ`, the +almost everywhere with the essential supremum, over the bounded stopping times `τ` after `n`, of +the conditional expectations `P[(E τ).toReal|ℱ n]` of the real values of the process at `τ`, the form in which it is classically defined. -/ theorem snellEnvelope_ae_eq_essSupFamily_condExp [SigmaFiniteFiltration P ℱ] (hE : ∀ n, Measurable (E n)) (hE_int : ∀ n, ∫⁻ ω, E n ω ∂P ≠ ∞) (n : ℕ) : snellEnvelope E ℱ P n =ᵐ[P] - essSupFamily (fun τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ - (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N} ↦ - fun ω ↦ ENNReal.ofReal (P[fun ω ↦ (E (τ.1 ω) ω).toReal|ℱ n] ω)) P := by + essSupFamily (fun τ : boundedStoppingTimesFrom ℱ n ↦ + fun ω ↦ ENNReal.ofReal (P[fun ω ↦ (E (τ.1 ω) ω).toReal|ℱ n] ω)) P := by have := SigmaFinite.of_trim (μ := P) (ℱ.le n) - have h (τ : {τ : Ω → ℕ // IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)) ∧ - (∀ ω, n ≤ τ ω) ∧ ∃ N : ℕ, ∀ ω, τ ω ≤ N}) : + have h (τ : boundedStoppingTimesFrom ℱ n) : P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n] =ᵐ[P] fun ω ↦ ENNReal.ofReal (P[fun ω ↦ (E (τ.1 ω) ω).toReal|ℱ n] ω) := by obtain ⟨τ, hτ, -, N, hτN⟩ := τ have hmeas : Measurable fun ω ↦ E (τ ω) ω := by simpa using measurable_stoppedValueLimsup hE hτ.measurable' -- The value at `τ ≤ N` is below the sum of the values at the times up to `N`. - have hle : ∫⁻ ω, E (τ ω) ω ∂P ≤ ∑ k ∈ Finset.range (N + 1), ∫⁻ ω, E k ω ∂P := by - rw [← lintegral_finsetSum (Finset.range (N + 1)) fun k _ ↦ hE k] - exact lintegral_mono fun ω ↦ Finset.single_le_sum (f := fun k ↦ E k ω) - (fun _ _ ↦ zero_le) (Finset.mem_range.2 (Nat.lt_succ_of_le (hτN ω))) + have hle := lintegral_stoppedValueLimsup_le_sum (μ := P) (fun k ↦ (hE k).aemeasurable) + (τ := fun ω ↦ (τ ω : WithTop ℕ)) (N := N) fun ω ↦ by exact_mod_cast hτN ω + rw [stoppedValueLimsup_natCast] at hle have hint : ∫⁻ ω, E (τ ω) ω ∂P ≠ ∞ := ne_top_of_le_ne_top (ENNReal.sum_ne_top.2 fun k _ ↦ hE_int k) hle filter_upwards [toReal_condLExp (ℱ n) hmeas.aemeasurable hint, diff --git a/LMLExplore/Probability/Process/StoppedValue.lean b/LMLExplore/Probability/Process/StoppedValue.lean index 7b312371..755e47db 100644 --- a/LMLExplore/Probability/Process/StoppedValue.lean +++ b/LMLExplore/Probability/Process/StoppedValue.lean @@ -6,6 +6,7 @@ Authors: LMLExplore contributors module public import Mathlib.MeasureTheory.Constructions.BorelSpace.Order +public import Mathlib.MeasureTheory.Integral.Lebesgue.Add public import Mathlib.Probability.Process.Stopping /-! @@ -35,6 +36,8 @@ optional stopping holds at every stopping time with this convention. * `MeasureTheory.tendsto_stoppedValueLimsup_min`: for a convergent process, the values at the truncated times `min τ N` converge to the value at `τ`. * `MeasureTheory.measurable_stoppedValueLimsup`: it is measurable for measurable `u n` and `τ`. +* `MeasureTheory.lintegral_stoppedValueLimsup_le_sum`: at a random time bounded by `N`, the + integral of an `ℝ≥0∞`-valued process is at most the sum of its integrals at the times up to `N`. ## References @@ -136,4 +139,22 @@ theorem measurable_stoppedValueLimsup [ConditionallyCompleteLinearOrder β] [Top | coe n => simpa using hu n exact h.comp (measurable_id.prodMk hτ) +open scoped ENNReal in +/-- The integral of the value of an `ℝ≥0∞`-valued process at a random time bounded by `N` is at +most the sum of the integrals of the process at the times up to `N`. -/ +theorem lintegral_stoppedValueLimsup_le_sum {mΩ : MeasurableSpace Ω} {μ : Measure Ω} + {u : ℕ → Ω → ℝ≥0∞} (hu : ∀ n, AEMeasurable (u n) μ) {N : ℕ} (hτN : ∀ ω, τ ω ≤ N) : + ∫⁻ ω, stoppedValueLimsup u τ ω ∂μ ≤ ∑ k ∈ Finset.range (N + 1), ∫⁻ ω, u k ω ∂μ := by + rw [← lintegral_finsetSum' (Finset.range (N + 1)) fun k _ ↦ hu k] + refine lintegral_mono fun ω ↦ ?_ + have h := hτN ω + induction hτω : τ ω using WithTop.recTopCoe with + | top => simp [hτω] at h + | coe k => + rw [← Nat.cast_withTop] at hτω + rw [hτω, Nat.cast_le] at h + rw [stoppedValueLimsup_of_eq_natCast hτω] + exact Finset.single_le_sum (f := fun k ↦ u k ω) (fun _ _ ↦ zero_le) + (Finset.mem_range.2 (Nat.lt_succ_of_le h)) + end MeasureTheory From 00bb14fb1da070aa415445a2a0ffd9311e115549 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:12:44 +0100 Subject: [PATCH 3/3] doc: state the measurability hypothesis of the real condExp comparison Co-Authored-By: Claude Code --- LMLExplore/Probability/Martingale/SnellEnvelope.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LMLExplore/Probability/Martingale/SnellEnvelope.lean b/LMLExplore/Probability/Martingale/SnellEnvelope.lean index 9b338834..edd274ba 100644 --- a/LMLExplore/Probability/Martingale/SnellEnvelope.lean +++ b/LMLExplore/Probability/Martingale/SnellEnvelope.lean @@ -22,8 +22,8 @@ process, the smallest `ℝ≥0∞`-valued supermartingale that dominates it. The conditional expectations are Mathlib's conditional Lebesgue expectations `P⁻[X|m]` of `ℝ≥0∞`-valued functions, and the essential supremum is `MeasureTheory.essSupFamily`. Neither needs integrability, so the Snell envelope is defined and is a supermartingale for every process. When -the values of the process have finite expectations, it agrees almost surely with the essential -supremum of the conditional expectations `P[(E τ).toReal|ℱ n]` of the real values +the values of the process are measurable with finite expectations, it agrees almost surely with +the essential supremum of the conditional expectations `P[(E τ).toReal|ℱ n]` of the real values (`ProbabilityTheory.snellEnvelope_ae_eq_essSupFamily_condExp`). Its role in anytime-valid inference is the characterization of e-processes: an adapted process