diff --git a/LMLExplore/EValues/OptionalStopping.lean b/LMLExplore/EValues/OptionalStopping.lean new file mode 100644 index 00000000..eb40879b --- /dev/null +++ b/LMLExplore/EValues/OptionalStopping.lean @@ -0,0 +1,296 @@ +/- +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.EValues.TestSupermartingale +public import LMLExplore.Probability.Process.StoppedValueLimsup +public import LMLExplore.Probability.Process.Stopping +public import Mathlib.Probability.Martingale.Convergence + +/-! +# Convergence and optional stopping of supermartingales in `ℝ≥0∞` + +An `ℝ≥0∞`-valued supermartingale `M` with finite initial expectation under a finite measure +converges almost surely, and its limit `limsup M` is almost surely finite with +`∫⁻ limsup M ≤ ∫⁻ M 0` [RW, Fact 7.5]. This is what gives a meaning to the value of `M` at a +stopping time that may be infinite: +`ProbabilityTheory.stoppedValueLimsup M τ` is `M (τ ω) ω` where `τ ω` is finite and +`limsup (M · ω)` where `τ ω = ⊤` [RRLK; RLKR23, (1.2)] +(`LMLExplore/Probability/Process/StoppedValueLimsup.lean`). + +The optional stopping theorem then holds at arbitrary stopping times, with no condition beyond a +finite measure and finite initial expectation [RW, Fact 7.5; ShSVV11, Theorem 1]: for +stopping times `σ ≤ τ` and every `s` measurable for the σ-algebra of `σ`, +`∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P`. In particular +the value of a test supermartingale at any stopping time is an e-variable, which is what makes +test supermartingales valid under optional stopping and the starting point of e-processes. +Mathlib's `MeasureTheory.Submartingale.expected_stoppedValue_mono` is the case of bounded stopping +times for integrable real processes. + +## Main statements + +* `ProbabilityTheory.IsENNSupermartingale.ae_tendsto_limsup`: almost sure convergence. +* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_limsup_le`: the limit closes the + supermartingale, `∫⁻ ω in s, limsup M ω ≤ ∫⁻ ω in s, M n ω` for `ℱ n`-measurable `s`. +* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_stoppedProcess_le`: optional stopping for + stopped processes at a fixed time. +* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_stoppedValueLimsup_le`: optional stopping at + arbitrary stopping times `σ ≤ τ`. +* `ProbabilityTheory.IsTestSupermartingale.isEVar_stoppedValueLimsup`: the value of a test + supermartingale at any stopping time is an e-variable. + +## Implementation notes + +Stopped processes are first compared at a fixed time +(`ProbabilityTheory.IsENNSupermartingale.setLIntegral_stoppedProcess_le`), which needs no +integrability at all; Fatou's lemma passes to the limit where `σ` is bounded, and the events +`{σ ≤ k}` exhaust `{σ < ⊤}`. Almost sure convergence comes from Mathlib's martingale convergence +theorem `MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd`, applied to the real +supermartingale `(M n).toReal`. + +## References + +* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in + Statistics 1 (2025), arXiv:2410.23614. +* [ShSVV11] G. Shafer, A. Shen, N. Vereshchagin and V. Vovk, *Test martingales, Bayes factors and + p-values*, Statist. Sci. 26 (2011), arXiv:0912.4269. +* [RRLK] A. Ramdas, J. Ruf, M. Larsson and W. M. Koolen, *Admissible anytime-valid sequential + inference must rely on nonnegative martingales*, arXiv:2009.03167. +* [RLKR23] J. Ruf, M. Larsson, W. M. Koolen and A. Ramdas, *A composite generalization of Ville's + martingale theorem using e-processes*, Electron. J. Probab. 28 (2023), arXiv:2203.04485. +-/ + +public section + +open MeasureTheory Filter Set +open scoped ENNReal Topology + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {ℱ : Filtration ℕ mΩ} {S : Set (Measure Ω)} + {P : Measure Ω} {M : ℕ → Ω → ℝ≥0∞} {σ τ : Ω → WithTop ℕ} + +/-! ### Almost sure convergence -/ + +namespace IsENNSupermartingale + +/-- An `ℝ≥0∞`-valued supermartingale with finite initial expectation under a finite measure +converges almost surely, to its `limsup` [RW, Fact 7.5]. -/ +theorem ae_tendsto_limsup (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] + (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) : + ∀ᵐ ω ∂P, Tendsto (fun n ↦ M n ω) atTop (𝓝 (limsup (fun n ↦ M n ω) atTop)) := by + have hbdd : ⨆ n, eLpNorm ((-fun n ω ↦ (M n ω).toReal) n) 1 P < ∞ := by + refine (iSup_le fun n ↦ ?_).trans_lt h0.lt_top + rw [eLpNorm_one_eq_lintegral_eNorm] + · refine (lintegral_mono fun ω ↦ ?_).trans (hM.lintegral_le hP n.zero_le) + rw [Pi.neg_apply, Pi.neg_apply, eNorm_neg, Real.eNorm_of_nonneg ENNReal.toReal_nonneg] + exact ENNReal.ofReal_toReal_le + · exact (hM.measurable n).ennreal_toReal.neg.aestronglyMeasurable + filter_upwards [(hM.supermartingale_toReal hP h0).neg.exists_ae_tendsto_of_bdd hbdd, + hM.ae_lt_top hP h0] with ω ⟨c, hc⟩ hfin + have hlim : Tendsto (fun n ↦ M n ω) atTop (𝓝 (ENNReal.ofReal (-c))) := by + refine ((ENNReal.continuous_ofReal.tendsto _).comp hc.neg).congr fun n ↦ ?_ + simp [ENNReal.ofReal_toReal (hfin n).ne] + rwa [hlim.limsup_eq] + +/-! ### Optional stopping -/ + +/-- In `WithTop ℕ`, a value strictly above `n` is at least `n + 1`. -/ +private lemma coe_add_one_le_of_coe_lt {n : ℕ} {x : WithTop ℕ} (h : (n : WithTop ℕ) < x) : + ((n + 1 : ℕ) : WithTop ℕ) ≤ x := by + cases x with + | top => exact le_top + | coe x => exact WithTop.coe_le_coe.2 (Nat.succ_le_of_lt (WithTop.coe_lt_coe.1 h)) + +/-- One step of the stopped process: its set integrals over `ℱ n`-measurable sets do not increase +from time `n` to time `n + 1`. -/ +private lemma setLIntegral_stoppedProcess_succ_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + (hτ : IsStoppingTime ℱ τ) (n : ℕ) {t : Set Ω} (ht : MeasurableSet[ℱ n] t) : + ∫⁻ ω in t, MeasureTheory.stoppedProcess M τ (n + 1) ω ∂P ≤ + ∫⁻ ω in t, MeasureTheory.stoppedProcess M τ n ω ∂P := by + have hC := hτ.measurableSet_gt n + have htC := ℱ.le n _ (ht.inter hC) + rw [← lintegral_inter_add_sdiff _ t (ℱ.le n _ hC), + ← lintegral_inter_add_sdiff (fun ω ↦ MeasureTheory.stoppedProcess M τ n ω) t (ℱ.le n _ hC)] + refine add_le_add ?_ (setLIntegral_congr_fun (ℱ.le n _ (ht.diff hC)) fun ω hω ↦ ?_).le + · rw [setLIntegral_congr_fun htC fun ω hω ↦ stoppedProcess_eq_of_le (i := n + 1) + (coe_add_one_le_of_coe_lt hω.2), + setLIntegral_congr_fun htC fun ω hω ↦ stoppedProcess_eq_of_le (i := n) hω.2.le] + exact hM.setLIntegral_succ_le P hP n _ (ht.inter hC) + · have hτn : τ ω ≤ n := not_lt.1 hω.2 + rw [stoppedProcess_eq_of_ge (i := n) hτn, + stoppedProcess_eq_of_ge (i := n + 1) (hτn.trans (WithTop.coe_le_coe.2 n.le_succ))] + +/-- **Optional stopping for stopped processes.** For stopping times `σ ≤ τ` and every set `s` +measurable for the σ-algebra of `σ`, the set integral over `s` of the process stopped at `τ` is +at most that of the process stopped at `σ`, at every time. No integrability is needed. -/ +theorem setLIntegral_stoppedProcess_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + (hσ : IsStoppingTime ℱ σ) (hτ : IsStoppingTime ℱ τ) (hστ : σ ≤ τ) (n : ℕ) {s : Set Ω} + (hs : MeasurableSet[hσ.measurableSpace] s) : + ∫⁻ ω in s, MeasureTheory.stoppedProcess M τ n ω ∂P ≤ + ∫⁻ ω in s, MeasureTheory.stoppedProcess M σ n ω ∂P := by + induction n generalizing s with + | zero => + refine (setLIntegral_congr_fun (hσ.measurableSpace_le s hs) fun ω _ ↦ ?_).le + rw [stoppedProcess_eq_of_le (i := 0) bot_le, stoppedProcess_eq_of_le (i := 0) bot_le] + | succ n ih => + have hsm := hσ.measurableSpace_le s hs + have hB := ℱ.le n _ (hσ.measurableSet_le n) + rw [← lintegral_inter_add_sdiff _ s hB, + ← lintegral_inter_add_sdiff (fun ω ↦ MeasureTheory.stoppedProcess M σ (n + 1) ω) s hB] + refine add_le_add ?_ (setLIntegral_congr_fun (hsm.diff hB) fun ω hω ↦ ?_).le + · calc ∫⁻ ω in s ∩ {ω | σ ω ≤ n}, MeasureTheory.stoppedProcess M τ (n + 1) ω ∂P + ≤ ∫⁻ ω in s ∩ {ω | σ ω ≤ n}, MeasureTheory.stoppedProcess M τ n ω ∂P := + setLIntegral_stoppedProcess_succ_le hM hP hτ n (((hσ.measurableSet s).1 hs).2 n) + _ ≤ ∫⁻ ω in s ∩ {ω | σ ω ≤ n}, MeasureTheory.stoppedProcess M σ n ω ∂P := + ih (hs.inter (hσ.measurableSet_le' n)) + _ = ∫⁻ ω in s ∩ {ω | σ ω ≤ n}, MeasureTheory.stoppedProcess M σ (n + 1) ω ∂P := + setLIntegral_congr_fun (hsm.inter hB) fun ω hω ↦ by + rw [stoppedProcess_eq_of_ge (i := n) hω.2, stoppedProcess_eq_of_ge (i := n + 1) + (hω.2.trans (WithTop.coe_le_coe.2 n.le_succ))] + · have hσn : ¬σ ω ≤ WithTop.some n := hω.2 + have hσn' : WithTop.some (n + 1) ≤ σ ω := coe_add_one_le_of_coe_lt (not_le.1 hσn) + rw [stoppedProcess_eq_of_le (i := n + 1) (hσn'.trans (hστ ω)), + stoppedProcess_eq_of_le (i := n + 1) hσn'] + +/-- Optional stopping where the smaller stopping time is bounded. -/ +private lemma setLIntegral_stoppedValueLimsup_le_of_le_const (hM : IsENNSupermartingale M ℱ S) + (hP : P ∈ S) [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (hσ : IsStoppingTime ℱ σ) + (hτ : IsStoppingTime ℱ τ) (hστ : σ ≤ τ) {N : ℕ} (hσN : ∀ ω, σ ω ≤ N) {s : Set Ω} + (hs : MeasurableSet[hσ.measurableSpace] s) : + ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P := by + have hlim : ∀ᵐ ω ∂P, Tendsto (fun n ↦ MeasureTheory.stoppedProcess M τ n ω) atTop + (𝓝 (stoppedValueLimsup M τ ω)) := by + filter_upwards [hM.ae_tendsto_limsup hP h0] with ω hω + exact tendsto_stoppedProcess_stoppedValueLimsup fun _ ↦ hω + have hmeas (n : ℕ) : Measurable (MeasureTheory.stoppedProcess M τ n) := by + rw [stoppedProcess_eq_stoppedValue] + exact measurable_stoppedValue_of_countable hM.measurable + (measurable_const.min hτ.measurable') + calc ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P + = ∫⁻ ω in s, liminf (fun n ↦ MeasureTheory.stoppedProcess M τ n ω) atTop ∂P := + lintegral_congr_ae (ae_restrict_of_ae (hlim.mono fun ω hω ↦ hω.liminf_eq.symm)) + _ ≤ liminf (fun n ↦ ∫⁻ ω in s, MeasureTheory.stoppedProcess M τ n ω ∂P) atTop := + lintegral_liminf_le' fun n ↦ (hmeas n).aemeasurable + _ ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P := by + refine liminf_le_of_frequently_le' (Eventually.frequently ?_) + filter_upwards [eventually_ge_atTop N] with n hn + refine (hM.setLIntegral_stoppedProcess_le hP hσ hτ hστ n hs).trans_eq ?_ + exact setLIntegral_congr_fun (hσ.measurableSpace_le s hs) fun ω _ ↦ + stoppedProcess_eq_stoppedValueLimsup ((hσN ω).trans (WithTop.coe_le_coe.2 hn)) + +/-- **Optional stopping at arbitrary stopping times** [RW, Fact 7.5; ShSVV11, Theorem 1]. For an +`ℝ≥0∞`-valued supermartingale with finite initial expectation under a finite measure, stopping +times `σ ≤ τ` with values in `WithTop ℕ` and every set `s` measurable for the σ-algebra of `σ`, +`∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P`. -/ +theorem setLIntegral_stoppedValueLimsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (hσ : IsStoppingTime ℱ σ) + (hτ : IsStoppingTime ℱ τ) (hστ : σ ≤ τ) {s : Set Ω} + (hs : MeasurableSet[hσ.measurableSpace] s) : + ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P := by + have hsm := hσ.measurableSpace_le s hs + have hT : MeasurableSet {ω | σ ω = ⊤} := hσ.measurable' (measurableSet_singleton ⊤) + rw [← lintegral_inter_add_sdiff _ s hT, ← lintegral_inter_add_sdiff (stoppedValueLimsup M σ) s hT] + refine add_le_add (setLIntegral_congr_fun (hsm.inter hT) fun ω hω ↦ ?_).le ?_ + · -- where `σ` is infinite, so is `τ` + rw [stoppedValueLimsup_of_eq_top (top_unique (hω.2 ▸ hστ ω)), stoppedValueLimsup_of_eq_top hω.2] + -- exhaust `{σ < ⊤}` by the events `{σ ≤ k}`, on which `σ` is the bounded time `min σ k` + have hU : s \ {ω | σ ω = ⊤} = ⋃ k : ℕ, s ∩ {ω | σ ω ≤ k} := by + ext ω + simp only [Set.mem_sdiff, mem_ofPred_eq, mem_iUnion, mem_inter_iff] + refine ⟨fun ⟨hs, hne⟩ ↦ ?_, fun ⟨k, hs, hk⟩ ↦ ⟨hs, ne_top_of_le_ne_top WithTop.coe_ne_top hk⟩⟩ + obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 hne + exact ⟨k, hs, hk ▸ le_rfl⟩ + have hdir : Directed (· ⊆ ·) fun k : ℕ ↦ s ∩ {ω | σ ω ≤ k} := + Monotone.directed_le fun i j hij ω hω ↦ ⟨hω.1, hω.2.trans (WithTop.coe_le_coe.2 hij)⟩ + rw [hU, setLIntegral_iUnion_of_directed _ hdir, setLIntegral_iUnion_of_directed _ hdir] + refine iSup_mono fun k ↦ ?_ + have hk : MeasurableSet[(hσ.min_const k).measurableSpace] (s ∩ {ω | σ ω ≤ k}) := + (hσ.measurableSet_inter_le_const_iff s k).1 (hs.inter (hσ.measurableSet_le' k)) + calc ∫⁻ ω in s ∩ {ω | σ ω ≤ k}, stoppedValueLimsup M τ ω ∂P + ≤ ∫⁻ ω in s ∩ {ω | σ ω ≤ k}, stoppedValueLimsup M (fun ω ↦ min (σ ω) k) ω ∂P := + setLIntegral_stoppedValueLimsup_le_of_le_const hM hP h0 (hσ.min_const k) hτ + (fun ω ↦ (min_le_left _ _).trans (hστ ω)) (fun ω ↦ min_le_right _ _) hk + _ = ∫⁻ ω in s ∩ {ω | σ ω ≤ k}, stoppedValueLimsup M σ ω ∂P := + setLIntegral_congr_fun (hsm.inter (ℱ.le k _ (hσ.measurableSet_le k))) fun ω hω ↦ + stoppedValueLimsup_congr (min_eq_left hω.2) + +/-- Optional stopping from time `0`: `∫⁻ stoppedValueLimsup M τ ≤ ∫⁻ M 0` at every stopping +time. -/ +theorem lintegral_stoppedValueLimsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (hτ : IsStoppingTime ℱ τ) : + ∫⁻ ω, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω, M 0 ω ∂P := by + have := hM.setLIntegral_stoppedValueLimsup_le hP h0 (isStoppingTime_const ℱ 0) hτ + (fun ω ↦ bot_le) MeasurableSet.univ + rwa [stoppedValueLimsup_const, Measure.restrict_univ] at this + +/-- The almost sure limit closes the supermartingale: for every `ℱ n`-measurable `s`, +`∫⁻ ω in s, limsup M ω ≤ ∫⁻ ω in s, M n ω`. -/ +theorem setLIntegral_limsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {n : ℕ} {s : Set Ω} + (hs : MeasurableSet[ℱ n] s) : + ∫⁻ ω in s, limsup (fun k ↦ M k ω) atTop ∂P ≤ ∫⁻ ω in s, M n ω ∂P := by + have hs' : MeasurableSet[(isStoppingTime_const ℱ n).measurableSpace] s := by + rwa [IsStoppingTime.measurableSpace_const] + have := hM.setLIntegral_stoppedValueLimsup_le hP h0 (isStoppingTime_const ℱ n) + (isStoppingTime_top ℱ) (fun _ ↦ le_top) hs' + rwa [stoppedValueLimsup_const, stoppedValueLimsup_top] at this + +/-- The almost sure limit has expectation at most `∫⁻ M 0`. -/ +theorem lintegral_limsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] + (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) : + ∫⁻ ω, limsup (fun n ↦ M n ω) atTop ∂P ≤ ∫⁻ ω, M 0 ω ∂P := by + simpa using hM.setLIntegral_limsup_le hP h0 (n := 0) MeasurableSet.univ + +/-- The almost sure limit is almost surely finite. -/ +theorem ae_limsup_lt_top (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] + (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) : ∀ᵐ ω ∂P, limsup (fun n ↦ M n ω) atTop < ∞ := + MeasureTheory.ae_lt_top (Measurable.limsup hM.measurable) + ((hM.lintegral_limsup_le hP h0).trans_lt h0.lt_top).ne + +end IsENNSupermartingale + +/-! ### Test supermartingales -/ + +namespace IsTestSupermartingale + +variable (hM : IsTestSupermartingale M ℱ S) +include hM + +/-- A test supermartingale converges almost surely, under every finite member of the null. -/ +theorem ae_tendsto_limsup (hP : P ∈ S) [IsFiniteMeasure P] : + ∀ᵐ ω ∂P, Tendsto (fun n ↦ M n ω) atTop (𝓝 (limsup (fun n ↦ M n ω) atTop)) := + hM.toIsENNSupermartingale.ae_tendsto_limsup hP (hM.lintegral_zero_ne_top hP) + +/-- The almost sure limit of a test supermartingale is almost surely finite. -/ +theorem ae_limsup_lt_top (hP : P ∈ S) [IsFiniteMeasure P] : + ∀ᵐ ω ∂P, limsup (fun n ↦ M n ω) atTop < ∞ := + hM.toIsENNSupermartingale.ae_limsup_lt_top hP (hM.lintegral_zero_ne_top hP) + +/-- Optional stopping for test supermartingales at arbitrary stopping times `σ ≤ τ`. -/ +theorem setLIntegral_stoppedValueLimsup_le (hP : P ∈ S) [IsFiniteMeasure P] + (hσ : IsStoppingTime ℱ σ) (hτ : IsStoppingTime ℱ τ) (hστ : σ ≤ τ) {s : Set Ω} + (hs : MeasurableSet[hσ.measurableSpace] s) : + ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P := + hM.toIsENNSupermartingale.setLIntegral_stoppedValueLimsup_le hP (hM.lintegral_zero_ne_top hP) + hσ hτ hστ hs + +/-- The value of a test supermartingale at any stopping time has expectation at most `1`. -/ +theorem lintegral_stoppedValueLimsup_le_one (hP : P ∈ S) [IsFiniteMeasure P] + (hτ : IsStoppingTime ℱ τ) : ∫⁻ ω, stoppedValueLimsup M τ ω ∂P ≤ 1 := + (hM.toIsENNSupermartingale.lintegral_stoppedValueLimsup_le hP (hM.lintegral_zero_ne_top hP) + hτ).trans (hM.lintegral_zero_le P hP) + +/-- The value of a test supermartingale at any stopping time, with values in `WithTop ℕ`, is an +e-variable for a null of probability measures. -/ +theorem isEVar_stoppedValueLimsup (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hτ : IsStoppingTime ℱ τ) : IsEVar (stoppedValueLimsup M τ) S := + IsEVar.of_lintegral_le_one hS (measurable_stoppedValueLimsup hM.measurable hτ.measurable') + fun P hP ↦ have := hS P hP; hM.lintegral_stoppedValueLimsup_le_one hP hτ + +end IsTestSupermartingale + +end ProbabilityTheory diff --git a/LMLExplore/EValues/TestSupermartingale.lean b/LMLExplore/EValues/TestSupermartingale.lean index 91b25dfa..2d372fe0 100644 --- a/LMLExplore/EValues/TestSupermartingale.lean +++ b/LMLExplore/EValues/TestSupermartingale.lean @@ -189,6 +189,11 @@ theorem lintegral_le_one (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) (n ∫⁻ ω, M n ω ∂P ≤ 1 := (hM.lintegral_le hP n.zero_le).trans (hM.lintegral_zero_le P hP) +/-- The initial expectation of a test supermartingale is finite. -/ +theorem lintegral_zero_ne_top (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) : + ∫⁻ ω, M 0 ω ∂P ≠ ∞ := + ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne + /-- Every value of a test supermartingale for a null of probability measures is an e-variable. -/ theorem isEVar (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hM : IsTestSupermartingale M ℱ S) @@ -198,15 +203,13 @@ theorem isEVar (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hM : IsTestSupermarti /-- A test supermartingale is almost surely finite at every time. -/ theorem ae_lt_top (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) : ∀ᵐ ω ∂P, ∀ n, M n ω < ∞ := - hM.toIsENNSupermartingale.ae_lt_top hP - ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne + hM.toIsENNSupermartingale.ae_lt_top hP (hM.lintegral_zero_ne_top hP) /-- The real values of a test supermartingale form a real supermartingale under every finite member of the null. -/ theorem supermartingale_toReal (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] : Supermartingale (fun n ω ↦ (M n ω).toReal) ℱ P := - hM.toIsENNSupermartingale.supermartingale_toReal hP - ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne + hM.toIsENNSupermartingale.supermartingale_toReal hP (hM.lintegral_zero_ne_top hP) end IsTestSupermartingale @@ -440,7 +443,6 @@ successive ratios `M (k + 1) / M k`, with `0 / 0 = 0`, which are conditional e-v theorem IsTestSupermartingale.ae_eq_mul_prod_div (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) : ∀ᵐ ω ∂P, ∀ n, M n ω = M 0 ω * ∏ k ∈ range n, M (k + 1) ω / M k ω := - hM.toIsENNSupermartingale.ae_eq_mul_prod_div hP - ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne + hM.toIsENNSupermartingale.ae_eq_mul_prod_div hP (hM.lintegral_zero_ne_top hP) end ProbabilityTheory diff --git a/LMLExplore/Probability/Process/StoppedValueLimsup.lean b/LMLExplore/Probability/Process/StoppedValueLimsup.lean new file mode 100644 index 00000000..e4bbea32 --- /dev/null +++ b/LMLExplore/Probability/Process/StoppedValueLimsup.lean @@ -0,0 +1,129 @@ +/- +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.Probability.Process.Stopping +public import TauCeti.Probability.Process.StoppedValue + +/-! +# The value of a process at a possibly infinite time + +The value of a process `M : ι → Ω → ℝ≥0∞` at a time `τ : Ω → WithTop ι` that may be infinite is +given a meaning by taking the `limsup` of `M` where `τ = ⊤` [RRLK; RLKR23, (1.2)]. This is the +limit of the stopped process wherever `M` converges, which is the case almost surely for +`ℝ≥0∞`-valued supermartingales with finite initial expectation under a finite measure. + +## Main definitions + +* `ProbabilityTheory.stoppedValueLimsup M τ`: the value of `M` at a time `τ : Ω → WithTop ι`, + with `limsup` at infinity. + +## Main statements + +* `ProbabilityTheory.tendsto_stoppedProcess_stoppedValueLimsup`: the stopped process converges to + `stoppedValueLimsup M τ` wherever `τ` is finite and wherever `M` converges. +* `ProbabilityTheory.limsup_stoppedProcess`: `stoppedValueLimsup M τ` is the `limsup` of the + stopped process. +* `ProbabilityTheory.measurable_stoppedValueLimsup`: measurability at a measurable time. + +## References + +* [RRLK] A. Ramdas, J. Ruf, M. Larsson and W. M. Koolen, *Admissible anytime-valid sequential + inference must rely on nonnegative martingales*, arXiv:2009.03167. +* [RLKR23] J. Ruf, M. Larsson, W. M. Koolen and A. Ramdas, *A composite generalization of Ville's + martingale theorem using e-processes*, Electron. J. Probab. 28 (2023), arXiv:2203.04485. +-/ + +public section + +open MeasureTheory Filter +open scoped ENNReal Topology + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} + +section StoppedValueLimsup + +variable {ι : Type*} [Nonempty ι] [LinearOrder ι] {M : ι → Ω → ℝ≥0∞} {τ : Ω → WithTop ι} + {ω : Ω} + +/-- The value of a process `M : ι → Ω → ℝ≥0∞` at a time `τ : Ω → WithTop ι`: `M (τ ω) ω` where +`τ ω` is finite and `limsup (M · ω)` where `τ ω = ⊤` [RRLK; RLKR23, (1.2)]. Unlike Mathlib's +`MeasureTheory.stoppedValue`, whose value at `⊤` is arbitrary, it is the limit of the stopped +process wherever `M` converges (`ProbabilityTheory.tendsto_stoppedProcess_stoppedValueLimsup`). -/ +noncomputable def stoppedValueLimsup (M : ι → Ω → ℝ≥0∞) (τ : Ω → WithTop ι) (ω : Ω) : ℝ≥0∞ := + if τ ω = ⊤ then limsup (fun n ↦ M n ω) atTop else stoppedValue M τ ω + +theorem stoppedValueLimsup_of_eq_top (h : τ ω = ⊤) : + stoppedValueLimsup M τ ω = limsup (fun n ↦ M n ω) atTop := by + simp [stoppedValueLimsup, h] + +theorem stoppedValueLimsup_of_ne_top (h : τ ω ≠ ⊤) : + stoppedValueLimsup M τ ω = stoppedValue M τ ω := by + simp [stoppedValueLimsup, h] + +theorem stoppedValueLimsup_of_eq_coe {i : ι} (h : τ ω = i) : + stoppedValueLimsup M τ ω = M i ω := by + rw [stoppedValueLimsup_of_ne_top (h ▸ WithTop.coe_ne_top), stoppedValue_of_eq h] + +/-- `stoppedValueLimsup M τ ω` depends on `τ` only through `τ ω`. -/ +theorem stoppedValueLimsup_congr {σ : Ω → WithTop ι} (h : σ ω = τ ω) : + stoppedValueLimsup M σ ω = stoppedValueLimsup M τ ω := by + simp [stoppedValueLimsup, stoppedValue, h] + +/-- At a time with finite values, `stoppedValueLimsup` is the value of the process. -/ +@[simp] +theorem stoppedValueLimsup_coe (M : ι → Ω → ℝ≥0∞) (τ : Ω → ι) : + stoppedValueLimsup M (fun ω ↦ (τ ω : WithTop ι)) = fun ω ↦ M (τ ω) ω := + funext fun _ ↦ stoppedValueLimsup_of_eq_coe rfl + +/-- At a constant finite time, `stoppedValueLimsup` is the value of the process. -/ +theorem stoppedValueLimsup_const (M : ι → Ω → ℝ≥0∞) (i : ι) : + stoppedValueLimsup M (fun _ ↦ (i : WithTop ι)) = M i := + funext fun _ ↦ stoppedValueLimsup_of_eq_coe rfl + +/-- At the time `⊤`, `stoppedValueLimsup` is the `limsup` of the process. -/ +@[simp] +theorem stoppedValueLimsup_top (M : ι → Ω → ℝ≥0∞) : + stoppedValueLimsup M (fun _ ↦ ⊤) = fun ω ↦ limsup (fun n ↦ M n ω) atTop := + funext fun _ ↦ stoppedValueLimsup_of_eq_top rfl + +/-- The stopped process at a time after `τ ω` is `stoppedValueLimsup M τ ω`. -/ +theorem stoppedProcess_eq_stoppedValueLimsup {i : ι} (h : τ ω ≤ i) : + stoppedProcess M τ i ω = stoppedValueLimsup M τ ω := by + rw [stoppedProcess_eq_of_ge h, stoppedValueLimsup_of_ne_top (ne_top_of_le_ne_top + WithTop.coe_ne_top h), stoppedValue] + +/-- The stopped process converges to `stoppedValueLimsup M τ` wherever `τ` is finite, and wherever +`M` converges. -/ +theorem tendsto_stoppedProcess_stoppedValueLimsup + (hM : τ ω = ⊤ → Tendsto (fun n ↦ M n ω) atTop (𝓝 (limsup (fun n ↦ M n ω) atTop))) : + Tendsto (fun n ↦ stoppedProcess M τ n ω) atTop (𝓝 (stoppedValueLimsup M τ ω)) := by + cases h : τ ω with + | top => + simp_rw [stoppedValueLimsup_of_eq_top h, stoppedProcess_eq_of_le (h ▸ le_top)] + exact hM h + | coe k => + exact tendsto_atTop_of_eventually_const (i₀ := k) fun n hn ↦ + stoppedProcess_eq_stoppedValueLimsup (h ▸ WithTop.coe_le_coe.2 hn) + +/-- `stoppedValueLimsup M τ ω` is the `limsup` of the stopped process. -/ +theorem limsup_stoppedProcess (M : ι → Ω → ℝ≥0∞) (τ : Ω → WithTop ι) (ω : Ω) : + limsup (fun n ↦ stoppedProcess M τ n ω) atTop = stoppedValueLimsup M τ ω := by + cases h : τ ω with + | top => simp_rw [stoppedValueLimsup_of_eq_top h, stoppedProcess_eq_of_le (h ▸ le_top)] + | coe k => exact (tendsto_stoppedProcess_stoppedValueLimsup fun h' ↦ by simp [h] at h').limsup_eq + +end StoppedValueLimsup + +/-- The value of a measurable process at a measurable time is measurable. -/ +theorem measurable_stoppedValueLimsup {M : ℕ → Ω → ℝ≥0∞} {τ : Ω → WithTop ℕ} + (hM : ∀ n, Measurable (M n)) (hτ : Measurable τ) : Measurable (stoppedValueLimsup M τ) := + Measurable.ite (hτ (measurableSet_singleton ⊤)) (Measurable.limsup hM) + (measurable_stoppedValue_of_countable hM hτ) + +end ProbabilityTheory diff --git a/LMLExplore/Probability/Process/Stopping.lean b/LMLExplore/Probability/Process/Stopping.lean index a422b996..e3bc2477 100644 --- a/LMLExplore/Probability/Process/Stopping.lean +++ b/LMLExplore/Probability/Process/Stopping.lean @@ -9,7 +9,9 @@ public import Mathlib.MeasureTheory.MeasurableSpace.Instances public import Mathlib.Probability.Process.Stopping /-! -# Measurability of stopping times valued in `ℕ∞` +# Stopping times: the constant time `⊤` and measurability in `ℕ∞` + +The constant time `⊤ : WithTop ι` is a stopping time of every filtration indexed by `ι`. A stopping time of a filtration indexed by `ℕ` takes values in `WithTop ℕ`, which Mathlib equips with its Borel σ-algebra, and `IsStoppingTime.measurable'` is measurability for that σ-algebra. @@ -19,12 +21,22 @@ syntactically equal. This file states measurability of such a stopping time for ## Main statements +* `MeasureTheory.isStoppingTime_top`: the constant time `⊤` is a stopping time. * `MeasureTheory.IsStoppingTime.measurable_enat`: a stopping time `τ : Ω → ℕ∞` of a filtration indexed by `ℕ` is measurable for the discrete σ-algebra of `ℕ∞`. -/ public section +namespace MeasureTheory + +/-- The constant time `⊤` is a stopping time. -/ +theorem isStoppingTime_top {Ω ι : Type*} {m : MeasurableSpace Ω} [Preorder ι] + (f : Filtration ι m) : IsStoppingTime f fun _ : Ω ↦ (⊤ : WithTop ι) := + fun _ ↦ by simp + +end MeasureTheory + namespace MeasureTheory.IsStoppingTime variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {f : Filtration ℕ mΩ} {τ : Ω → ℕ∞}