From 1ee454f3f6466d7a7a7a88b8b9472fa1c9d03619 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 19:44:58 +0100 Subject: [PATCH 1/4] feat: stopped processes, minima, mixtures and optional continuation of test supermartingales Co-Authored-By: Claude Code --- LMLExplore/EValues/TestSupermartingale.lean | 241 ++++++++++++++++++++ LMLExplore/Probability/Process/Adapted.lean | 22 +- 2 files changed, 259 insertions(+), 4 deletions(-) diff --git a/LMLExplore/EValues/TestSupermartingale.lean b/LMLExplore/EValues/TestSupermartingale.lean index 91b25dfa..89b86b19 100644 --- a/LMLExplore/EValues/TestSupermartingale.lean +++ b/LMLExplore/EValues/TestSupermartingale.lean @@ -29,6 +29,13 @@ wealth process. It contains the products of sequential e-variables conditional e-variables with predictable weights [WSJ26], and betting `∏ k, (1 - c k + c k * E k)` with predictable bets `c k ≤ 1` [RW, Definition 7.21; WSR24]. +Test supermartingales are closed under the operations a statistician performs on running +evidence: stopping at a stopping time, taking the minimum of two of them, mixing a measurable +family over a probability measure (Tonelli in `ℝ≥0∞`, with no integrability hypothesis), and +optional continuation, in which the evidence `A τ` gathered up to a stopping time `τ` is +multiplied by a new process `B` that starts at `1` after `τ` [RW, Proposition 7.9]. These closure +properties transfer to e-processes through their domination by test supermartingales. + ## Main definitions * `ProbabilityTheory.IsENNSupermartingale M ℱ S`: `M : ℕ → Ω → ℝ≥0∞` is adapted and @@ -54,6 +61,13 @@ conditional e-variables with predictable weights [WSJ26], and betting `ProbabilityTheory.IsTestSupermartingale.ae_eq_mul_prod_div`: conversely, every test supermartingale is almost surely the wealth `M 0 * ∏ k < n, M (k + 1) / M k` of its successive ratios, which are conditional e-variables [WSR24, Proposition 3]. +* `ProbabilityTheory.IsTestSupermartingale.stoppedProcess_mul`, + `ProbabilityTheory.IsTestMartingale.stoppedProcess_mul`: optional continuation + [RW, Proposition 7.9]; `ProbabilityTheory.IsTestSupermartingale.stoppedProcess` and + `ProbabilityTheory.IsTestMartingale.stoppedProcess` are the case `B = 1` of stopped processes. +* `ProbabilityTheory.IsTestSupermartingale.inf`: the minimum of two test supermartingales. +* `ProbabilityTheory.isTestSupermartingale_lintegral`, + `ProbabilityTheory.isTestMartingale_lintegral`: mixtures over a probability measure. ## References @@ -443,4 +457,231 @@ theorem IsTestSupermartingale.ae_eq_mul_prod_div (hM : IsTestSupermartingale M hM.toIsENNSupermartingale.ae_eq_mul_prod_div hP ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne +/-! ### Pulling a known factor out of a supermartingale step -/ + +/-- A factor `Y` and a set `s` that are `ℱ n`-measurable can be pulled out of a step of an +`ℝ≥0∞`-valued supermartingale: `∫⁻ ω in s, Y ω * M (n + 1) ω ∂P ≤ ∫⁻ ω in s, Y ω * M n ω ∂P`. -/ +theorem IsENNSupermartingale.setLIntegral_mul_succ_le (hM : IsENNSupermartingale M ℱ S) + (hP : P ∈ S) {n : ℕ} {Y : Ω → ℝ≥0∞} (hY : Measurable[ℱ n] Y) {s : Set Ω} + (hs : MeasurableSet[ℱ n] s) : + ∫⁻ ω in s, Y ω * M (n + 1) ω ∂P ≤ ∫⁻ ω in s, Y ω * M n ω ∂P := by + rw [← lintegral_indicator (ℱ.le n s hs), ← lintegral_indicator (ℱ.le n s hs)] + simp_rw [indicator_mul_left] + exact lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le (ℱ.le n) + (hM.measurable (n + 1)).aemeasurable (hM.measurable n).aemeasurable + (hM.setLIntegral_succ_le P hP n) (hY.indicator hs) + +/-- A factor `Y` and a set `s` that are `ℱ n`-measurable can be pulled out of a step of a test +martingale: `∫⁻ ω in s, Y ω * M (n + 1) ω ∂P = ∫⁻ ω in s, Y ω * M n ω ∂P`. -/ +theorem IsTestMartingale.setLIntegral_mul_succ_eq (hM : IsTestMartingale M ℱ S) + (hP : P ∈ S) {n : ℕ} {Y : Ω → ℝ≥0∞} (hY : Measurable[ℱ n] Y) {s : Set Ω} + (hs : MeasurableSet[ℱ n] s) : + ∫⁻ ω in s, Y ω * M (n + 1) ω ∂P = ∫⁻ ω in s, Y ω * M n ω ∂P := by + rw [← lintegral_indicator (ℱ.le n s hs), ← lintegral_indicator (ℱ.le n s hs)] + simp_rw [indicator_mul_left] + exact lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq (ℱ.le n) + (hM.measurable (n + 1)).aemeasurable (hM.measurable n).aemeasurable + (hM.setLIntegral_succ_eq P hP n) (hY.indicator hs) + +/-! ### Minima -/ + +/-- The minimum of two `ℝ≥0∞`-valued supermartingales is a supermartingale. -/ +theorem IsENNSupermartingale.inf (hM : IsENNSupermartingale M ℱ S) + (hN : IsENNSupermartingale N ℱ S) : IsENNSupermartingale (M ⊓ N) ℱ S := by + refine ⟨fun n ↦ (hM.adapted n).min (hN.adapted n), fun P hP n s hs ↦ ?_⟩ + -- split `s` according to which of `M n` and `N n` is the minimum, an `ℱ n`-measurable event + have hT : MeasurableSet[ℱ n] {ω | M n ω ≤ N n ω} := + measurableSet_le (hM.adapted n) (hN.adapted n) + rw [← lintegral_inter_add_sdiff _ s (ℱ.le n _ hT), + ← lintegral_inter_add_sdiff _ s (ℱ.le n _ hT)] + gcongr ?_ + ?_ + · calc ∫⁻ ω in s ∩ {ω | M n ω ≤ N n ω}, (M ⊓ N) (n + 1) ω ∂P + ≤ ∫⁻ ω in s ∩ {ω | M n ω ≤ N n ω}, M (n + 1) ω ∂P := + lintegral_mono fun _ ↦ inf_le_left + _ ≤ ∫⁻ ω in s ∩ {ω | M n ω ≤ N n ω}, M n ω ∂P := + hM.setLIntegral_succ_le P hP n _ (hs.inter hT) + _ = ∫⁻ ω in s ∩ {ω | M n ω ≤ N n ω}, (M ⊓ N) n ω ∂P := + setLIntegral_congr_fun ((ℱ.le n _ hs).inter (ℱ.le n _ hT)) + fun _ hω ↦ (inf_eq_left.2 hω.2).symm + · calc ∫⁻ ω in s \ {ω | M n ω ≤ N n ω}, (M ⊓ N) (n + 1) ω ∂P + ≤ ∫⁻ ω in s \ {ω | M n ω ≤ N n ω}, N (n + 1) ω ∂P := + lintegral_mono fun _ ↦ inf_le_right + _ ≤ ∫⁻ ω in s \ {ω | M n ω ≤ N n ω}, N n ω ∂P := + hN.setLIntegral_succ_le P hP n _ (hs.diff hT) + _ = ∫⁻ ω in s \ {ω | M n ω ≤ N n ω}, (M ⊓ N) n ω ∂P := + setLIntegral_congr_fun ((ℱ.le n _ hs).diff (ℱ.le n _ hT)) + fun _ hω ↦ (inf_eq_right.2 (not_le.1 hω.2).le).symm + +/-- The minimum of a test supermartingale and an `ℝ≥0∞`-valued supermartingale, in particular of +two test supermartingales, is a test supermartingale. -/ +theorem IsTestSupermartingale.inf (hM : IsTestSupermartingale M ℱ S) + (hN : IsENNSupermartingale N ℱ S) : IsTestSupermartingale (M ⊓ N) ℱ S := + ⟨hM.toIsENNSupermartingale.inf hN, fun P hP ↦ + (lintegral_mono fun _ ↦ inf_le_left).trans (hM.lintegral_zero_le P hP)⟩ + +/-! ### Optional continuation and stopped processes -/ + +/-- The step of `stoppedProcess A τ * B` from time `n` to time `n + 1`, split at the +`ℱ n`-measurable event `{τ ≤ n}`: on it, `A` is already stopped; off it, `B` is still `1`. -/ +private lemma setLIntegral_stoppedProcess_mul_eq {A B : ℕ → Ω → ℝ≥0∞} {τ : Ω → WithTop ℕ} + (hτ : IsStoppingTime ℱ τ) (hB : ∀ (n : ℕ) ω, (n : WithTop ℕ) ≤ τ ω → B n ω = 1) {n j : ℕ} + (hnj : n ≤ j) (hjn : j ≤ n + 1) {s : Set Ω} (hs : MeasurableSet[ℱ n] s) : + ∫⁻ ω in s, (stoppedProcess A τ * B) j ω ∂P = + ∫⁻ ω in s ∩ {ω | τ ω ≤ n}, stoppedProcess A τ n ω * B j ω ∂P + + ∫⁻ ω in s \ {ω | τ ω ≤ n}, A j ω ∂P := by + have hT := ℱ.le n _ (hτ.measurableSet_le n) + rw [← lintegral_inter_add_sdiff _ s hT] + congr 1 + · refine setLIntegral_congr_fun ((ℱ.le n _ hs).inter hT) fun ω hω ↦ ?_ + have hτn : τ ω ≤ n := hω.2 + simp only [Pi.mul_apply] + rw [stoppedProcess_eq_of_ge (i := n) hτn, + stoppedProcess_eq_of_ge (i := j) (hτn.trans (WithTop.coe_le_coe.2 hnj))] + · refine setLIntegral_congr_fun ((ℱ.le n _ hs).diff hT) fun ω hω ↦ ?_ + have hjτ : (j : WithTop ℕ) ≤ τ ω := by + have hnτ : (n : WithTop ℕ) < τ ω := not_le.1 hω.2 + cases h : τ ω with + | top => exact le_top + | coe k => + rw [h] at hnτ + exact WithTop.coe_le_coe.2 (hjn.trans (WithTop.coe_lt_coe.1 hnτ)) + simp only [Pi.mul_apply] + rw [stoppedProcess_eq_of_le (i := j) hjτ, hB j ω hjτ, mul_one] + +/-- **Optional continuation of `ℝ≥0∞`-valued supermartingales** [RW, Proposition 7.9]. For +supermartingales `A` and `B` and a stopping time `τ` such that `B n = 1` whenever `n ≤ τ`, the +process `stoppedProcess A τ * B`, equal to `A` up to `τ` and to `A τ * B` after it, is a +supermartingale. -/ +theorem IsENNSupermartingale.stoppedProcess_mul {A B : ℕ → Ω → ℝ≥0∞} + (hA : IsENNSupermartingale A ℱ S) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) + (hB : IsENNSupermartingale B ℱ S) (hB1 : ∀ (n : ℕ) ω, (n : WithTop ℕ) ≤ τ ω → B n ω = 1) : + IsENNSupermartingale (stoppedProcess A τ * B) ℱ S := by + have hAτ := hA.adapted.stoppedProcess_of_discrete hτ + refine ⟨hAτ.mul hB.adapted, fun P hP n s hs ↦ ?_⟩ + rw [setLIntegral_stoppedProcess_mul_eq hτ hB1 n.le_succ le_rfl hs, + setLIntegral_stoppedProcess_mul_eq hτ hB1 le_rfl n.le_succ hs] + exact add_le_add (hB.setLIntegral_mul_succ_le hP (hAτ n) (hs.inter (hτ.measurableSet_le n))) + (hA.setLIntegral_succ_le P hP n _ (hs.diff (hτ.measurableSet_le n))) + +/-- **Optional continuation of test supermartingales** [RW, Proposition 7.9]. For a test +supermartingale `A`, a stopping time `τ` and an `ℝ≥0∞`-valued supermartingale `B` such that +`B n = 1` whenever `n ≤ τ`, the process `stoppedProcess A τ * B`, which continues the evidence +`A τ` gathered up to `τ` with the new experiment `B`, is a test supermartingale. -/ +theorem IsTestSupermartingale.stoppedProcess_mul {A B : ℕ → Ω → ℝ≥0∞} + (hA : IsTestSupermartingale A ℱ S) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) + (hB : IsENNSupermartingale B ℱ S) (hB1 : ∀ (n : ℕ) ω, (n : WithTop ℕ) ≤ τ ω → B n ω = 1) : + IsTestSupermartingale (stoppedProcess A τ * B) ℱ S := + ⟨hA.toIsENNSupermartingale.stoppedProcess_mul hτ hB hB1, fun P hP ↦ by + simpa [stoppedProcess_eq_of_le, hB1 0 _ (by simp)] using hA.lintegral_zero_le P hP⟩ + +/-- **Optional continuation of test martingales** [RW, Proposition 7.9]. For test martingales `A` +and `B` and a stopping time `τ` such that `B n = 1` whenever `n ≤ τ`, the process +`stoppedProcess A τ * B` is a test martingale. -/ +theorem IsTestMartingale.stoppedProcess_mul {A B : ℕ → Ω → ℝ≥0∞} + (hA : IsTestMartingale A ℱ S) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) + (hB : IsTestMartingale B ℱ S) (hB1 : ∀ (n : ℕ) ω, (n : WithTop ℕ) ≤ τ ω → B n ω = 1) : + IsTestMartingale (stoppedProcess A τ * B) ℱ S := by + have hAτ := hA.adapted.stoppedProcess_of_discrete hτ + refine ⟨hAτ.mul hB.adapted, fun P hP ↦ ?_, fun P hP n s hs ↦ ?_⟩ + · simpa [stoppedProcess_eq_of_le, hB1 0 _ (by simp)] using hA.lintegral_zero_le P hP + rw [setLIntegral_stoppedProcess_mul_eq hτ hB1 n.le_succ le_rfl hs, + setLIntegral_stoppedProcess_mul_eq hτ hB1 le_rfl n.le_succ hs] + congr 1 + · exact hB.setLIntegral_mul_succ_eq hP (hAτ n) (hs.inter (hτ.measurableSet_le n)) + · exact hA.setLIntegral_succ_eq P hP n _ (hs.diff (hτ.measurableSet_le n)) + +/-- An `ℝ≥0∞`-valued supermartingale stopped at a stopping time is a supermartingale. -/ +theorem IsENNSupermartingale.stoppedProcess (hM : IsENNSupermartingale M ℱ S) + {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) : + IsENNSupermartingale (stoppedProcess M τ) ℱ S := by + simpa using hM.stoppedProcess_mul hτ (B := 1) + ⟨fun _ ↦ measurable_const, fun _ _ _ _ _ ↦ le_rfl⟩ fun _ _ _ ↦ rfl + +/-- A test supermartingale stopped at a stopping time is a test supermartingale. -/ +theorem IsTestSupermartingale.stoppedProcess (hM : IsTestSupermartingale M ℱ S) + {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) : + IsTestSupermartingale (stoppedProcess M τ) ℱ S := + ⟨hM.toIsENNSupermartingale.stoppedProcess hτ, fun P hP ↦ by + simpa [stoppedProcess_eq_of_le] using hM.lintegral_zero_le P hP⟩ + +/-- A test martingale stopped at a stopping time is a test martingale. -/ +theorem IsTestMartingale.stoppedProcess (hM : IsTestMartingale M ℱ S) {τ : Ω → WithTop ℕ} + (hτ : IsStoppingTime ℱ τ) : IsTestMartingale (stoppedProcess M τ) ℱ S := by + refine ⟨hM.adapted.stoppedProcess_of_discrete hτ, fun P hP ↦ ?_, fun P hP n s hs ↦ ?_⟩ + · simpa [stoppedProcess_eq_of_le] using hM.lintegral_zero_le P hP + have h (j : ℕ) (hnj : n ≤ j) (hjn : j ≤ n + 1) := + setLIntegral_stoppedProcess_mul_eq (P := P) (A := M) (B := 1) hτ (fun _ _ _ ↦ rfl) hnj hjn hs + simp only [mul_one, Pi.one_apply] at h + rw [h (n + 1) n.le_succ le_rfl, h n le_rfl n.le_succ] + congr 1 + exact hM.setLIntegral_succ_eq P hP n _ (hs.diff (hτ.measurableSet_le n)) + +/-! ### Mixtures -/ + +section Mixture + +variable {Θ : Type*} {mΘ : MeasurableSpace Θ} {π : Measure Θ} {M : Θ → ℕ → Ω → ℝ≥0∞} + +/-- The mixture of a family of processes that is jointly measurable at every time, measurable in +the observations for `ℱ n` at time `n`, is adapted. -/ +private lemma adapted_lintegral [SFinite π] + (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) : + Adapted ℱ (fun n ω ↦ ∫⁻ θ, M θ n ω ∂π) := fun n ↦ + -- the measurable space on `Ω` is `ℱ n`, not the ambient `mΩ`, hence the explicit instances + @Measurable.lintegral_prod_left' Θ Ω mΘ (ℱ n) π _ _ (hM_meas n) + +/-- Integrals of a mixture over a set and over the mixing measure can be swapped. -/ +private lemma setLIntegral_lintegral_swap [SFinite π] (hP : SFinite P) + (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) (n : ℕ) (s : Set Ω) : + ∫⁻ ω in s, ∫⁻ θ, M θ n ω ∂π ∂P = ∫⁻ θ, ∫⁻ ω in s, M θ n ω ∂P ∂π := + lintegral_lintegral_swap + (((hM_meas n).mono (MeasurableSpace.prod_mono le_rfl (ℱ.le n)) le_rfl).comp + measurable_swap).aemeasurable + +/-- A mixture over a probability measure of processes whose initial values have expectation at +most `1` has initial value with expectation at most `1`. -/ +private lemma lintegral_lintegral_le_one [IsProbabilityMeasure π] (hP : SFinite P) + (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) + (hM : ∀ θ, ∫⁻ ω, M θ 0 ω ∂P ≤ 1) : ∫⁻ ω, ∫⁻ θ, M θ 0 ω ∂π ∂P ≤ 1 := by + calc ∫⁻ ω, ∫⁻ θ, M θ 0 ω ∂π ∂P = ∫⁻ θ, ∫⁻ ω, M θ 0 ω ∂P ∂π := by + simpa using setLIntegral_lintegral_swap (π := π) hP hM_meas 0 univ + _ ≤ ∫⁻ _, 1 ∂π := lintegral_mono hM + _ = 1 := by simp + +/-- **Mixtures of `ℝ≥0∞`-valued supermartingales.** For an s-finite measure `π` and a family +`M θ` of supermartingales, jointly measurable in `(θ, ω)` for `ℱ n` at every time `n`, the +mixture `∫⁻ θ, M θ n ω ∂π` is a supermartingale under every s-finite member of the null. No +integrability is needed. -/ +theorem isENNSupermartingale_lintegral [SFinite π] (hS : ∀ P ∈ S, SFinite P) + (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) + (hM : ∀ θ, IsENNSupermartingale (M θ) ℱ S) : + IsENNSupermartingale (fun n ω ↦ ∫⁻ θ, M θ n ω ∂π) ℱ S := by + refine ⟨adapted_lintegral hM_meas, fun P hP n s hs ↦ ?_⟩ + rw [setLIntegral_lintegral_swap (hS P hP) hM_meas, setLIntegral_lintegral_swap (hS P hP) hM_meas] + exact lintegral_mono fun θ ↦ (hM θ).setLIntegral_succ_le P hP n s hs + +/-- **Mixtures of test supermartingales.** For a probability measure `π` and a family `M θ` of +test supermartingales, jointly measurable in `(θ, ω)` for `ℱ n` at every time `n`, the mixture +`∫⁻ θ, M θ n ω ∂π` is a test supermartingale for every null of s-finite measures. -/ +theorem isTestSupermartingale_lintegral [IsProbabilityMeasure π] (hS : ∀ P ∈ S, SFinite P) + (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) + (hM : ∀ θ, IsTestSupermartingale (M θ) ℱ S) : + IsTestSupermartingale (fun n ω ↦ ∫⁻ θ, M θ n ω ∂π) ℱ S := + ⟨isENNSupermartingale_lintegral hS hM_meas fun θ ↦ (hM θ).toIsENNSupermartingale, + fun P hP ↦ lintegral_lintegral_le_one (hS P hP) hM_meas fun θ ↦ (hM θ).lintegral_zero_le P hP⟩ + +/-- **Mixtures of test martingales.** For a probability measure `π` and a family `M θ` of test +martingales, jointly measurable in `(θ, ω)` for `ℱ n` at every time `n`, the mixture +`∫⁻ θ, M θ n ω ∂π` is a test martingale for every null of s-finite measures. -/ +theorem isTestMartingale_lintegral [IsProbabilityMeasure π] (hS : ∀ P ∈ S, SFinite P) + (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) + (hM : ∀ θ, IsTestMartingale (M θ) ℱ S) : + IsTestMartingale (fun n ω ↦ ∫⁻ θ, M θ n ω ∂π) ℱ S := by + refine ⟨adapted_lintegral hM_meas, fun P hP ↦ ?_, fun P hP n s hs ↦ ?_⟩ + · exact lintegral_lintegral_le_one (hS P hP) hM_meas fun θ ↦ (hM θ).lintegral_zero_le P hP + rw [setLIntegral_lintegral_swap (hS P hP) hM_meas, setLIntegral_lintegral_swap (hS P hP) hM_meas] + exact lintegral_congr fun θ ↦ (hM θ).setLIntegral_succ_eq P hP n s hs + +end Mixture + end ProbabilityTheory diff --git a/LMLExplore/Probability/Process/Adapted.lean b/LMLExplore/Probability/Process/Adapted.lean index 414d3d5a..c9809e4a 100644 --- a/LMLExplore/Probability/Process/Adapted.lean +++ b/LMLExplore/Probability/Process/Adapted.lean @@ -5,23 +5,26 @@ Authors: LMLExplore contributors -/ module -public import Mathlib.Probability.Process.Adapted +public import Mathlib.Probability.Process.Stopping /-! -# Adapted products +# Adapted products and stopped processes A product `M₀ * ∏ k < n, F k` is adapted to a filtration `ℱ` indexed by `ℕ` when `M₀` is `ℱ 0`-measurable and each factor `F k` is `ℱ (k + 1)`-measurable. Such products are the wealth -processes of a gambler who reinvests at every round. +processes of a gambler who reinvests at every round. A process that is adapted, in the sense of +measurability, to a filtration indexed by a discrete order stays adapted when it is stopped at a +stopping time; Mathlib states this for strongly adapted processes. ## Main statements * `MeasureTheory.adapted_mul_prod_range`: the process `n ↦ M₀ * ∏ k < n, F k` is adapted. +* `MeasureTheory.Adapted.stoppedProcess_of_discrete`: a stopped adapted process is adapted. -/ public section -open Finset +open Finset TopologicalSpace namespace MeasureTheory @@ -36,4 +39,15 @@ theorem adapted_mul_prod_range {M₀ : Ω → β} (hM₀ : Measurable[ℱ 0] M (hM₀.mono (ℱ.mono n.zero_le) le_rfl).mul <| Finset.measurable_fun_prod _ fun k hk ↦ (hF k).mono (ℱ.mono (mem_range.1 hk)) le_rfl +/-- If the indexing order has the discrete topology, then the stopped process of an adapted +process with values in a second-countable pseudo-metrizable Borel space is adapted. This is the +measurable form of Mathlib's `StronglyAdapted.stoppedProcess_of_discrete`. -/ +theorem Adapted.stoppedProcess_of_discrete {ι γ : Type*} [Nonempty ι] [LinearOrder ι] + [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι] + [BorelSpace ι] [DiscreteTopology ι] [TopologicalSpace γ] [PseudoMetrizableSpace γ] + [SecondCountableTopology γ] [MeasurableSpace γ] [BorelSpace γ] {f : Filtration ι mΩ} + {u : ι → Ω → γ} (hu : Adapted f u) {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) : + Adapted f (stoppedProcess u τ) := + (hu.stronglyAdapted.stoppedProcess_of_discrete hτ).adapted + end MeasureTheory From d02830c621be5053afc39e12c38de6df7c23346d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 20:07:06 +0100 Subject: [PATCH 2/4] fix: address review of test supermartingale closure properties - Move `Adapted.stoppedProcess_of_discrete` to `Probability/Process/Stopping.lean` and restore the narrower import of `Probability/Process/Adapted.lean`. - Make `adapted_lintegral` public in `Probability/Process/Adapted.lean`, for any preorder index. - Weaken `IsTestMartingale.stoppedProcess_mul` to an adapted `B` with martingale steps, replace `IsTestMartingale.setLIntegral_mul_succ_eq` by `Adapted.setLIntegral_mul_succ_eq`, and derive `IsTestMartingale.stoppedProcess` as the case `B = 1`. - Fix the module and mixture docstrings. Co-Authored-By: Claude Code --- LMLExplore/EValues/TestSupermartingale.lean | 64 +++++++++----------- LMLExplore/Probability/Process/Adapted.lean | 35 +++++------ LMLExplore/Probability/Process/Stopping.lean | 26 +++++++- 3 files changed, 73 insertions(+), 52 deletions(-) diff --git a/LMLExplore/EValues/TestSupermartingale.lean b/LMLExplore/EValues/TestSupermartingale.lean index 89b86b19..0c33e395 100644 --- a/LMLExplore/EValues/TestSupermartingale.lean +++ b/LMLExplore/EValues/TestSupermartingale.lean @@ -8,6 +8,7 @@ module public import LMLExplore.EValues.CondEVariable public import LMLExplore.Probability.Martingale.Basic public import LMLExplore.Probability.Process.Adapted +public import LMLExplore.Probability.Process.Stopping /-! # Test supermartingales and wealth processes @@ -33,8 +34,9 @@ Test supermartingales are closed under the operations a statistician performs on evidence: stopping at a stopping time, taking the minimum of two of them, mixing a measurable family over a probability measure (Tonelli in `ℝ≥0∞`, with no integrability hypothesis), and optional continuation, in which the evidence `A τ` gathered up to a stopping time `τ` is -multiplied by a new process `B` that starts at `1` after `τ` [RW, Proposition 7.9]. These closure -properties transfer to e-processes through their domination by test supermartingales. +multiplied by a new supermartingale `B` that equals `1` up to time `τ` [RW, Proposition 7.9]. +These closure properties transfer to e-processes through their domination by test +supermartingales. ## Main definitions @@ -63,8 +65,10 @@ properties transfer to e-processes through their domination by test supermarting ratios, which are conditional e-variables [WSR24, Proposition 3]. * `ProbabilityTheory.IsTestSupermartingale.stoppedProcess_mul`, `ProbabilityTheory.IsTestMartingale.stoppedProcess_mul`: optional continuation - [RW, Proposition 7.9]; `ProbabilityTheory.IsTestSupermartingale.stoppedProcess` and - `ProbabilityTheory.IsTestMartingale.stoppedProcess` are the case `B = 1` of stopped processes. + [RW, Proposition 7.9]. +* `ProbabilityTheory.IsTestSupermartingale.stoppedProcess`, + `ProbabilityTheory.IsTestMartingale.stoppedProcess`: stopped test (super)martingales, the case + `B = 1` of optional continuation. * `ProbabilityTheory.IsTestSupermartingale.inf`: the minimum of two test supermartingales. * `ProbabilityTheory.isTestSupermartingale_lintegral`, `ProbabilityTheory.isTestMartingale_lintegral`: mixtures over a probability measure. @@ -471,17 +475,20 @@ theorem IsENNSupermartingale.setLIntegral_mul_succ_le (hM : IsENNSupermartingale (hM.measurable (n + 1)).aemeasurable (hM.measurable n).aemeasurable (hM.setLIntegral_succ_le P hP n) (hY.indicator hs) -/-- A factor `Y` and a set `s` that are `ℱ n`-measurable can be pulled out of a step of a test -martingale: `∫⁻ ω in s, Y ω * M (n + 1) ω ∂P = ∫⁻ ω in s, Y ω * M n ω ∂P`. -/ -theorem IsTestMartingale.setLIntegral_mul_succ_eq (hM : IsTestMartingale M ℱ S) - (hP : P ∈ S) {n : ℕ} {Y : Ω → ℝ≥0∞} (hY : Measurable[ℱ n] Y) {s : Set Ω} - (hs : MeasurableSet[ℱ n] s) : +/-- A factor `Y` and a set `s` that are `ℱ n`-measurable can be pulled out of a martingale step +of an adapted `ℝ≥0∞`-valued process, that is, a step whose set integrals over `ℱ n`-measurable +sets agree at times `n` and `n + 1`: +`∫⁻ ω in s, Y ω * M (n + 1) ω ∂P = ∫⁻ ω in s, Y ω * M n ω ∂P`. This applies to a test martingale, +but no bound on the initial expectation is needed. -/ +theorem _root_.MeasureTheory.Adapted.setLIntegral_mul_succ_eq (hM : Adapted ℱ M) {n : ℕ} + (hMn : ∀ s, MeasurableSet[ℱ n] s → ∫⁻ ω in s, M (n + 1) ω ∂P = ∫⁻ ω in s, M n ω ∂P) + {Y : Ω → ℝ≥0∞} (hY : Measurable[ℱ n] Y) {s : Set Ω} (hs : MeasurableSet[ℱ n] s) : ∫⁻ ω in s, Y ω * M (n + 1) ω ∂P = ∫⁻ ω in s, Y ω * M n ω ∂P := by rw [← lintegral_indicator (ℱ.le n s hs), ← lintegral_indicator (ℱ.le n s hs)] simp_rw [indicator_mul_left] exact lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq (ℱ.le n) - (hM.measurable (n + 1)).aemeasurable (hM.measurable n).aemeasurable - (hM.setLIntegral_succ_eq P hP n) (hY.indicator hs) + ((hM (n + 1)).mono (ℱ.le (n + 1)) le_rfl).aemeasurable + ((hM n).mono (ℱ.le n) le_rfl).aemeasurable hMn (hY.indicator hs) /-! ### Minima -/ @@ -574,20 +581,23 @@ theorem IsTestSupermartingale.stoppedProcess_mul {A B : ℕ → Ω → ℝ≥0 ⟨hA.toIsENNSupermartingale.stoppedProcess_mul hτ hB hB1, fun P hP ↦ by simpa [stoppedProcess_eq_of_le, hB1 0 _ (by simp)] using hA.lintegral_zero_le P hP⟩ -/-- **Optional continuation of test martingales** [RW, Proposition 7.9]. For test martingales `A` -and `B` and a stopping time `τ` such that `B n = 1` whenever `n ≤ τ`, the process -`stoppedProcess A τ * B` is a test martingale. -/ +/-- **Optional continuation of test martingales** [RW, Proposition 7.9]. For a test martingale +`A`, a stopping time `τ` and an adapted `ℝ≥0∞`-valued process `B` whose set integrals over +`ℱ n`-measurable sets agree at times `n` and `n + 1` under every member of the null, such that +`B n = 1` whenever `n ≤ τ`, the process `stoppedProcess A τ * B` is a test martingale. -/ theorem IsTestMartingale.stoppedProcess_mul {A B : ℕ → Ω → ℝ≥0∞} (hA : IsTestMartingale A ℱ S) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) - (hB : IsTestMartingale B ℱ S) (hB1 : ∀ (n : ℕ) ω, (n : WithTop ℕ) ≤ τ ω → B n ω = 1) : + (hBa : Adapted ℱ B) (hB : ∀ P ∈ S, ∀ n s, MeasurableSet[ℱ n] s → + ∫⁻ ω in s, B (n + 1) ω ∂P = ∫⁻ ω in s, B n ω ∂P) + (hB1 : ∀ (n : ℕ) ω, (n : WithTop ℕ) ≤ τ ω → B n ω = 1) : IsTestMartingale (stoppedProcess A τ * B) ℱ S := by have hAτ := hA.adapted.stoppedProcess_of_discrete hτ - refine ⟨hAτ.mul hB.adapted, fun P hP ↦ ?_, fun P hP n s hs ↦ ?_⟩ + refine ⟨hAτ.mul hBa, fun P hP ↦ ?_, fun P hP n s hs ↦ ?_⟩ · simpa [stoppedProcess_eq_of_le, hB1 0 _ (by simp)] using hA.lintegral_zero_le P hP rw [setLIntegral_stoppedProcess_mul_eq hτ hB1 n.le_succ le_rfl hs, setLIntegral_stoppedProcess_mul_eq hτ hB1 le_rfl n.le_succ hs] congr 1 - · exact hB.setLIntegral_mul_succ_eq hP (hAτ n) (hs.inter (hτ.measurableSet_le n)) + · exact hBa.setLIntegral_mul_succ_eq (hB P hP n) (hAτ n) (hs.inter (hτ.measurableSet_le n)) · exact hA.setLIntegral_succ_eq P hP n _ (hs.diff (hτ.measurableSet_le n)) /-- An `ℝ≥0∞`-valued supermartingale stopped at a stopping time is a supermartingale. -/ @@ -607,14 +617,8 @@ theorem IsTestSupermartingale.stoppedProcess (hM : IsTestSupermartingale M ℱ S /-- A test martingale stopped at a stopping time is a test martingale. -/ theorem IsTestMartingale.stoppedProcess (hM : IsTestMartingale M ℱ S) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) : IsTestMartingale (stoppedProcess M τ) ℱ S := by - refine ⟨hM.adapted.stoppedProcess_of_discrete hτ, fun P hP ↦ ?_, fun P hP n s hs ↦ ?_⟩ - · simpa [stoppedProcess_eq_of_le] using hM.lintegral_zero_le P hP - have h (j : ℕ) (hnj : n ≤ j) (hjn : j ≤ n + 1) := - setLIntegral_stoppedProcess_mul_eq (P := P) (A := M) (B := 1) hτ (fun _ _ _ ↦ rfl) hnj hjn hs - simp only [mul_one, Pi.one_apply] at h - rw [h (n + 1) n.le_succ le_rfl, h n le_rfl n.le_succ] - congr 1 - exact hM.setLIntegral_succ_eq P hP n _ (hs.diff (hτ.measurableSet_le n)) + simpa using hM.stoppedProcess_mul hτ (B := 1) (fun _ ↦ measurable_const) + (fun _ _ _ _ _ ↦ rfl) fun _ _ _ ↦ rfl /-! ### Mixtures -/ @@ -622,14 +626,6 @@ section Mixture variable {Θ : Type*} {mΘ : MeasurableSpace Θ} {π : Measure Θ} {M : Θ → ℕ → Ω → ℝ≥0∞} -/-- The mixture of a family of processes that is jointly measurable at every time, measurable in -the observations for `ℱ n` at time `n`, is adapted. -/ -private lemma adapted_lintegral [SFinite π] - (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) : - Adapted ℱ (fun n ω ↦ ∫⁻ θ, M θ n ω ∂π) := fun n ↦ - -- the measurable space on `Ω` is `ℱ n`, not the ambient `mΩ`, hence the explicit instances - @Measurable.lintegral_prod_left' Θ Ω mΘ (ℱ n) π _ _ (hM_meas n) - /-- Integrals of a mixture over a set and over the mixing measure can be swapped. -/ private lemma setLIntegral_lintegral_swap [SFinite π] (hP : SFinite P) (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) (n : ℕ) (s : Set Ω) : @@ -650,7 +646,7 @@ private lemma lintegral_lintegral_le_one [IsProbabilityMeasure π] (hP : SFinite /-- **Mixtures of `ℝ≥0∞`-valued supermartingales.** For an s-finite measure `π` and a family `M θ` of supermartingales, jointly measurable in `(θ, ω)` for `ℱ n` at every time `n`, the -mixture `∫⁻ θ, M θ n ω ∂π` is a supermartingale under every s-finite member of the null. No +mixture `∫⁻ θ, M θ n ω ∂π` is a supermartingale for every null `S` of s-finite measures. No integrability is needed. -/ theorem isENNSupermartingale_lintegral [SFinite π] (hS : ∀ P ∈ S, SFinite P) (hM_meas : ∀ n, Measurable[mΘ.prod (ℱ n)] fun p : Θ × Ω ↦ M p.1 n p.2) diff --git a/LMLExplore/Probability/Process/Adapted.lean b/LMLExplore/Probability/Process/Adapted.lean index c9809e4a..f4f61d9f 100644 --- a/LMLExplore/Probability/Process/Adapted.lean +++ b/LMLExplore/Probability/Process/Adapted.lean @@ -5,26 +5,28 @@ Authors: LMLExplore contributors -/ module -public import Mathlib.Probability.Process.Stopping +public import Mathlib.MeasureTheory.Measure.Prod +public import Mathlib.Probability.Process.Adapted /-! -# Adapted products and stopped processes +# Adapted products and mixtures A product `M₀ * ∏ k < n, F k` is adapted to a filtration `ℱ` indexed by `ℕ` when `M₀` is `ℱ 0`-measurable and each factor `F k` is `ℱ (k + 1)`-measurable. Such products are the wealth -processes of a gambler who reinvests at every round. A process that is adapted, in the sense of -measurability, to a filtration indexed by a discrete order stays adapted when it is stopped at a -stopping time; Mathlib states this for strongly adapted processes. +processes of a gambler who reinvests at every round. A mixture `∫⁻ θ, M θ i ω ∂π` of a family of +`ℝ≥0∞`-valued processes over an s-finite measure is adapted when the family is jointly measurable +in `(θ, ω)` for `ℱ i` at every time `i`. ## Main statements * `MeasureTheory.adapted_mul_prod_range`: the process `n ↦ M₀ * ∏ k < n, F k` is adapted. -* `MeasureTheory.Adapted.stoppedProcess_of_discrete`: a stopped adapted process is adapted. +* `MeasureTheory.adapted_lintegral`: the mixture `i ↦ ∫⁻ θ, M θ i · ∂π` is adapted. -/ public section -open Finset TopologicalSpace +open Finset +open scoped ENNReal namespace MeasureTheory @@ -39,15 +41,14 @@ theorem adapted_mul_prod_range {M₀ : Ω → β} (hM₀ : Measurable[ℱ 0] M (hM₀.mono (ℱ.mono n.zero_le) le_rfl).mul <| Finset.measurable_fun_prod _ fun k hk ↦ (hF k).mono (ℱ.mono (mem_range.1 hk)) le_rfl -/-- If the indexing order has the discrete topology, then the stopped process of an adapted -process with values in a second-countable pseudo-metrizable Borel space is adapted. This is the -measurable form of Mathlib's `StronglyAdapted.stoppedProcess_of_discrete`. -/ -theorem Adapted.stoppedProcess_of_discrete {ι γ : Type*} [Nonempty ι] [LinearOrder ι] - [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι] - [BorelSpace ι] [DiscreteTopology ι] [TopologicalSpace γ] [PseudoMetrizableSpace γ] - [SecondCountableTopology γ] [MeasurableSpace γ] [BorelSpace γ] {f : Filtration ι mΩ} - {u : ι → Ω → γ} (hu : Adapted f u) {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) : - Adapted f (stoppedProcess u τ) := - (hu.stronglyAdapted.stoppedProcess_of_discrete hτ).adapted +/-- The mixture `i ↦ ∫⁻ θ, M θ i · ∂π` over an s-finite measure `π` of a family of +`ℝ≥0∞`-valued processes is adapted when, at every time `i`, the family is jointly measurable in +`(θ, ω)` for the product of the σ-algebra of `Θ` and `f i`. -/ +theorem adapted_lintegral {ι Θ : Type*} [Preorder ι] {mΘ : MeasurableSpace Θ} {π : Measure Θ} + [SFinite π] {f : Filtration ι mΩ} {M : Θ → ι → Ω → ℝ≥0∞} + (hM : ∀ i, Measurable[mΘ.prod (f i)] fun p : Θ × Ω ↦ M p.1 i p.2) : + Adapted f (fun i ω ↦ ∫⁻ θ, M θ i ω ∂π) := fun i ↦ + -- the measurable space on `Ω` is `f i`, not the ambient `mΩ`, hence the explicit instances + @Measurable.lintegral_prod_left' Θ Ω mΘ (f i) π _ _ (hM i) end MeasureTheory diff --git a/LMLExplore/Probability/Process/Stopping.lean b/LMLExplore/Probability/Process/Stopping.lean index a422b996..09cc9e05 100644 --- a/LMLExplore/Probability/Process/Stopping.lean +++ b/LMLExplore/Probability/Process/Stopping.lean @@ -9,7 +9,7 @@ public import Mathlib.MeasureTheory.MeasurableSpace.Instances public import Mathlib.Probability.Process.Stopping /-! -# Measurability of stopping times valued in `ℕ∞` +# Stopping times valued in `ℕ∞` and stopped adapted processes 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. @@ -17,14 +17,21 @@ The same type seen as `ℕ∞` carries the discrete σ-algebra `⊤`; the two in syntactically equal. This file states measurability of such a stopping time for the discrete σ-algebra of `ℕ∞`. +A process that is adapted, in the sense of measurability, to a filtration indexed by a discrete +order stays adapted when it is stopped at a stopping time; Mathlib states this for strongly adapted +processes. + ## Main statements * `MeasureTheory.IsStoppingTime.measurable_enat`: a stopping time `τ : Ω → ℕ∞` of a filtration indexed by `ℕ` is measurable for the discrete σ-algebra of `ℕ∞`. +* `MeasureTheory.Adapted.stoppedProcess_of_discrete`: a stopped adapted process is adapted. -/ public section +open TopologicalSpace + namespace MeasureTheory.IsStoppingTime variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {f : Filtration ℕ mΩ} {τ : Ω → ℕ∞} @@ -39,3 +46,20 @@ lemma measurable_enat (hτ : IsStoppingTime f τ) : Measurable τ := measurable_to_countable' fun x ↦ hτ.measurable' (measurableSet_singleton (α := WithTop ℕ) x) end MeasureTheory.IsStoppingTime + +namespace MeasureTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} + +/-- If the indexing order has the discrete topology, then the stopped process of an adapted +process with values in a second-countable pseudo-metrizable Borel space is adapted. This is the +measurable form of Mathlib's `StronglyAdapted.stoppedProcess_of_discrete`. -/ +theorem Adapted.stoppedProcess_of_discrete {ι γ : Type*} [Nonempty ι] [LinearOrder ι] + [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι] + [BorelSpace ι] [DiscreteTopology ι] [TopologicalSpace γ] [PseudoMetrizableSpace γ] + [SecondCountableTopology γ] [MeasurableSpace γ] [BorelSpace γ] {f : Filtration ι mΩ} + {u : ι → Ω → γ} (hu : Adapted f u) {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) : + Adapted f (stoppedProcess u τ) := + (hu.stronglyAdapted.stoppedProcess_of_discrete hτ).adapted + +end MeasureTheory From f8beda29a9d484cf8fd374351aed906a0a509db7 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 20:39:36 +0100 Subject: [PATCH 3/4] refactor: factor set-integral weight pulls through WithDensity lemmas Add setLIntegral_mul_le_setLIntegral_mul_of_forall_setLIntegral_le and its _eq twin in MeasureTheory/Measure/WithDensity.lean, make IsENNSupermartingale.setLIntegral_mul_succ_le a one-line use of the first, and replace the misplaced Adapted.setLIntegral_mul_succ_eq by a direct use of the second in IsTestMartingale.stoppedProcess_mul. Co-Authored-By: Claude Code --- LMLExplore/EValues/TestSupermartingale.lean | 28 +++++-------------- .../MeasureTheory/Measure/WithDensity.lean | 28 +++++++++++++++++++ 2 files changed, 35 insertions(+), 21 deletions(-) diff --git a/LMLExplore/EValues/TestSupermartingale.lean b/LMLExplore/EValues/TestSupermartingale.lean index 0c33e395..0bdb7d88 100644 --- a/LMLExplore/EValues/TestSupermartingale.lean +++ b/LMLExplore/EValues/TestSupermartingale.lean @@ -468,27 +468,10 @@ theorem IsTestSupermartingale.ae_eq_mul_prod_div (hM : IsTestSupermartingale M theorem IsENNSupermartingale.setLIntegral_mul_succ_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) {n : ℕ} {Y : Ω → ℝ≥0∞} (hY : Measurable[ℱ n] Y) {s : Set Ω} (hs : MeasurableSet[ℱ n] s) : - ∫⁻ ω in s, Y ω * M (n + 1) ω ∂P ≤ ∫⁻ ω in s, Y ω * M n ω ∂P := by - rw [← lintegral_indicator (ℱ.le n s hs), ← lintegral_indicator (ℱ.le n s hs)] - simp_rw [indicator_mul_left] - exact lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le (ℱ.le n) + ∫⁻ ω in s, Y ω * M (n + 1) ω ∂P ≤ ∫⁻ ω in s, Y ω * M n ω ∂P := + setLIntegral_mul_le_setLIntegral_mul_of_forall_setLIntegral_le (ℱ.le n) (hM.measurable (n + 1)).aemeasurable (hM.measurable n).aemeasurable - (hM.setLIntegral_succ_le P hP n) (hY.indicator hs) - -/-- A factor `Y` and a set `s` that are `ℱ n`-measurable can be pulled out of a martingale step -of an adapted `ℝ≥0∞`-valued process, that is, a step whose set integrals over `ℱ n`-measurable -sets agree at times `n` and `n + 1`: -`∫⁻ ω in s, Y ω * M (n + 1) ω ∂P = ∫⁻ ω in s, Y ω * M n ω ∂P`. This applies to a test martingale, -but no bound on the initial expectation is needed. -/ -theorem _root_.MeasureTheory.Adapted.setLIntegral_mul_succ_eq (hM : Adapted ℱ M) {n : ℕ} - (hMn : ∀ s, MeasurableSet[ℱ n] s → ∫⁻ ω in s, M (n + 1) ω ∂P = ∫⁻ ω in s, M n ω ∂P) - {Y : Ω → ℝ≥0∞} (hY : Measurable[ℱ n] Y) {s : Set Ω} (hs : MeasurableSet[ℱ n] s) : - ∫⁻ ω in s, Y ω * M (n + 1) ω ∂P = ∫⁻ ω in s, Y ω * M n ω ∂P := by - rw [← lintegral_indicator (ℱ.le n s hs), ← lintegral_indicator (ℱ.le n s hs)] - simp_rw [indicator_mul_left] - exact lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq (ℱ.le n) - ((hM (n + 1)).mono (ℱ.le (n + 1)) le_rfl).aemeasurable - ((hM n).mono (ℱ.le n) le_rfl).aemeasurable hMn (hY.indicator hs) + (hM.setLIntegral_succ_le P hP n) hY hs /-! ### Minima -/ @@ -597,7 +580,10 @@ theorem IsTestMartingale.stoppedProcess_mul {A B : ℕ → Ω → ℝ≥0∞} rw [setLIntegral_stoppedProcess_mul_eq hτ hB1 n.le_succ le_rfl hs, setLIntegral_stoppedProcess_mul_eq hτ hB1 le_rfl n.le_succ hs] congr 1 - · exact hBa.setLIntegral_mul_succ_eq (hB P hP n) (hAτ n) (hs.inter (hτ.measurableSet_le n)) + · exact setLIntegral_mul_eq_setLIntegral_mul_of_forall_setLIntegral_eq (ℱ.le n) + ((hBa (n + 1)).mono (ℱ.le (n + 1)) le_rfl).aemeasurable + ((hBa n).mono (ℱ.le n) le_rfl).aemeasurable (hB P hP n) (hAτ n) + (hs.inter (hτ.measurableSet_le n)) · exact hA.setLIntegral_succ_eq P hP n _ (hs.diff (hτ.measurableSet_le n)) /-- An `ℝ≥0∞`-valued supermartingale stopped at a stopping time is a supermartingale. -/ diff --git a/LMLExplore/MeasureTheory/Measure/WithDensity.lean b/LMLExplore/MeasureTheory/Measure/WithDensity.lean index 79628bbe..f71701c2 100644 --- a/LMLExplore/MeasureTheory/Measure/WithDensity.lean +++ b/LMLExplore/MeasureTheory/Measure/WithDensity.lean @@ -27,10 +27,14 @@ conditionally bounded increment. * `MeasureTheory.lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le`, `MeasureTheory.lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq`: they extend to `m`-measurable weights. +* `MeasureTheory.setLIntegral_mul_le_setLIntegral_mul_of_forall_setLIntegral_le`, + `MeasureTheory.setLIntegral_mul_eq_setLIntegral_mul_of_forall_setLIntegral_eq`: the same over an + `m`-measurable set. -/ public section +open Set open scoped ENNReal namespace MeasureTheory @@ -87,4 +91,28 @@ theorem lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq (hm : m ≤ mΩ lintegral_mul_eq_lintegral_trim_withDensity hm hg hY, (withDensity_trim_eq_withDensity_trim_iff hm).2 h] +/-- If the set integrals of `f` are at most those of `g` over the `m`-measurable sets, then +`∫⁻ ω in s, Y ω * f ω ∂μ ≤ ∫⁻ ω in s, Y ω * g ω ∂μ` for every `m`-measurable `Y : Ω → ℝ≥0∞` and +`m`-measurable set `s`. -/ +theorem setLIntegral_mul_le_setLIntegral_mul_of_forall_setLIntegral_le (hm : m ≤ mΩ) + (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) + (h : ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, f ω ∂μ ≤ ∫⁻ ω in s, g ω ∂μ) + (hY : Measurable[m] Y) {s : Set Ω} (hs : MeasurableSet[m] s) : + ∫⁻ ω in s, Y ω * f ω ∂μ ≤ ∫⁻ ω in s, Y ω * g ω ∂μ := by + rw [← lintegral_indicator (hm s hs), ← lintegral_indicator (hm s hs)] + simp_rw [indicator_mul_left] + exact lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le hm hf hg h (hY.indicator hs) + +/-- If the set integrals of `f` and `g` agree over the `m`-measurable sets, then +`∫⁻ ω in s, Y ω * f ω ∂μ = ∫⁻ ω in s, Y ω * g ω ∂μ` for every `m`-measurable `Y : Ω → ℝ≥0∞` and +`m`-measurable set `s`. -/ +theorem setLIntegral_mul_eq_setLIntegral_mul_of_forall_setLIntegral_eq (hm : m ≤ mΩ) + (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) + (h : ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, f ω ∂μ = ∫⁻ ω in s, g ω ∂μ) + (hY : Measurable[m] Y) {s : Set Ω} (hs : MeasurableSet[m] s) : + ∫⁻ ω in s, Y ω * f ω ∂μ = ∫⁻ ω in s, Y ω * g ω ∂μ := by + rw [← lintegral_indicator (hm s hs), ← lintegral_indicator (hm s hs)] + simp_rw [indicator_mul_left] + exact lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq hm hf hg h (hY.indicator hs) + end MeasureTheory From 09f5d33caba39e1c5fa833611a6807707452c4ce Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 21:03:03 +0100 Subject: [PATCH 4/4] doc: state the s-finite null of the mixture theorems in the module docstring Drop the unproved claim that the closure properties transfer to e-processes. Co-Authored-By: Claude Code --- LMLExplore/EValues/TestSupermartingale.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/LMLExplore/EValues/TestSupermartingale.lean b/LMLExplore/EValues/TestSupermartingale.lean index 0bdb7d88..be665cdc 100644 --- a/LMLExplore/EValues/TestSupermartingale.lean +++ b/LMLExplore/EValues/TestSupermartingale.lean @@ -32,11 +32,10 @@ conditional e-variables with predictable weights [WSJ26], and betting Test supermartingales are closed under the operations a statistician performs on running evidence: stopping at a stopping time, taking the minimum of two of them, mixing a measurable -family over a probability measure (Tonelli in `ℝ≥0∞`, with no integrability hypothesis), and -optional continuation, in which the evidence `A τ` gathered up to a stopping time `τ` is -multiplied by a new supermartingale `B` that equals `1` up to time `τ` [RW, Proposition 7.9]. -These closure properties transfer to e-processes through their domination by test -supermartingales. +family over a probability measure for a null of s-finite measures (Tonelli in `ℝ≥0∞`, with no +integrability hypothesis), and optional continuation, in which the evidence `A τ` gathered up to a +stopping time `τ` is multiplied by a new supermartingale `B` that equals `1` up to time `τ` +[RW, Proposition 7.9]. ## Main definitions @@ -71,7 +70,8 @@ supermartingales. `B = 1` of optional continuation. * `ProbabilityTheory.IsTestSupermartingale.inf`: the minimum of two test supermartingales. * `ProbabilityTheory.isTestSupermartingale_lintegral`, - `ProbabilityTheory.isTestMartingale_lintegral`: mixtures over a probability measure. + `ProbabilityTheory.isTestMartingale_lintegral`: mixtures over a probability measure, for a null + of s-finite measures. ## References