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/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..edd274ba --- /dev/null +++ b/LMLExplore/Probability/Martingale/SnellEnvelope.lean @@ -0,0 +1,298 @@ +/- +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 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 +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.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 + +* `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 Ω} + {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 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 τ : 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 τ : boundedStoppingTimesFrom ℱ 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 `τ` after `n`. -/ +theorem condLExp_ae_le_snellEnvelope [SigmaFiniteFiltration P ℱ] + (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 τ : 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 `τ` after `n`. -/ +theorem snellEnvelope_ae_le + (hh : ∀ τ ∈ boundedStoppingTimesFrom ℱ n, P⁻[fun ω ↦ E (τ ω) ω | ℱ n] ≤ᵐ[P] h) : + snellEnvelope E ℱ P n ≤ᵐ[P] h := + 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 `τ` after `n`. -/ +theorem snellEnvelope_ae_le_iff [SigmaFiniteFiltration P ℱ] : + 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) + (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 `τ` 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 τ : boundedStoppingTimesFrom ℱ n ↦ P⁻[fun ω ↦ E (τ.1 ω) ω|ℱ n]) := by + classical + 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 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 τ₁ τ₂, piecewise_mem_boundedStoppingTimesFrom hA hτ₁ hτ₂⟩, ?_, ?_⟩ + · 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 `τ` after `n`. -/ +theorem setLIntegral_snellEnvelope [SigmaFiniteFiltration P ℱ] {s : Set Ω} + (hs : MeasurableSet[ℱ n] s) : + ∫⁻ ω in s, snellEnvelope E ℱ P n ω ∂P = + ⨆ τ ∈ 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, 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 = + ⨆ τ ∈ 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∞) : + 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 biSup_mono fun _ hτ ↦ boundedStoppingTimesFrom_anti ℱ n.le_succ hτ + +/-- **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 ℱ 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⟩ ↦ ?_ + 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 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 + (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 : ∀ τ ∈ 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 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 `τ` 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 τ : boundedStoppingTimesFrom ℱ n ↦ + fun ω ↦ ENNReal.ofReal (P[fun ω ↦ (E (τ.1 ω) ω).toReal|ℱ n] ω)) P := by + have := SigmaFinite.of_trim (μ := P) (ℱ.le 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 := 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, + 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 diff --git a/LMLExplore/Probability/Process/StoppedValue.lean b/LMLExplore/Probability/Process/StoppedValue.lean index 5791cd56..a6ecf1c4 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`. * `MeasureTheory.tendsto_lintegral_stoppedValueLimsup_min`: for an almost everywhere nondecreasing `ℝ≥0∞`-valued process, the integrals at the truncated times `min τ N` converge to the integral at `τ`. @@ -146,6 +149,23 @@ theorem measurable_stoppedValueLimsup [ConditionallyCompleteLinearOrder β] [Top | coe n => simpa using hu n exact h.comp (measurable_id.prodMk hτ) +/-- 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)) + /-- **Monotone convergence at truncated times.** For an almost everywhere nondecreasing process of measurable `ℝ≥0∞`-valued functions and a measurable random time `τ`, the integrals of its values at the truncated times `min τ N` increase to the integral of its value at `τ`. -/