From 32dd5c5f1837c335cb2aa49192d3cc9203809d60 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 00:38:27 +0100 Subject: [PATCH 1/6] =?UTF-8?q?feat:=20the=20exact=20Ville=20identity,=20t?= =?UTF-8?q?he=20extended=20Ville=20inequality=20and=20Ville's=20inequality?= =?UTF-8?q?=20in=20=E2=84=9D=E2=89=A50=E2=88=9E?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Code Co-Authored-By: Claude Opus 5.5 --- .../Probability/Martingale/Centering.lean | 95 ++++ .../Probability/Martingale/ExactVille.lean | 496 ++++++++++++++++++ 2 files changed, 591 insertions(+) create mode 100644 LMLExplore/Probability/Martingale/Centering.lean create mode 100644 LMLExplore/Probability/Martingale/ExactVille.lean diff --git a/LMLExplore/Probability/Martingale/Centering.lean b/LMLExplore/Probability/Martingale/Centering.lean new file mode 100644 index 00000000..ac74f528 --- /dev/null +++ b/LMLExplore/Probability/Martingale/Centering.lean @@ -0,0 +1,95 @@ +/- +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.Martingale.Centering +public import Mathlib.Probability.Process.Stopping + +/-! +# The Doob decomposition at stopping times + +Mathlib's `MeasureTheory.predictablePart f ℱ μ` is the predictable part of the Doob decomposition +of a process `f` indexed by `ℕ`: `predictablePart f ℱ μ n = ∑ k < n, μ[f (k + 1) - f k | ℱ k]`. +Between two bounded stopping times `σ ≤ τ`, the increments of an integrable process and those of +its predictable part have the same set integrals over every set measurable for the σ-algebra at +`σ`: the martingale part of the decomposition has no drift. No adaptedness is needed. + +This identity is the expectation form of optional stopping for every integrable process, and +the source of exact identities such as the exact Ville identity, in which the predictable part +measures the decrease of a supermartingale up to a hitting time. + +## Main statements + +* `MeasureTheory.setIntegral_stoppedValue_sub_eq_predictablePart`: for bounded stopping times + `σ ≤ τ` and `s` measurable at `σ`, + `∫ ω in s, f τ - f σ ∂μ = ∫ ω in s, predictablePart f τ - predictablePart f σ ∂μ`. +* `MeasureTheory.Supermartingale.antitone_predictablePart`: the predictable part of a + supermartingale is almost surely antitone. +-/ + +public section + +open Finset Set + +namespace MeasureTheory + +variable {Ω E : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] + [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ mΩ} + {σ τ : Ω → WithTop ℕ} + +/-- **The Doob decomposition between stopping times.** For an integrable process `f`, bounded +stopping times `σ ≤ τ` and a set `s` measurable for the σ-algebra at `σ`, the increments of `f` and +of its predictable part from `σ` to `τ` have the same integral over `s`. -/ +theorem setIntegral_stoppedValue_sub_eq_predictablePart [SigmaFiniteFiltration μ ℱ] + (hf : ∀ n, Integrable (f n) μ) (hσ : IsStoppingTime ℱ σ) (hτ : IsStoppingTime ℱ τ) + (hστ : σ ≤ τ) {N : ℕ} (hτN : ∀ ω, τ ω ≤ N) {s : Set Ω} + (hs : MeasurableSet[hσ.measurableSpace] s) : + ∫ ω in s, stoppedValue f τ ω - stoppedValue f σ ω ∂μ = + ∫ ω in s, stoppedValue (predictablePart f ℱ μ) τ ω - + stoppedValue (predictablePart f ℱ μ) σ ω ∂μ := by + -- The set `{σ ≤ k < τ}`, and its intersection with `s`, are `ℱ k`-measurable. + have hmeas' (k : ℕ) : MeasurableSet[ℱ k] {ω | σ ω ≤ k ∧ k < τ ω} := by + rw [ofPred_and] + have h₁ : MeasurableSet[ℱ k] {ω | σ ω ≤ k} := by simpa using hσ.measurableSet_le k + have h₂ : MeasurableSet[ℱ k] {ω | k < τ ω} := by simpa using hτ.measurableSet_gt k + exact h₁.inter h₂ + have hmeas (k : ℕ) : MeasurableSet[ℱ k] (s ∩ {ω | σ ω ≤ k ∧ k < τ ω}) := by + have h₁ : MeasurableSet[ℱ k] (s ∩ {ω | σ ω ≤ k}) := by simpa using hs.2 k + have h₂ : MeasurableSet[ℱ k] {ω | k < τ ω} := by simpa using hτ.measurableSet_gt k + rw [ofPred_and, ← Set.inter_assoc] + exact h₁.inter h₂ + -- Both increments are sums over `k ≤ N` of the increments from `k` to `k + 1` on `{σ ≤ k < τ}`. + have hsum (g : ℕ → Ω → E) (ω : Ω) : stoppedValue g τ ω - stoppedValue g σ ω = + ∑ k ∈ range (N + 1), {ω | σ ω ≤ k ∧ k < τ ω}.indicator (g (k + 1) - g k) ω := by + simpa [Finset.sum_apply] using congrFun (stoppedValue_sub_eq_sum' (u := g) hστ hτN) ω + have hint (k : ℕ) : Integrable (f (k + 1) - f k) μ := (hf (k + 1)).sub (hf k) + have hA (k : ℕ) : predictablePart f ℱ μ (k + 1) - predictablePart f ℱ μ k = + μ[f (k + 1) - f k | ℱ k] := by + rw [predictablePart_add_one, add_sub_cancel_left] + simp_rw [hsum, hA] + rw [integral_finsetSum _ fun k _ ↦ ((hint k).indicator (ℱ.le k _ (hmeas' k))).integrableOn, + integral_finsetSum _ fun k _ ↦ + (integrable_condExp.indicator (ℱ.le k _ (hmeas' k))).integrableOn] + refine Finset.sum_congr rfl fun k _ ↦ ?_ + rw [setIntegral_indicator (ℱ.le k _ (hmeas' k)), setIntegral_indicator (ℱ.le k _ (hmeas' k)), + setIntegral_condExp (ℱ.le k) (hint k) (hmeas k)] + +/-- The predictable part of a supermartingale is almost surely antitone: the supermartingale +counterpart of Mathlib's `MeasureTheory.Submartingale.monotone_predictablePart`. -/ +theorem Supermartingale.antitone_predictablePart [PartialOrder E] [IsOrderedAddMonoid E] + (hf : Supermartingale f ℱ μ) : ∀ᵐ ω ∂μ, Antitone (predictablePart f ℱ μ · ω) := by + have h (n : ℕ) : μ[f (n + 1) - f n | ℱ n] ≤ᵐ[μ] 0 := by + have h' := hf.neg.condExp_sub_nonneg n.le_succ + rw [Pi.neg_apply, Pi.neg_apply, neg_sub_neg, ← neg_sub] at h' + filter_upwards [h', condExp_neg (f (n + 1) - f n) (ℱ n)] with ω hω hneg + rw [hneg, Pi.neg_apply, Pi.zero_apply, neg_nonneg] at hω + exact hω + filter_upwards [ae_all_iff.2 h] with ω hω + refine antitone_nat_of_succ_le fun n ↦ ?_ + rw [predictablePart_add_one, Pi.add_apply, add_le_iff_nonpos_right] + exact hω n + +end MeasureTheory diff --git a/LMLExplore/Probability/Martingale/ExactVille.lean b/LMLExplore/Probability/Martingale/ExactVille.lean new file mode 100644 index 00000000..3f084712 --- /dev/null +++ b/LMLExplore/Probability/Martingale/ExactVille.lean @@ -0,0 +1,496 @@ +/- +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.Probability.Martingale.Centering +public import LMLExplore.Probability.Martingale.OptionalStopping +public import Mathlib.Probability.Process.HittingTime + +/-! +# The exact Ville identity + +For an `ℝ≥0∞`-valued supermartingale `M` (`ProbabilityTheory.IsENNSupermartingale`) with finite +initial expectation under a finite measure `P`, a level `b`, and the first time `T` after `m` at +which `b ≤ M n`, the exact Ville identity [dlP+26, Theorem 1] decomposes the initial wealth +exactly: for every horizon `N ≥ m` and every `ℱ m`-measurable set `s`, +$$\int_s M_m = b\,P(s\cap\{T\le N\}) + \int_{s\cap\{T\le N\}}(M_T-b) + + \int_s\sum_{m\le kN\}}M_N,$$ +the four terms being the level reached, the overshoot, the predictable decrease and the +remainder. The decrease is read off Mathlib's `MeasureTheory.predictablePart` of the real +values `(M n).toReal`: it is `A m - A (T ∧ N)` for `A` that predictable part, the value at +`T ∧ N` of the almost surely nondecreasing process `D n = ofReal (A m - A n)`. Letting the +horizon tend to infinity gives the identity without horizon [dlP+26, Theorem 4], with the +overshoot over `{T < ∞}`, the decrease up to `T` (read with `MeasureTheory.stoppedValueLimsup`) +and the remainder `⨅ N ≥ m, ∫⁻ ω in s ∩ {N < T}, M N ω ∂P`, the limit of the remainders. + +All terms are nonnegative: dropping overshoot, decrease and remainder gives Ville's inequality +[Vil39; RW, Fact 7.6], with equality exactly when the three vanish. From time `m` on `s`, it +gives the extended Ville inequality [WR23, Theorem 4.1] for every `ℝ≥0∞`-valued supermartingale, +with no integrability condition: +`P (s ∩ {∃ n ≥ m, c ≤ M n}) ≤ (∫⁻ ω in s, min (M m ω) c ∂P) / c`. Ville's inequality for test +supermartingales, `P {∃ n, α⁻¹ ≤ M n} ≤ α`, is the time-uniform validity of the test that +rejects the null as soon as the evidence exceeds `α⁻¹`. + +## Main statements + +* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup`: exact optional + stopping at a bounded stopping time `τ ≥ m`: `∫⁻ ω in s, M m ω ∂P` is the integral of `M` at + `τ` plus that of the decrease up to `τ`. +* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_eq_exact_ville_horizon`, + `ProbabilityTheory.IsENNSupermartingale.lintegral_zero_eq_exact_ville_horizon`: the exact Ville + identity with a horizon [dlP+26, Theorem 1]. +* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_eq_exact_ville`, + `ProbabilityTheory.IsENNSupermartingale.lintegral_zero_eq_exact_ville`: the exact Ville identity + without horizon [dlP+26, Theorem 4]. +* `ProbabilityTheory.IsENNSupermartingale.mul_measure_inter_eq_setLIntegral_iff`: equality in + Ville's inequality holds exactly when overshoot, decrease and remainder vanish. +* `ProbabilityTheory.IsENNSupermartingale.measure_inter_exists_le_le`: the extended Ville + inequality from time `m` [WR23, Theorem 4.1]. +* `ProbabilityTheory.IsENNSupermartingale.measure_exists_le_le`, + `ProbabilityTheory.IsTestSupermartingale.measure_exists_le_le`, + `ProbabilityTheory.IsTestSupermartingale.measure_exists_inv_le_le`: Ville's inequality. + +## References + +* [dlP+26] V. H. de la Peña, M. J. Klass, V. H. de la Peña, A. Ly, A. Neishloss and Y. Lin, *The + exact Ville identity*, 2026. +* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in + Statistics 1 (2025), arXiv:2410.23614. +* [Vil39] J. Ville, *Étude critique de la notion de collectif*, Gauthier-Villars, 1939. +* [WR23] H. Wang and A. Ramdas, *The extended Ville's inequality for nonintegrable nonnegative + supermartingales*, arXiv:2304.01163. +-/ + +public section + +open MeasureTheory Filter Set Topology +open scoped ENNReal + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {ℱ : Filtration ℕ mΩ} {S : Set (Measure Ω)} + {P : Measure Ω} {M : ℕ → Ω → ℝ≥0∞} {s : Set Ω} {m N : ℕ} + +namespace IsENNSupermartingale + +/-- **Exact optional stopping in `ℝ≥0∞`.** For an `ℝ≥0∞`-valued supermartingale with finite initial +expectation under a finite measure, a stopping time `m ≤ τ ≤ N` and an `ℱ m`-measurable set `s`, +the integral of `M m` over `s` is that of `M` at `τ` plus that of the decrease from `m` to `τ`, +the value at `τ` of `n ↦ ofReal (A m - A n)` for `A` the predictable part of the real values of +`M`. -/ +theorem setLIntegral_eq_add_stoppedValueLimsup (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) + (hmτ : ∀ ω, (m : WithTop ℕ) ≤ τ ω) (hτN : ∀ ω, τ ω ≤ N) (hs : MeasurableSet[ℱ m] s) : + ∫⁻ ω in s, M m ω ∂P = ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P + + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - + predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) τ ω ∂P := by + set g : ℕ → Ω → ℝ := fun n ω ↦ (M n ω).toReal + set A := predictablePart g ℱ P + have hsup : Supermartingale g ℱ P := hM.supermartingale_toReal hP h0 + have hA_int (n : ℕ) : Integrable (A n) P := + integrable_finsetSum' _ fun _ _ ↦ integrable_condExp + have hτN' (ω : Ω) : τ ω ≤ (N : ℕ) := by simpa using hτN ω + have hτ_top (ω : Ω) : τ ω ≠ ⊤ := ne_top_of_le_ne_top WithTop.coe_ne_top (hτN' ω) + -- The untopped value of `τ` is between `m` and `N`. + have hτ_ge (ω : Ω) : m ≤ (τ ω).untopA := + (WithTop.le_untopA_iff (hτ_top ω)).2 (by simpa using hmτ ω) + have hint_g : Integrable (stoppedValue g τ) P := integrable_stoppedValue ℕ hτ hsup.integrable hτN' + have hint_A : Integrable (stoppedValue A τ) P := integrable_stoppedValue ℕ hτ hA_int hτN' + -- The real identity of the Doob decomposition between the constant time `m` and `τ`. + have hreal := setIntegral_stoppedValue_sub_eq_predictablePart hsup.integrable + (isStoppingTime_const ℱ m) hτ (fun ω ↦ by simpa using hmτ ω) hτN' + (by rwa [IsStoppingTime.measurableSpace_const]) + simp only [stoppedValue_const] at hreal + rw [integral_sub hint_g.integrableOn (hsup.integrable m).integrableOn, + integral_sub hint_A.integrableOn (hA_int m).integrableOn] at hreal + have hfin := hM.ae_lt_top hP h0 + -- Each lower integral is the `ofReal` of the integral of its real counterpart. + have h₁ : ∫⁻ ω in s, M m ω ∂P = ENNReal.ofReal (∫ ω in s, g m ω ∂P) := by + rw [ofReal_integral_eq_lintegral_ofReal (hsup.integrable m).integrableOn + (ae_of_all _ fun _ ↦ ENNReal.toReal_nonneg)] + refine lintegral_congr_ae (ae_restrict_of_ae ?_) + filter_upwards [hfin] with ω hω using (ENNReal.ofReal_toReal (hω m).ne).symm + have h₂ : ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P = + ENNReal.ofReal (∫ ω in s, stoppedValue g τ ω ∂P) := by + rw [ofReal_integral_eq_lintegral_ofReal hint_g.integrableOn + (ae_of_all _ fun _ ↦ by simp [stoppedValue, g])] + refine lintegral_congr_ae (ae_restrict_of_ae ?_) + filter_upwards [hfin] with ω hω + rw [stoppedValueLimsup_eq_stoppedValue (hτ_top ω)] + simp only [stoppedValue, g] + exact (ENNReal.ofReal_toReal (hω _).ne).symm + -- The predictable part of a supermartingale is antitone, and `m ≤ τ`. + have hnonneg : 0 ≤ᵐ[P.restrict s] fun ω ↦ A m ω - stoppedValue A τ ω := by + refine ae_restrict_of_ae ?_ + filter_upwards [hsup.antitone_predictablePart] with ω hω + exact sub_nonneg.2 (hω (hτ_ge ω)) + have h₃ : ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal (A m ω - A n ω)) τ ω ∂P = + ENNReal.ofReal (∫ ω in s, A m ω - stoppedValue A τ ω ∂P) := by + rw [ofReal_integral_eq_lintegral_ofReal (f := fun ω ↦ A m ω - stoppedValue A τ ω) + ((hA_int m).sub hint_A).integrableOn hnonneg] + refine lintegral_congr fun ω ↦ ?_ + rw [stoppedValueLimsup_eq_stoppedValue (hτ_top ω)] + simp [stoppedValue] + rw [h₁, h₂, h₃, ← ENNReal.ofReal_add (integral_nonneg fun ω ↦ by simp [stoppedValue, g]) + (setIntegral_nonneg_of_ae_restrict hnonneg)] + congr 1 + rw [integral_sub (hA_int m).integrableOn hint_A.integrableOn] + linarith + +/-- Splitting at the horizon: for a stopping time `T ≥ m` and `N ≥ m`, the value at `min T N` is +the value at `T` on `{T ≤ N}` and `M N` on `{N < T}`. -/ +private theorem setLIntegral_eq_add_add_of_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {T : Ω → WithTop ℕ} (hT : IsStoppingTime ℱ T) + (hmT : ∀ ω, (m : WithTop ℕ) ≤ T ω) (hmN : m ≤ N) (hs : MeasurableSet[ℱ m] s) : + ∫⁻ ω in s, M m ω ∂P = ∫⁻ ω in s ∩ {ω | T ω ≤ N}, stoppedValueLimsup M T ω ∂P + + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - + predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) (fun ω ↦ min (T ω) N) ω ∂P + + ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < T ω}, M N ω ∂P := by + have hs' : MeasurableSet s := ℱ.le m _ hs + have hTN : MeasurableSet {ω | T ω ≤ N} := ℱ.le N _ (hT.measurableSet_le_natCast N) + have hNT : MeasurableSet {ω | (N : WithTop ℕ) < T ω} := + ℱ.le N _ (hT.measurableSet_natCast_lt N) + have hdiff : s \ {ω | T ω ≤ N} = s ∩ {ω | (N : WithTop ℕ) < T ω} := by + ext ω + simp [not_le] + rw [hM.setLIntegral_eq_add_stoppedValueLimsup hP h0 (hT.min_natCast N) + (fun ω ↦ le_min (hmT ω) (by exact_mod_cast hmN)) (fun ω ↦ min_le_right _ _) hs, + ← lintegral_inter_add_sdiff _ s hTN, hdiff, + setLIntegral_congr_fun (f := stoppedValueLimsup M fun ω ↦ min (T ω) N) + (g := stoppedValueLimsup M T) (hs'.inter hTN) + (fun ω hω ↦ stoppedValueLimsup_congr (min_eq_left hω.2)), + setLIntegral_congr_fun (f := stoppedValueLimsup M fun ω ↦ min (T ω) N) (g := M N) + (hs'.inter hNT) (fun ω hω ↦ stoppedValueLimsup_of_eq_natCast (min_eq_right hω.2.le)), + add_right_comm] + +/-- A hitting time after `m` is at least `m`, at the cast `(m : WithTop ℕ)`. -/ +private theorem natCast_le_hittingAfter (t : Set ℝ≥0∞) (ω : Ω) : + (m : WithTop ℕ) ≤ hittingAfter M t m ω := by + simpa using le_hittingAfter (u := M) (s := t) (n := m) ω + +/-- On a set where the hitting time `T` of `[b, ∞]` is finite, `M` at `T` is `b` plus the +overshoot `M T - b`. -/ +private theorem setLIntegral_stoppedValueLimsup_hittingAfter (b : ℝ≥0∞) {t : Set Ω} + (ht : MeasurableSet t) (htT : t ⊆ {ω | hittingAfter M (Ici b) m ω ≠ ⊤}) : + ∫⁻ ω in t, stoppedValueLimsup M (hittingAfter M (Ici b) m) ω ∂P = + b * P t + ∫⁻ ω in t, (stoppedValueLimsup M (hittingAfter M (Ici b) m) ω - b) ∂P := by + rw [← setLIntegral_const, ← lintegral_add_left measurable_const] + refine setLIntegral_congr_fun ht fun ω hω ↦ ?_ + have hb : b ≤ stoppedValueLimsup M (hittingAfter M (Ici b) m) ω := by + rw [stoppedValueLimsup_eq_stoppedValue (htT hω)] + exact hittingAfter_mem_set_of_ne_top (htT hω) + exact (add_tsub_cancel_of_le hb).symm + +/-- **The exact Ville identity** [dlP+26, Theorem 1], from time `m` on an `ℱ m`-measurable set +`s`. For an `ℝ≥0∞`-valued supermartingale with finite initial expectation under a finite +measure, a level `b`, the first time `T` after `m` at which `b ≤ M n`, and a horizon `N ≥ m`, the +integral of `M m` over `s` is the sum of the level reached `b * P (s ∩ {T ≤ N})`, the overshoot +`M T - b` over `s ∩ {T ≤ N}`, the predictable decrease up to `T ∧ N` (with `A` the predictable +part of the real values of `M`, the sum over `m ≤ k < T ∧ N` of `M k - E[M (k + 1) | ℱ k]`) and the +remainder `M N` over `s ∩ {N < T}`. -/ +theorem setLIntegral_eq_exact_ville_horizon (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (b : ℝ≥0∞) (hmN : m ≤ N) + (hs : MeasurableSet[ℱ m] s) : + ∫⁻ ω in s, M m ω ∂P = + b * P (s ∩ {ω | hittingAfter M (Ici b) m ω ≤ N}) + + ∫⁻ ω in s ∩ {ω | hittingAfter M (Ici b) m ω ≤ N}, + (stoppedValueLimsup M (hittingAfter M (Ici b) m) ω - b) ∂P + + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - + predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) + (fun ω ↦ min (hittingAfter M (Ici b) m ω) N) ω ∂P + + ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P := by + have hT : IsStoppingTime ℱ (hittingAfter M (Ici b) m) := + hM.adapted.isStoppingTime_hittingAfter measurableSet_Ici + rw [hM.setLIntegral_eq_add_add_of_le hP h0 hT (natCast_le_hittingAfter (Ici b)) + hmN hs, + setLIntegral_stoppedValueLimsup_hittingAfter b + ((ℱ.le m _ hs).inter (ℱ.le N _ (hT.measurableSet_le_natCast N))) + (fun ω hω ↦ ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hω.2)] + +/-- **The exact Ville identity** [dlP+26, Theorem 1]. For an `ℝ≥0∞`-valued supermartingale with +finite initial expectation under a finite measure, a level `b`, the first time `T` at which +`b ≤ M n`, and a horizon `N`, the initial expectation is the sum of the level reached +`b * P {T ≤ N}`, the overshoot `M T - b` over `{T ≤ N}`, the predictable decrease +`-A (T ∧ N)` (with `A` the predictable part of the real values of `M`, the sum over `k < T ∧ N` +of `M k - E[M (k + 1) | ℱ k]`) and the remainder `M N` over `{N < T}`. -/ +theorem lintegral_zero_eq_exact_ville_horizon (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (b : ℝ≥0∞) (N : ℕ) : + ∫⁻ ω, M 0 ω ∂P = + b * P {ω | hittingAfter M (Ici b) 0 ω ≤ N} + + ∫⁻ ω in {ω | hittingAfter M (Ici b) 0 ω ≤ N}, + (stoppedValueLimsup M (hittingAfter M (Ici b) 0) ω - b) ∂P + + ∫⁻ ω, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (-predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) + (fun ω ↦ min (hittingAfter M (Ici b) 0 ω) N) ω ∂P + + ∫⁻ ω in {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) 0 ω}, M N ω ∂P := by + simpa using hM.setLIntegral_eq_exact_ville_horizon hP h0 b N.zero_le MeasurableSet.univ + +/-- The remainders `∫⁻ ω in s ∩ {N < T}, M N ω ∂P` are nonincreasing after time `m`, hence +converge to their infimum over `N ≥ m`. -/ +private theorem tendsto_setLIntegral_natCast_lt (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + {T : Ω → WithTop ℕ} (hT : IsStoppingTime ℱ T) (hs : MeasurableSet[ℱ m] s) : + Tendsto (fun N : ℕ ↦ ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < T ω}, M N ω ∂P) atTop + (𝓝 (⨅ N ≥ m, ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < T ω}, M N ω ∂P)) := by + set r : ℕ → ℝ≥0∞ := fun N ↦ ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < T ω}, M N ω ∂P + have hr_succ (N : ℕ) (hN : m ≤ N) : r (N + 1) ≤ r N := by + refine (lintegral_mono_set (inter_subset_inter_right _ fun ω hω ↦ ?_)).trans + (hM.setLIntegral_succ_le P hP N _ ((ℱ.mono hN _ hs).inter (hT.measurableSet_natCast_lt N))) + rw [mem_ofPred_eq] at hω ⊢ + exact lt_trans (by exact_mod_cast N.lt_succ_self) hω + rw [iInf_ge_eq_iInf_nat_add, ← tendsto_add_atTop_iff_nat m] + refine tendsto_atTop_iInf (antitone_nat_of_succ_le fun k ↦ ?_) + simpa [add_right_comm] using hr_succ (k + m) (Nat.le_add_left m k) + +/-- Letting the horizon tend to infinity: for a stopping time `T ≥ m`, the integral of `M m` over +`s` is that of `M` at `T` over `s ∩ {T ≠ ⊤}`, plus the decrease up to `T`, plus the limit of the +remainders. -/ +private theorem setLIntegral_eq_add_add_iInf (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {T : Ω → WithTop ℕ} (hT : IsStoppingTime ℱ T) + (hmT : ∀ ω, (m : WithTop ℕ) ≤ T ω) (hs : MeasurableSet[ℱ m] s) : + ∫⁻ ω in s, M m ω ∂P = ∫⁻ ω in s ∩ {ω | T ω ≠ ⊤}, stoppedValueLimsup M T ω ∂P + + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - + predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) T ω ∂P + + ⨅ N ≥ m, ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < T ω}, M N ω ∂P := by + set A := predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P + set D : ℕ → Ω → ℝ≥0∞ := fun n ω ↦ ENNReal.ofReal (A m ω - A n ω) + have hs' : MeasurableSet s := ℱ.le m _ hs + -- The integrals of `M T` over `s ∩ {T ≤ N}` increase to its integral over `s ∩ {T ≠ ⊤}`. + have ha : Tendsto (fun N : ℕ ↦ ∫⁻ ω in s ∩ {ω | T ω ≤ N}, stoppedValueLimsup M T ω ∂P) atTop + (𝓝 (∫⁻ ω in s ∩ {ω | T ω ≠ ⊤}, stoppedValueLimsup M T ω ∂P)) := by + have hmeas (N : ℕ) : MeasurableSet (s ∩ {ω | T ω ≤ N}) := + hs'.inter (ℱ.le N _ (hT.measurableSet_le_natCast N)) + have hU : ⋃ N : ℕ, s ∩ {ω | T ω ≤ N} = s ∩ {ω | T ω ≠ ⊤} := by + rw [← inter_iUnion] + congr 1 + ext ω + simp only [mem_iUnion, mem_ofPred_eq] + refine ⟨fun ⟨N, hN⟩ ↦ ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hN, fun h ↦ ?_⟩ + obtain ⟨t, ht⟩ := WithTop.ne_top_iff_exists.1 h + exact ⟨t, by simp [← ht]⟩ + simp_rw [← withDensity_apply _ (hmeas _)] + rw [← withDensity_apply _ (hU ▸ MeasurableSet.iUnion hmeas), ← hU] + exact tendsto_measure_iUnion_atTop fun N N' h ↦ + inter_subset_inter_right _ fun ω (hω : T ω ≤ N) ↦ hω.trans (by exact_mod_cast h) + -- The decrease process is almost surely nondecreasing, and its values at `min T N` increase to + -- its value at `T`. + have hDmeas (n : ℕ) : Measurable (D n) := + ENNReal.measurable_ofReal.comp + ((((stronglyAdapted_predictablePart' m).mono (ℱ.le m)).measurable).sub + (((stronglyAdapted_predictablePart' n).mono (ℱ.le n)).measurable)) + have hDmono : ∀ᵐ ω ∂P, Monotone (D · ω) := by + filter_upwards [(hM.supermartingale_toReal hP h0).antitone_predictablePart] with ω hω + exact fun n n' h ↦ ENNReal.ofReal_le_ofReal (sub_le_sub_left (hω h) _) + have hd : Tendsto (fun N : ℕ ↦ ∫⁻ ω in s, stoppedValueLimsup D (fun ω ↦ min (T ω) N) ω ∂P) + atTop (𝓝 (∫⁻ ω in s, stoppedValueLimsup D T ω ∂P)) := by + have hmin_top (ω : Ω) (N : ℕ) : min (T ω) N ≠ ⊤ := + ne_top_of_le_ne_top (WithTop.natCast_ne_top N) (min_le_right _ _) + refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ (measurable_stoppedValueLimsup hDmeas + (hT.min_natCast N).measurable').aemeasurable) (ae_restrict_of_ae ?_) (ae_restrict_of_ae ?_) + · filter_upwards [hDmono] with ω hω N N' h + dsimp only + rw [stoppedValueLimsup_eq_stoppedValue (τ := fun ω ↦ min (T ω) N) (hmin_top ω N), + stoppedValueLimsup_eq_stoppedValue (τ := fun ω ↦ min (T ω) N') (hmin_top ω N')] + exact hω (WithTop.untopA_mono (hmin_top ω N') (min_le_min_left _ (by exact_mod_cast h))) + · filter_upwards [hDmono] with ω hω + refine tendsto_stoppedValueLimsup_min ?_ + have h := tendsto_atTop_iSup hω + rwa [h.limsup_eq] + have hr := hM.tendsto_setLIntegral_natCast_lt hP hT hs + -- The finite-horizon identities pass to the limit. + refine tendsto_nhds_unique (tendsto_const_nhds.congr' ?_) ((ha.add hd).add hr) + filter_upwards [eventually_ge_atTop m] with N hN + exact hM.setLIntegral_eq_add_add_of_le hP h0 hT hmT hN hs + +/-- **The exact Ville identity without horizon** [dlP+26, Theorem 4], from time `m` on an +`ℱ m`-measurable set `s`. For an `ℝ≥0∞`-valued supermartingale with finite initial expectation +under a finite measure, a level `b` and the first time `T` after `m` at which `b ≤ M n`, the +integral of `M m` over `s` is the sum of the level reached `b * P (s ∩ {T < ∞})`, the overshoot +`M T - b` over `s ∩ {T < ∞}`, the predictable decrease up to `T`, and the limit +`⨅ N ≥ m, ∫⁻ ω in s ∩ {N < T}, M N ω ∂P` of the remainders. -/ +theorem setLIntegral_eq_exact_ville (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (b : ℝ≥0∞) (hs : MeasurableSet[ℱ m] s) : + ∫⁻ ω in s, M m ω ∂P = + b * P (s ∩ {ω | hittingAfter M (Ici b) m ω ≠ ⊤}) + + ∫⁻ ω in s ∩ {ω | hittingAfter M (Ici b) m ω ≠ ⊤}, + (stoppedValueLimsup M (hittingAfter M (Ici b) m) ω - b) ∂P + + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - + predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) (hittingAfter M (Ici b) m) ω ∂P + + ⨅ N ≥ m, ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P := by + have hT : IsStoppingTime ℱ (hittingAfter M (Ici b) m) := + hM.adapted.isStoppingTime_hittingAfter measurableSet_Ici + have hTtop : MeasurableSet {ω | hittingAfter M (Ici b) m ω ≠ ⊤} := by + exact (hT.measurable' (measurableSet_singleton ⊤)).compl + rw [hM.setLIntegral_eq_add_add_iInf hP h0 hT (natCast_le_hittingAfter (Ici b)) hs, + setLIntegral_stoppedValueLimsup_hittingAfter b ((ℱ.le m _ hs).inter hTtop) + inter_subset_right] + +/-- **The exact Ville identity without horizon** [dlP+26, Theorem 4]. For an `ℝ≥0∞`-valued +supermartingale with finite initial expectation under a finite measure, a level `b` and the +first time `T` at which `b ≤ M n`, the initial expectation is the sum of the level reached +`b * P {T < ∞}`, the overshoot `M T - b` over `{T < ∞}`, the predictable decrease `-A T` (with `A` +the predictable part of the real values of `M`), and the limit `⨅ N, ∫⁻ ω in {N < T}, M N ω ∂P` of +the remainders. -/ +theorem lintegral_zero_eq_exact_ville (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (b : ℝ≥0∞) : + ∫⁻ ω, M 0 ω ∂P = + b * P {ω | hittingAfter M (Ici b) 0 ω ≠ ⊤} + + ∫⁻ ω in {ω | hittingAfter M (Ici b) 0 ω ≠ ⊤}, + (stoppedValueLimsup M (hittingAfter M (Ici b) 0) ω - b) ∂P + + ∫⁻ ω, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (-predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) (hittingAfter M (Ici b) 0) ω ∂P + + ⨅ N : ℕ, ∫⁻ ω in {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) 0 ω}, M N ω ∂P := by + simpa using hM.setLIntegral_eq_exact_ville (m := 0) hP h0 b MeasurableSet.univ + +/-- **Equality in Ville's inequality.** For an `ℝ≥0∞`-valued supermartingale with finite initial +expectation under a finite measure, a level `b` and the first time `T` after `m` at which +`b ≤ M n`, the bound `b * P (s ∩ {T < ∞}) ≤ ∫⁻ ω in s, M m ω ∂P` is an equality exactly when the +overshoot, the predictable decrease and the remainder of the exact Ville identity vanish. -/ +theorem mul_measure_inter_eq_setLIntegral_iff (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (b : ℝ≥0∞) (hs : MeasurableSet[ℱ m] s) : + b * P (s ∩ {ω | hittingAfter M (Ici b) m ω ≠ ⊤}) = ∫⁻ ω in s, M m ω ∂P ↔ + ∫⁻ ω in s ∩ {ω | hittingAfter M (Ici b) m ω ≠ ⊤}, + (stoppedValueLimsup M (hittingAfter M (Ici b) m) ω - b) ∂P = 0 ∧ + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal + (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - + predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) (hittingAfter M (Ici b) m) ω ∂P = 0 ∧ + ⨅ N ≥ m, ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P = 0 := by + have hfin : ∫⁻ ω in s, M m ω ∂P ≠ ∞ := + ((setLIntegral_le_lintegral s _).trans (hM.lintegral_le hP m.zero_le)).trans_lt h0.lt_top |>.ne + rw [hM.setLIntegral_eq_exact_ville hP h0 b hs, add_assoc, add_assoc] at hfin ⊢ + conv_lhs => lhs; rw [← add_zero (b * _)] + rw [ENNReal.add_right_inj (ENNReal.add_ne_top.1 hfin).1, eq_comm, add_eq_zero, add_eq_zero] + +/-- Ville's maximal inequality from time `m`, for an `ℝ≥0∞`-valued supermartingale with finite +initial expectation: the exact Ville identity without its overshoot, decrease and remainder. -/ +private theorem mul_measure_inter_exists_le_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (b : ℝ≥0∞) (hs : MeasurableSet[ℱ m] s) : + b * P (s ∩ {ω | ∃ n ≥ m, b ≤ M n ω}) ≤ ∫⁻ ω in s, M m ω ∂P := by + have hset : {ω | ∃ n ≥ m, b ≤ M n ω} = {ω | hittingAfter M (Ici b) m ω ≠ ⊤} := by + ext ω + simp [hittingAfter_eq_top_iff] + rw [hset, hM.setLIntegral_eq_exact_ville hP h0 b hs, add_assoc, add_assoc] + exact le_self_add + +/-- Ville's maximal inequality from time `m` on an `ℱ m`-measurable set `u` on which `M m ≤ c`, +for every `ℝ≥0∞`-valued supermartingale under a finite measure, with no integrability condition: +the process equal to `c` before time `m` and to `M` on `u` from time `m` on has finite initial +expectation. -/ +private theorem mul_measure_inter_exists_le_le_of_le (hM : IsENNSupermartingale M ℱ S) + (hP : P ∈ S) [IsFiniteMeasure P] {c : ℝ≥0∞} (hc : c ≠ ∞) {u : Set Ω} + (hu : MeasurableSet[ℱ m] u) (hMu : ∀ ω ∈ u, M m ω ≤ c) : + c * P (u ∩ {ω | ∃ n ≥ m, c ≤ M n ω}) ≤ ∫⁻ ω in u, M m ω ∂P := by + set M' : ℕ → Ω → ℝ≥0∞ := fun n ↦ if n < m then fun _ ↦ c else u.indicator (M n) + have hM'_le (n : ℕ) (hn : n ≤ m) (ω : Ω) : M' n ω ≤ c := by + rcases hn.lt_or_eq with hn | rfl + · simp [M', hn] + · by_cases hω : ω ∈ u + · simpa [M', indicator_of_mem hω] using hMu ω hω + · simp [M', indicator_of_notMem hω] + have hM' : IsENNSupermartingale M' ℱ {P} := by + refine ⟨fun n ↦ ?_, fun Q hQ n v hv ↦ ?_⟩ + · by_cases hn : n < m + · simp [M', hn] + · simpa [M', hn] using (hM.adapted n).indicator (ℱ.mono (not_lt.1 hn) _ hu) + rw [mem_singleton_iff] at hQ + subst hQ + by_cases hnm : n < m + · calc ∫⁻ ω in v, M' (n + 1) ω ∂Q ≤ ∫⁻ ω in v, c ∂Q := + lintegral_mono fun ω ↦ hM'_le (n + 1) hnm ω + _ = ∫⁻ ω in v, M' n ω ∂Q := by simp [M', hnm] + · have hn : ¬n + 1 < m := by omega + simp only [M', hn, hnm, ite_false] + rw [setLIntegral_indicator (ℱ.le m _ hu), setLIntegral_indicator (ℱ.le m _ hu)] + exact hM.setLIntegral_succ_le Q hP n _ ((ℱ.mono (not_lt.1 hnm) _ hu).inter hv) + have h0' : ∫⁻ ω, M' 0 ω ∂P ≠ ∞ := by + refine ((lintegral_mono (hM'_le 0 m.zero_le)).trans_lt ?_).ne + rw [lintegral_const] + exact ENNReal.mul_lt_top hc.lt_top (measure_lt_top P univ) + -- On `u`, `M'` agrees with `M` from time `m` on. + have hE : u ∩ {ω | ∃ n ≥ m, c ≤ M' n ω} = u ∩ {ω | ∃ n ≥ m, c ≤ M n ω} := by + ext ω + simp only [mem_inter_iff, mem_ofPred_eq] + refine and_congr_right fun hω ↦ exists_congr fun n ↦ and_congr_right fun hn ↦ ?_ + simp [M', not_lt.2 hn, indicator_of_mem hω] + have hM'm : ∫⁻ ω in u, M' m ω ∂P = ∫⁻ ω in u, M m ω ∂P := by + simp only [M', lt_irrefl, ite_false] + rw [setLIntegral_indicator (ℱ.le m _ hu), inter_self] + simpa only [hE, hM'm] using hM'.mul_measure_inter_exists_le_le (mem_singleton P) h0' c hu + +/-- **The extended Ville inequality** [WR23, Theorem 4.1]. For every `ℝ≥0∞`-valued +supermartingale under a finite measure, with no integrability condition, every time `m`, every +`ℱ m`-measurable set `s` and every level `0 < c < ∞`, +`P (s ∩ {∃ n ≥ m, c ≤ M n}) ≤ (∫⁻ ω in s, min (M m ω) c ∂P) / c`. -/ +theorem measure_inter_exists_le_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] {c : ℝ≥0∞} (hc0 : c ≠ 0) (hc : c ≠ ∞) (hs : MeasurableSet[ℱ m] s) : + P (s ∩ {ω | ∃ n ≥ m, c ≤ M n ω}) ≤ (∫⁻ ω in s, min (M m ω) c ∂P) / c := by + rw [ENNReal.le_div_iff_mul_le (.inl hc0) (.inl hc), mul_comm] + set E := {ω | ∃ n ≥ m, c ≤ M n ω} + set t := {ω | M m ω < c} + have ht : MeasurableSet[ℱ m] t := measurableSet_lt (hM.adapted m) measurable_const + have hmax := hM.mul_measure_inter_exists_le_le_of_le hP hc (hs.inter ht) fun ω hω ↦ hω.2.le + -- On `s \ t`, `c ≤ M m`, so that the event holds at time `m` and `min (M m) c = c`. + have hs' : MeasurableSet s := ℱ.le m _ hs + have ht' : MeasurableSet t := ℱ.le m _ ht + calc c * P (s ∩ E) ≤ c * (P (s ∩ t ∩ E) + P (s \ t)) := by + refine mul_le_mul_right ((measure_mono fun ω hω ↦ ?_).trans (measure_union_le _ _)) c + by_cases h : ω ∈ t + · exact Or.inl ⟨⟨hω.1, h⟩, hω.2⟩ + · exact Or.inr ⟨hω.1, h⟩ + _ = c * P (s ∩ t ∩ E) + ∫⁻ ω in s \ t, c ∂P := by rw [mul_add, setLIntegral_const, mul_comm] + _ ≤ ∫⁻ ω in s ∩ t, M m ω ∂P + ∫⁻ ω in s \ t, c ∂P := by gcongr + _ = ∫⁻ ω in s ∩ t, min (M m ω) c ∂P + ∫⁻ ω in s \ t, min (M m ω) c ∂P := by + congr 1 + · exact setLIntegral_congr_fun (hs'.inter ht') fun ω hω ↦ (min_eq_left hω.2.le).symm + · exact setLIntegral_congr_fun (hs'.diff ht') fun ω hω ↦ + (min_eq_right (not_lt.1 hω.2)).symm + _ = ∫⁻ ω in s, min (M m ω) c ∂P := lintegral_inter_add_sdiff _ s ht' + +/-- **Ville's inequality** [Vil39; RW, Fact 7.6]. For every `ℝ≥0∞`-valued supermartingale under a +finite measure, with no integrability condition, and every level `0 < c < ∞`, the probability +that the process ever reaches `c` is at most `(∫⁻ ω, M 0 ω ∂P) / c`. -/ +theorem measure_exists_le_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] + {c : ℝ≥0∞} (hc0 : c ≠ 0) (hc : c ≠ ∞) : + P {ω | ∃ n, c ≤ M n ω} ≤ (∫⁻ ω, M 0 ω ∂P) / c := by + have h := hM.measure_inter_exists_le_le (m := 0) hP hc0 hc MeasurableSet.univ + simp only [univ_inter, ge_iff_le, zero_le, true_and, Measure.restrict_univ] at h + exact h.trans (ENNReal.div_le_div_right (lintegral_mono fun ω ↦ min_le_left _ _) c) + +end IsENNSupermartingale + +namespace IsTestSupermartingale + +/-- **Ville's inequality** for test supermartingales [Vil39; RW, Fact 7.6]: under every finite +member of the null, the probability that the process ever reaches a level `c ≠ 0` is at most +`(∫⁻ ω, M 0 ω ∂P) / c`. -/ +theorem measure_exists_le_le (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] + {c : ℝ≥0∞} (hc0 : c ≠ 0) : + P {ω | ∃ n, c ≤ M n ω} ≤ (∫⁻ ω, M 0 ω ∂P) / c := by + rcases eq_or_ne c ∞ with rfl | hc + · refine (measure_eq_zero_iff_ae_notMem.2 ?_).trans_le zero_le + filter_upwards [hM.ae_lt_top hP] with ω hω ⟨n, hn⟩ + exact (hω n).not_ge hn + · exact hM.toIsENNSupermartingale.measure_exists_le_le hP hc0 hc + +/-- **Ville's inequality** for test supermartingales, at level `α` [RW, Fact 7.6]: under every +finite member of the null, the test that rejects as soon as the process reaches `α⁻¹` has type I +error at most `α`, uniformly over time. -/ +theorem measure_exists_inv_le_le (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) + [IsFiniteMeasure P] (α : ℝ≥0∞) : P {ω | ∃ n, α⁻¹ ≤ M n ω} ≤ α := by + rcases eq_or_ne α ∞ with rfl | hα + · exact le_top + refine (hM.measure_exists_le_le hP (ENNReal.inv_ne_zero.2 hα)).trans ?_ + rw [div_eq_mul_inv, inv_inv] + exact mul_le_of_le_one_left zero_le (hM.lintegral_zero_le P hP) + +end IsTestSupermartingale + +end ProbabilityTheory From 0029b2e331126eebf213067088e0c8d13c853605 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 02:01:38 +0100 Subject: [PATCH 2/6] refactor: cite dlP+26 in full and factor out the monotone-convergence steps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Give the full title and arXiv identifier of [dlP+26]. Extract the monotone convergence of integrals at truncated times as `MeasureTheory.tendsto_lintegral_stoppedValueLimsup_min` in Process/StoppedValue.lean, and the convergence of set integrals over `{T ≤ N}` as a private lemma; use Mathlib's `ofReal_toReal_ae_eq`; drop the redundant `hτN'`; share the stopping-time and `{k < τ}` measurability facts. Co-Authored-By: Claude Code --- .../Probability/Martingale/Centering.lean | 9 +- .../Probability/Martingale/ExactVille.lean | 92 +++++++++---------- .../Probability/Process/StoppedValue.lean | 26 ++++++ 3 files changed, 71 insertions(+), 56 deletions(-) diff --git a/LMLExplore/Probability/Martingale/Centering.lean b/LMLExplore/Probability/Martingale/Centering.lean index ac74f528..0801ac86 100644 --- a/LMLExplore/Probability/Martingale/Centering.lean +++ b/LMLExplore/Probability/Martingale/Centering.lean @@ -51,16 +51,13 @@ theorem setIntegral_stoppedValue_sub_eq_predictablePart [SigmaFiniteFiltration ∫ ω in s, stoppedValue (predictablePart f ℱ μ) τ ω - stoppedValue (predictablePart f ℱ μ) σ ω ∂μ := by -- The set `{σ ≤ k < τ}`, and its intersection with `s`, are `ℱ k`-measurable. + have hgt (k : ℕ) : MeasurableSet[ℱ k] {ω | k < τ ω} := by simpa using hτ.measurableSet_gt k have hmeas' (k : ℕ) : MeasurableSet[ℱ k] {ω | σ ω ≤ k ∧ k < τ ω} := by rw [ofPred_and] - have h₁ : MeasurableSet[ℱ k] {ω | σ ω ≤ k} := by simpa using hσ.measurableSet_le k - have h₂ : MeasurableSet[ℱ k] {ω | k < τ ω} := by simpa using hτ.measurableSet_gt k - exact h₁.inter h₂ + exact (by simpa using hσ.measurableSet_le k : MeasurableSet[ℱ k] {ω | σ ω ≤ k}).inter (hgt k) have hmeas (k : ℕ) : MeasurableSet[ℱ k] (s ∩ {ω | σ ω ≤ k ∧ k < τ ω}) := by - have h₁ : MeasurableSet[ℱ k] (s ∩ {ω | σ ω ≤ k}) := by simpa using hs.2 k - have h₂ : MeasurableSet[ℱ k] {ω | k < τ ω} := by simpa using hτ.measurableSet_gt k rw [ofPred_and, ← Set.inter_assoc] - exact h₁.inter h₂ + exact (by simpa using hs.2 k : MeasurableSet[ℱ k] (s ∩ {ω | σ ω ≤ k})).inter (hgt k) -- Both increments are sums over `k ≤ N` of the increments from `k` to `k + 1` on `{σ ≤ k < τ}`. have hsum (g : ℕ → Ω → E) (ω : Ω) : stoppedValue g τ ω - stoppedValue g σ ω = ∑ k ∈ range (N + 1), {ω | σ ω ≤ k ∧ k < τ ω}.indicator (g (k + 1) - g k) ω := by diff --git a/LMLExplore/Probability/Martingale/ExactVille.lean b/LMLExplore/Probability/Martingale/ExactVille.lean index 3f084712..d56cf8a2 100644 --- a/LMLExplore/Probability/Martingale/ExactVille.lean +++ b/LMLExplore/Probability/Martingale/ExactVille.lean @@ -57,7 +57,7 @@ rejects the null as soon as the evidence exceeds `α⁻¹`. ## References * [dlP+26] V. H. de la Peña, M. J. Klass, V. H. de la Peña, A. Ly, A. Neishloss and Y. Lin, *The - exact Ville identity*, 2026. + exact Ville identity with applications to e-values*, arXiv:2607.04620v2. * [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in Statistics 1 (2025), arXiv:2410.23614. * [Vil39] J. Ville, *Étude critique de la notion de collectif*, Gauthier-Villars, 1939. @@ -94,16 +94,15 @@ theorem setLIntegral_eq_add_stoppedValueLimsup (hM : IsENNSupermartingale M ℱ have hsup : Supermartingale g ℱ P := hM.supermartingale_toReal hP h0 have hA_int (n : ℕ) : Integrable (A n) P := integrable_finsetSum' _ fun _ _ ↦ integrable_condExp - have hτN' (ω : Ω) : τ ω ≤ (N : ℕ) := by simpa using hτN ω - have hτ_top (ω : Ω) : τ ω ≠ ⊤ := ne_top_of_le_ne_top WithTop.coe_ne_top (hτN' ω) + have hτ_top (ω : Ω) : τ ω ≠ ⊤ := ne_top_of_le_ne_top (WithTop.natCast_ne_top N) (hτN ω) -- The untopped value of `τ` is between `m` and `N`. have hτ_ge (ω : Ω) : m ≤ (τ ω).untopA := (WithTop.le_untopA_iff (hτ_top ω)).2 (by simpa using hmτ ω) - have hint_g : Integrable (stoppedValue g τ) P := integrable_stoppedValue ℕ hτ hsup.integrable hτN' - have hint_A : Integrable (stoppedValue A τ) P := integrable_stoppedValue ℕ hτ hA_int hτN' + have hint_g : Integrable (stoppedValue g τ) P := integrable_stoppedValue ℕ hτ hsup.integrable hτN + have hint_A : Integrable (stoppedValue A τ) P := integrable_stoppedValue ℕ hτ hA_int hτN -- The real identity of the Doob decomposition between the constant time `m` and `τ`. have hreal := setIntegral_stoppedValue_sub_eq_predictablePart hsup.integrable - (isStoppingTime_const ℱ m) hτ (fun ω ↦ by simpa using hmτ ω) hτN' + (isStoppingTime_const ℱ m) hτ (fun ω ↦ by simpa using hmτ ω) hτN (by rwa [IsStoppingTime.measurableSpace_const]) simp only [stoppedValue_const] at hreal rw [integral_sub hint_g.integrableOn (hsup.integrable m).integrableOn, @@ -113,17 +112,15 @@ theorem setLIntegral_eq_add_stoppedValueLimsup (hM : IsENNSupermartingale M ℱ have h₁ : ∫⁻ ω in s, M m ω ∂P = ENNReal.ofReal (∫ ω in s, g m ω ∂P) := by rw [ofReal_integral_eq_lintegral_ofReal (hsup.integrable m).integrableOn (ae_of_all _ fun _ ↦ ENNReal.toReal_nonneg)] - refine lintegral_congr_ae (ae_restrict_of_ae ?_) - filter_upwards [hfin] with ω hω using (ENNReal.ofReal_toReal (hω m).ne).symm + exact lintegral_congr_ae + (ae_restrict_of_ae (ofReal_toReal_ae_eq (hfin.mono fun _ h ↦ h m)).symm) have h₂ : ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P = ENNReal.ofReal (∫ ω in s, stoppedValue g τ ω ∂P) := by rw [ofReal_integral_eq_lintegral_ofReal hint_g.integrableOn (ae_of_all _ fun _ ↦ by simp [stoppedValue, g])] - refine lintegral_congr_ae (ae_restrict_of_ae ?_) - filter_upwards [hfin] with ω hω - rw [stoppedValueLimsup_eq_stoppedValue (hτ_top ω)] - simp only [stoppedValue, g] - exact (ENNReal.ofReal_toReal (hω _).ne).symm + rw [funext fun ω ↦ stoppedValueLimsup_eq_stoppedValue (hτ_top ω)] + exact lintegral_congr_ae + (ae_restrict_of_ae (ofReal_toReal_ae_eq (hfin.mono fun _ h ↦ h _)).symm) -- The predictable part of a supermartingale is antitone, and `m ≤ τ`. have hnonneg : 0 ≤ᵐ[P.restrict s] fun ω ↦ A m ω - stoppedValue A τ ω := by refine ae_restrict_of_ae ?_ @@ -169,6 +166,12 @@ private theorem setLIntegral_eq_add_add_of_le (hM : IsENNSupermartingale M ℱ S (hs'.inter hNT) (fun ω hω ↦ stoppedValueLimsup_of_eq_natCast (min_eq_right hω.2.le)), add_right_comm] +/-- The hitting time after `m` of `[b, ∞]` by an `ℝ≥0∞`-valued supermartingale is a stopping +time. -/ +private theorem isStoppingTime_hittingAfter_Ici (hM : IsENNSupermartingale M ℱ S) (b : ℝ≥0∞) : + IsStoppingTime ℱ (hittingAfter M (Ici b) m) := + hM.adapted.isStoppingTime_hittingAfter measurableSet_Ici + /-- A hitting time after `m` is at least `m`, at the cast `(m : WithTop ℕ)`. -/ private theorem natCast_le_hittingAfter (t : Set ℝ≥0∞) (ω : Ω) : (m : WithTop ℕ) ≤ hittingAfter M t m ω := by @@ -206,8 +209,7 @@ theorem setLIntegral_eq_exact_ville_horizon (hM : IsENNSupermartingale M ℱ S) predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) (fun ω ↦ min (hittingAfter M (Ici b) m ω) N) ω ∂P + ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P := by - have hT : IsStoppingTime ℱ (hittingAfter M (Ici b) m) := - hM.adapted.isStoppingTime_hittingAfter measurableSet_Ici + have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b rw [hM.setLIntegral_eq_add_add_of_le hP h0 hT (natCast_le_hittingAfter (Ici b)) hmN hs, setLIntegral_stoppedValueLimsup_hittingAfter b @@ -248,6 +250,26 @@ private theorem tendsto_setLIntegral_natCast_lt (hM : IsENNSupermartingale M ℱ refine tendsto_atTop_iInf (antitone_nat_of_succ_le fun k ↦ ?_) simpa [add_right_comm] using hr_succ (k + m) (Nat.le_add_left m k) +/-- The integrals of `f` over `s ∩ {T ≤ N}` increase to its integral over `s ∩ {T ≠ ⊤}`. -/ +private theorem tendsto_setLIntegral_inter_le_natCast {T : Ω → WithTop ℕ} (f : Ω → ℝ≥0∞) + (hs : MeasurableSet s) (hT : Measurable T) : + Tendsto (fun N : ℕ ↦ ∫⁻ ω in s ∩ {ω | T ω ≤ N}, f ω ∂P) atTop + (𝓝 (∫⁻ ω in s ∩ {ω | T ω ≠ ⊤}, f ω ∂P)) := by + have hmeas (N : ℕ) : MeasurableSet (s ∩ {ω | T ω ≤ N}) := hs.inter (hT measurableSet_Iic) + have hU : ⋃ N : ℕ, s ∩ {ω | T ω ≤ N} = s ∩ {ω | T ω ≠ ⊤} := by + rw [← inter_iUnion] + congr 1 + ext ω + simp only [mem_iUnion, mem_ofPred_eq] + refine ⟨fun ⟨N, hN⟩ ↦ ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hN, fun h ↦ ?_⟩ + obtain ⟨t, ht⟩ := WithTop.ne_top_iff_exists.1 h + exact ⟨t, by simp [← ht]⟩ + -- The set integrals of `f` are the measures of the sets under `P.withDensity f`. + simp_rw [← withDensity_apply _ (hmeas _)] + rw [← withDensity_apply _ (hU ▸ MeasurableSet.iUnion hmeas), ← hU] + exact tendsto_measure_iUnion_atTop fun N N' h ↦ + inter_subset_inter_right _ fun ω (hω : T ω ≤ N) ↦ hω.trans (by exact_mod_cast h) + /-- Letting the horizon tend to infinity: for a stopping time `T ≥ m`, the integral of `M m` over `s` is that of `M` at `T` over `s ∩ {T ≠ ⊤}`, plus the decrease up to `T`, plus the limit of the remainders. -/ @@ -261,24 +283,8 @@ private theorem setLIntegral_eq_add_add_iInf (hM : IsENNSupermartingale M ℱ S) ⨅ N ≥ m, ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < T ω}, M N ω ∂P := by set A := predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P set D : ℕ → Ω → ℝ≥0∞ := fun n ω ↦ ENNReal.ofReal (A m ω - A n ω) - have hs' : MeasurableSet s := ℱ.le m _ hs - -- The integrals of `M T` over `s ∩ {T ≤ N}` increase to its integral over `s ∩ {T ≠ ⊤}`. - have ha : Tendsto (fun N : ℕ ↦ ∫⁻ ω in s ∩ {ω | T ω ≤ N}, stoppedValueLimsup M T ω ∂P) atTop - (𝓝 (∫⁻ ω in s ∩ {ω | T ω ≠ ⊤}, stoppedValueLimsup M T ω ∂P)) := by - have hmeas (N : ℕ) : MeasurableSet (s ∩ {ω | T ω ≤ N}) := - hs'.inter (ℱ.le N _ (hT.measurableSet_le_natCast N)) - have hU : ⋃ N : ℕ, s ∩ {ω | T ω ≤ N} = s ∩ {ω | T ω ≠ ⊤} := by - rw [← inter_iUnion] - congr 1 - ext ω - simp only [mem_iUnion, mem_ofPred_eq] - refine ⟨fun ⟨N, hN⟩ ↦ ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hN, fun h ↦ ?_⟩ - obtain ⟨t, ht⟩ := WithTop.ne_top_iff_exists.1 h - exact ⟨t, by simp [← ht]⟩ - simp_rw [← withDensity_apply _ (hmeas _)] - rw [← withDensity_apply _ (hU ▸ MeasurableSet.iUnion hmeas), ← hU] - exact tendsto_measure_iUnion_atTop fun N N' h ↦ - inter_subset_inter_right _ fun ω (hω : T ω ≤ N) ↦ hω.trans (by exact_mod_cast h) + have ha := tendsto_setLIntegral_inter_le_natCast (P := P) (stoppedValueLimsup M T) + (ℱ.le m _ hs) hT.measurable' -- The decrease process is almost surely nondecreasing, and its values at `min T N` increase to -- its value at `T`. have hDmeas (n : ℕ) : Measurable (D n) := @@ -288,21 +294,8 @@ private theorem setLIntegral_eq_add_add_iInf (hM : IsENNSupermartingale M ℱ S) have hDmono : ∀ᵐ ω ∂P, Monotone (D · ω) := by filter_upwards [(hM.supermartingale_toReal hP h0).antitone_predictablePart] with ω hω exact fun n n' h ↦ ENNReal.ofReal_le_ofReal (sub_le_sub_left (hω h) _) - have hd : Tendsto (fun N : ℕ ↦ ∫⁻ ω in s, stoppedValueLimsup D (fun ω ↦ min (T ω) N) ω ∂P) - atTop (𝓝 (∫⁻ ω in s, stoppedValueLimsup D T ω ∂P)) := by - have hmin_top (ω : Ω) (N : ℕ) : min (T ω) N ≠ ⊤ := - ne_top_of_le_ne_top (WithTop.natCast_ne_top N) (min_le_right _ _) - refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ (measurable_stoppedValueLimsup hDmeas - (hT.min_natCast N).measurable').aemeasurable) (ae_restrict_of_ae ?_) (ae_restrict_of_ae ?_) - · filter_upwards [hDmono] with ω hω N N' h - dsimp only - rw [stoppedValueLimsup_eq_stoppedValue (τ := fun ω ↦ min (T ω) N) (hmin_top ω N), - stoppedValueLimsup_eq_stoppedValue (τ := fun ω ↦ min (T ω) N') (hmin_top ω N')] - exact hω (WithTop.untopA_mono (hmin_top ω N') (min_le_min_left _ (by exact_mod_cast h))) - · filter_upwards [hDmono] with ω hω - refine tendsto_stoppedValueLimsup_min ?_ - have h := tendsto_atTop_iSup hω - rwa [h.limsup_eq] + have hd := tendsto_lintegral_stoppedValueLimsup_min (μ := P.restrict s) hDmeas + (ae_restrict_of_ae hDmono) hT.measurable' have hr := hM.tendsto_setLIntegral_natCast_lt hP hT hs -- The finite-horizon identities pass to the limit. refine tendsto_nhds_unique (tendsto_const_nhds.congr' ?_) ((ha.add hd).add hr) @@ -325,8 +318,7 @@ theorem setLIntegral_eq_exact_ville (hM : IsENNSupermartingale M ℱ S) (hP : P (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P n ω)) (hittingAfter M (Ici b) m) ω ∂P + ⨅ N ≥ m, ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P := by - have hT : IsStoppingTime ℱ (hittingAfter M (Ici b) m) := - hM.adapted.isStoppingTime_hittingAfter measurableSet_Ici + have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b have hTtop : MeasurableSet {ω | hittingAfter M (Ici b) m ω ≠ ⊤} := by exact (hT.measurable' (measurableSet_singleton ⊤)).compl rw [hM.setLIntegral_eq_add_add_iInf hP h0 hT (natCast_le_hittingAfter (Ici b)) hs, diff --git a/LMLExplore/Probability/Process/StoppedValue.lean b/LMLExplore/Probability/Process/StoppedValue.lean index 7b312371..28f2037c 100644 --- a/LMLExplore/Probability/Process/StoppedValue.lean +++ b/LMLExplore/Probability/Process/StoppedValue.lean @@ -35,6 +35,9 @@ 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.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 `τ`. ## References @@ -47,6 +50,7 @@ optional stopping holds at every stopping time with this convention. public section open Filter Topology +open scoped ENNReal namespace MeasureTheory @@ -136,4 +140,26 @@ theorem measurable_stoppedValueLimsup [ConditionallyCompleteLinearOrder β] [Top | coe n => simpa using hu n exact h.comp (measurable_id.prodMk 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 `τ`. -/ +theorem tendsto_lintegral_stoppedValueLimsup_min {mΩ : MeasurableSpace Ω} {μ : Measure Ω} + {u : ℕ → Ω → ℝ≥0∞} (hu : ∀ n, Measurable (u n)) (hmono : ∀ᵐ ω ∂μ, Monotone (u · ω)) + (hτ : Measurable τ) : + Tendsto (fun N : ℕ ↦ ∫⁻ ω, stoppedValueLimsup u (fun ω ↦ min (τ ω) N) ω ∂μ) atTop + (𝓝 (∫⁻ ω, stoppedValueLimsup u τ ω ∂μ)) := by + have hmin_top (ω : Ω) (N : ℕ) : min (τ ω) N ≠ ⊤ := + ne_top_of_le_ne_top (WithTop.natCast_ne_top N) (min_le_right _ _) + refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ (measurable_stoppedValueLimsup hu + ((measurable_of_countable fun t : WithTop ℕ ↦ min t N).comp hτ)).aemeasurable) ?_ ?_ + · filter_upwards [hmono] with ω hω N N' h + dsimp only + rw [stoppedValueLimsup_eq_stoppedValue (τ := fun ω ↦ min (τ ω) N) (hmin_top ω N), + stoppedValueLimsup_eq_stoppedValue (τ := fun ω ↦ min (τ ω) N') (hmin_top ω N')] + exact hω (WithTop.untopA_mono (hmin_top ω N') (min_le_min_left _ (by exact_mod_cast h))) + · filter_upwards [hmono] with ω hω + refine tendsto_stoppedValueLimsup_min ?_ + rw [(tendsto_atTop_iSup hω).limsup_eq] + exact tendsto_atTop_iSup hω + end MeasureTheory From a3ab3446143c1dea97b4cec8fb8aa885ea0d566d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 10:05:00 +0100 Subject: [PATCH 3/6] refactor: make tendsto_setLIntegral_inter_le_natCast public in StoppedValue Co-Authored-By: Claude Code --- .../Probability/Martingale/ExactVille.lean | 22 +------------------ .../Probability/Process/StoppedValue.lean | 22 +++++++++++++++++++ 2 files changed, 23 insertions(+), 21 deletions(-) diff --git a/LMLExplore/Probability/Martingale/ExactVille.lean b/LMLExplore/Probability/Martingale/ExactVille.lean index d56cf8a2..b9c37003 100644 --- a/LMLExplore/Probability/Martingale/ExactVille.lean +++ b/LMLExplore/Probability/Martingale/ExactVille.lean @@ -250,26 +250,6 @@ private theorem tendsto_setLIntegral_natCast_lt (hM : IsENNSupermartingale M ℱ refine tendsto_atTop_iInf (antitone_nat_of_succ_le fun k ↦ ?_) simpa [add_right_comm] using hr_succ (k + m) (Nat.le_add_left m k) -/-- The integrals of `f` over `s ∩ {T ≤ N}` increase to its integral over `s ∩ {T ≠ ⊤}`. -/ -private theorem tendsto_setLIntegral_inter_le_natCast {T : Ω → WithTop ℕ} (f : Ω → ℝ≥0∞) - (hs : MeasurableSet s) (hT : Measurable T) : - Tendsto (fun N : ℕ ↦ ∫⁻ ω in s ∩ {ω | T ω ≤ N}, f ω ∂P) atTop - (𝓝 (∫⁻ ω in s ∩ {ω | T ω ≠ ⊤}, f ω ∂P)) := by - have hmeas (N : ℕ) : MeasurableSet (s ∩ {ω | T ω ≤ N}) := hs.inter (hT measurableSet_Iic) - have hU : ⋃ N : ℕ, s ∩ {ω | T ω ≤ N} = s ∩ {ω | T ω ≠ ⊤} := by - rw [← inter_iUnion] - congr 1 - ext ω - simp only [mem_iUnion, mem_ofPred_eq] - refine ⟨fun ⟨N, hN⟩ ↦ ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hN, fun h ↦ ?_⟩ - obtain ⟨t, ht⟩ := WithTop.ne_top_iff_exists.1 h - exact ⟨t, by simp [← ht]⟩ - -- The set integrals of `f` are the measures of the sets under `P.withDensity f`. - simp_rw [← withDensity_apply _ (hmeas _)] - rw [← withDensity_apply _ (hU ▸ MeasurableSet.iUnion hmeas), ← hU] - exact tendsto_measure_iUnion_atTop fun N N' h ↦ - inter_subset_inter_right _ fun ω (hω : T ω ≤ N) ↦ hω.trans (by exact_mod_cast h) - /-- Letting the horizon tend to infinity: for a stopping time `T ≥ m`, the integral of `M m` over `s` is that of `M` at `T` over `s ∩ {T ≠ ⊤}`, plus the decrease up to `T`, plus the limit of the remainders. -/ @@ -283,7 +263,7 @@ private theorem setLIntegral_eq_add_add_iInf (hM : IsENNSupermartingale M ℱ S) ⨅ N ≥ m, ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < T ω}, M N ω ∂P := by set A := predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P set D : ℕ → Ω → ℝ≥0∞ := fun n ω ↦ ENNReal.ofReal (A m ω - A n ω) - have ha := tendsto_setLIntegral_inter_le_natCast (P := P) (stoppedValueLimsup M T) + have ha := tendsto_setLIntegral_inter_le_natCast (μ := P) (stoppedValueLimsup M T) (ℱ.le m _ hs) hT.measurable' -- The decrease process is almost surely nondecreasing, and its values at `min T N` increase to -- its value at `T`. diff --git a/LMLExplore/Probability/Process/StoppedValue.lean b/LMLExplore/Probability/Process/StoppedValue.lean index 28f2037c..2d272448 100644 --- a/LMLExplore/Probability/Process/StoppedValue.lean +++ b/LMLExplore/Probability/Process/StoppedValue.lean @@ -38,6 +38,8 @@ optional stopping holds at every stopping time with this convention. * `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 `τ`. +* `MeasureTheory.tendsto_setLIntegral_inter_le_natCast`: the integrals of a function over + `s ∩ {τ ≤ N}` increase to its integral over `s ∩ {τ ≠ ⊤}`. ## References @@ -162,4 +164,24 @@ theorem tendsto_lintegral_stoppedValueLimsup_min {mΩ : MeasurableSpace Ω} {μ rw [(tendsto_atTop_iSup hω).limsup_eq] exact tendsto_atTop_iSup hω +/-- The integrals of `f` over `s ∩ {τ ≤ N}` increase to its integral over `s ∩ {τ ≠ ⊤}`. -/ +theorem tendsto_setLIntegral_inter_le_natCast {mΩ : MeasurableSpace Ω} {μ : Measure Ω} + {s : Set Ω} (f : Ω → ℝ≥0∞) (hs : MeasurableSet s) (hτ : Measurable τ) : + Tendsto (fun N : ℕ ↦ ∫⁻ ω in s ∩ {ω | τ ω ≤ N}, f ω ∂μ) atTop + (𝓝 (∫⁻ ω in s ∩ {ω | τ ω ≠ ⊤}, f ω ∂μ)) := by + have hmeas (N : ℕ) : MeasurableSet (s ∩ {ω | τ ω ≤ N}) := hs.inter (hτ measurableSet_Iic) + have hU : ⋃ N : ℕ, s ∩ {ω | τ ω ≤ N} = s ∩ {ω | τ ω ≠ ⊤} := by + rw [← Set.inter_iUnion] + congr 1 + ext ω + simp only [Set.mem_iUnion, Set.mem_ofPred_eq] + refine ⟨fun ⟨N, hN⟩ ↦ ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hN, fun h ↦ ?_⟩ + obtain ⟨t, ht⟩ := WithTop.ne_top_iff_exists.1 h + exact ⟨t, by simp [← ht]⟩ + -- The set integrals of `f` are the measures of the sets under `μ.withDensity f`. + simp_rw [← withDensity_apply _ (hmeas _)] + rw [← withDensity_apply _ (hU ▸ MeasurableSet.iUnion hmeas), ← hU] + exact tendsto_measure_iUnion_atTop fun N N' h ↦ + Set.inter_subset_inter_right _ fun ω (hω : τ ω ≤ N) ↦ hω.trans (by exact_mod_cast h) + end MeasureTheory From 51e2cfc283462105705d6816d7a715e3a9c07214 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 10:36:40 +0100 Subject: [PATCH 4/6] refactor: expose exact optional stopping at general stopping times in ExactVille MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Make the horizon and no-horizon exact optional-stopping identities at an arbitrary stopping time T ≥ m public, as IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup_min and IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup_add_iInf, and list them in the main statements. Co-Authored-By: Claude Code Co-Authored-By: Claude Opus 5.5 --- .../Probability/Martingale/ExactVille.lean | 39 ++++++++++++------- 1 file changed, 26 insertions(+), 13 deletions(-) diff --git a/LMLExplore/Probability/Martingale/ExactVille.lean b/LMLExplore/Probability/Martingale/ExactVille.lean index b9c37003..36b33e6d 100644 --- a/LMLExplore/Probability/Martingale/ExactVille.lean +++ b/LMLExplore/Probability/Martingale/ExactVille.lean @@ -40,6 +40,9 @@ rejects the null as soon as the evidence exceeds `α⁻¹`. * `ProbabilityTheory.IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup`: exact optional stopping at a bounded stopping time `τ ≥ m`: `∫⁻ ω in s, M m ω ∂P` is the integral of `M` at `τ` plus that of the decrease up to `τ`. +* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup_min`, + `ProbabilityTheory.IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup_add_iInf`: exact + optional stopping at any stopping time `T ≥ m`, with a horizon `N` and without one. * `ProbabilityTheory.IsENNSupermartingale.setLIntegral_eq_exact_ville_horizon`, `ProbabilityTheory.IsENNSupermartingale.lintegral_zero_eq_exact_ville_horizon`: the exact Ville identity with a horizon [dlP+26, Theorem 1]. @@ -139,11 +142,16 @@ theorem setLIntegral_eq_add_stoppedValueLimsup (hM : IsENNSupermartingale M ℱ rw [integral_sub (hA_int m).integrableOn hint_A.integrableOn] linarith -/-- Splitting at the horizon: for a stopping time `T ≥ m` and `N ≥ m`, the value at `min T N` is -the value at `T` on `{T ≤ N}` and `M N` on `{N < T}`. -/ -private theorem setLIntegral_eq_add_add_of_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) - [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {T : Ω → WithTop ℕ} (hT : IsStoppingTime ℱ T) - (hmT : ∀ ω, (m : WithTop ℕ) ≤ T ω) (hmN : m ≤ N) (hs : MeasurableSet[ℱ m] s) : +/-- **Exact optional stopping in `ℝ≥0∞` with a horizon.** For an `ℝ≥0∞`-valued supermartingale with +finite initial expectation under a finite measure, a stopping time `T ≥ m`, a horizon `N ≥ m` and +an `ℱ m`-measurable set `s`, the integral of `M m` over `s` is that of `M` at `T` over +`s ∩ {T ≤ N}`, plus that of the decrease from `m` to `T ∧ N` (the value at `T ∧ N` of +`n ↦ ofReal (A m - A n)` for `A` the predictable part of the real values of `M`), plus that of +`M N` over `s ∩ {N < T}`. -/ +theorem setLIntegral_eq_add_stoppedValueLimsup_min (hM : IsENNSupermartingale M ℱ S) + (hP : P ∈ S) [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {T : Ω → WithTop ℕ} + (hT : IsStoppingTime ℱ T) (hmT : ∀ ω, (m : WithTop ℕ) ≤ T ω) (hmN : m ≤ N) + (hs : MeasurableSet[ℱ m] s) : ∫⁻ ω in s, M m ω ∂P = ∫⁻ ω in s ∩ {ω | T ω ≤ N}, stoppedValueLimsup M T ω ∂P + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - @@ -210,7 +218,7 @@ theorem setLIntegral_eq_exact_ville_horizon (hM : IsENNSupermartingale M ℱ S) (fun ω ↦ min (hittingAfter M (Ici b) m ω) N) ω ∂P + ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P := by have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b - rw [hM.setLIntegral_eq_add_add_of_le hP h0 hT (natCast_le_hittingAfter (Ici b)) + rw [hM.setLIntegral_eq_add_stoppedValueLimsup_min hP h0 hT (natCast_le_hittingAfter (Ici b)) hmN hs, setLIntegral_stoppedValueLimsup_hittingAfter b ((ℱ.le m _ hs).inter (ℱ.le N _ (hT.measurableSet_le_natCast N))) @@ -250,12 +258,16 @@ private theorem tendsto_setLIntegral_natCast_lt (hM : IsENNSupermartingale M ℱ refine tendsto_atTop_iInf (antitone_nat_of_succ_le fun k ↦ ?_) simpa [add_right_comm] using hr_succ (k + m) (Nat.le_add_left m k) -/-- Letting the horizon tend to infinity: for a stopping time `T ≥ m`, the integral of `M m` over -`s` is that of `M` at `T` over `s ∩ {T ≠ ⊤}`, plus the decrease up to `T`, plus the limit of the +/-- **Exact optional stopping in `ℝ≥0∞` without horizon.** For an `ℝ≥0∞`-valued supermartingale +with finite initial expectation under a finite measure, a stopping time `T ≥ m` (possibly +infinite) and an `ℱ m`-measurable set `s`, the integral of `M m` over `s` is that of `M` at `T` +over `s ∩ {T ≠ ⊤}`, plus that of the decrease from `m` to `T` (the value at `T`, read with +`MeasureTheory.stoppedValueLimsup`, of `n ↦ ofReal (A m - A n)` for `A` the predictable part of +the real values of `M`), plus the limit `⨅ N ≥ m, ∫⁻ ω in s ∩ {N < T}, M N ω ∂P` of the remainders. -/ -private theorem setLIntegral_eq_add_add_iInf (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) - [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {T : Ω → WithTop ℕ} (hT : IsStoppingTime ℱ T) - (hmT : ∀ ω, (m : WithTop ℕ) ≤ T ω) (hs : MeasurableSet[ℱ m] s) : +theorem setLIntegral_eq_add_stoppedValueLimsup_add_iInf (hM : IsENNSupermartingale M ℱ S) + (hP : P ∈ S) [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {T : Ω → WithTop ℕ} + (hT : IsStoppingTime ℱ T) (hmT : ∀ ω, (m : WithTop ℕ) ≤ T ω) (hs : MeasurableSet[ℱ m] s) : ∫⁻ ω in s, M m ω ∂P = ∫⁻ ω in s ∩ {ω | T ω ≠ ⊤}, stoppedValueLimsup M T ω ∂P + ∫⁻ ω in s, stoppedValueLimsup (fun n ω ↦ ENNReal.ofReal (predictablePart (fun n ω ↦ (M n ω).toReal) ℱ P m ω - @@ -280,7 +292,7 @@ private theorem setLIntegral_eq_add_add_iInf (hM : IsENNSupermartingale M ℱ S) -- The finite-horizon identities pass to the limit. refine tendsto_nhds_unique (tendsto_const_nhds.congr' ?_) ((ha.add hd).add hr) filter_upwards [eventually_ge_atTop m] with N hN - exact hM.setLIntegral_eq_add_add_of_le hP h0 hT hmT hN hs + exact hM.setLIntegral_eq_add_stoppedValueLimsup_min hP h0 hT hmT hN hs /-- **The exact Ville identity without horizon** [dlP+26, Theorem 4], from time `m` on an `ℱ m`-measurable set `s`. For an `ℝ≥0∞`-valued supermartingale with finite initial expectation @@ -301,7 +313,8 @@ theorem setLIntegral_eq_exact_ville (hM : IsENNSupermartingale M ℱ S) (hP : P have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b have hTtop : MeasurableSet {ω | hittingAfter M (Ici b) m ω ≠ ⊤} := by exact (hT.measurable' (measurableSet_singleton ⊤)).compl - rw [hM.setLIntegral_eq_add_add_iInf hP h0 hT (natCast_le_hittingAfter (Ici b)) hs, + rw [hM.setLIntegral_eq_add_stoppedValueLimsup_add_iInf hP h0 hT (natCast_le_hittingAfter (Ici b)) + hs, setLIntegral_stoppedValueLimsup_hittingAfter b ((ℱ.le m _ hs).inter hTtop) inter_subset_right] From 8ca765bfdf9e111437048f18babbaee4cacbf43c Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 11:13:50 +0100 Subject: [PATCH 5/6] refactor: reuse IsENNSupermartingale.inf for the extended Ville inequality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Derive the extended Ville inequality by applying Ville's maximal inequality to `M ⊓ c`, deleting the hand-built auxiliary process. Factor out `MeasureTheory.Supermartingale.condExp_sub_nonpos` and prove `antitone_predictablePart` from it. Make the hitting-time lower bound public as `MeasureTheory.natCast_le_hittingAfter` in a new `Probability/Process/HittingTime.lean`. Co-Authored-By: Claude Code --- .../Probability/Martingale/Centering.lean | 22 +++-- .../Probability/Martingale/ExactVille.lean | 85 +++---------------- .../Probability/Process/HittingTime.lean | 35 ++++++++ 3 files changed, 62 insertions(+), 80 deletions(-) create mode 100644 LMLExplore/Probability/Process/HittingTime.lean diff --git a/LMLExplore/Probability/Martingale/Centering.lean b/LMLExplore/Probability/Martingale/Centering.lean index 0801ac86..7b9fc461 100644 --- a/LMLExplore/Probability/Martingale/Centering.lean +++ b/LMLExplore/Probability/Martingale/Centering.lean @@ -26,6 +26,8 @@ measures the decrease of a supermartingale up to a hitting time. * `MeasureTheory.setIntegral_stoppedValue_sub_eq_predictablePart`: for bounded stopping times `σ ≤ τ` and `s` measurable at `σ`, `∫ ω in s, f τ - f σ ∂μ = ∫ ω in s, predictablePart f τ - predictablePart f σ ∂μ`. +* `MeasureTheory.Supermartingale.condExp_sub_nonpos`: the conditional expectation of an increment + of a supermartingale is almost surely nonpositive. * `MeasureTheory.Supermartingale.antitone_predictablePart`: the predictable part of a supermartingale is almost surely antitone. -/ @@ -74,17 +76,23 @@ theorem setIntegral_stoppedValue_sub_eq_predictablePart [SigmaFiniteFiltration rw [setIntegral_indicator (ℱ.le k _ (hmeas' k)), setIntegral_indicator (ℱ.le k _ (hmeas' k)), setIntegral_condExp (ℱ.le k) (hint k) (hmeas k)] +/-- The conditional expectation of an increment of a supermartingale is almost surely +nonpositive: the supermartingale counterpart of Mathlib's +`MeasureTheory.Submartingale.condExp_sub_nonneg`. -/ +theorem Supermartingale.condExp_sub_nonpos {ι : Type*} [Preorder ι] [PartialOrder E] + [IsOrderedAddMonoid E] {g : ι → Ω → E} {𝒢 : Filtration ι mΩ} (hg : Supermartingale g 𝒢 μ) + {i j : ι} (hij : i ≤ j) : μ[g j - g i | 𝒢 i] ≤ᵐ[μ] 0 := by + have h := hg.neg.condExp_sub_nonneg hij + simp only [Pi.neg_apply, neg_sub_neg] at h + filter_upwards [h, condExp_neg (g i - g j) (𝒢 i)] with ω hω hneg + rw [← neg_sub, hneg, Pi.neg_apply, Pi.zero_apply, neg_nonpos] + exact hω + /-- The predictable part of a supermartingale is almost surely antitone: the supermartingale counterpart of Mathlib's `MeasureTheory.Submartingale.monotone_predictablePart`. -/ theorem Supermartingale.antitone_predictablePart [PartialOrder E] [IsOrderedAddMonoid E] (hf : Supermartingale f ℱ μ) : ∀ᵐ ω ∂μ, Antitone (predictablePart f ℱ μ · ω) := by - have h (n : ℕ) : μ[f (n + 1) - f n | ℱ n] ≤ᵐ[μ] 0 := by - have h' := hf.neg.condExp_sub_nonneg n.le_succ - rw [Pi.neg_apply, Pi.neg_apply, neg_sub_neg, ← neg_sub] at h' - filter_upwards [h', condExp_neg (f (n + 1) - f n) (ℱ n)] with ω hω hneg - rw [hneg, Pi.neg_apply, Pi.zero_apply, neg_nonneg] at hω - exact hω - filter_upwards [ae_all_iff.2 h] with ω hω + filter_upwards [ae_all_iff.2 fun n : ℕ ↦ hf.condExp_sub_nonpos n.le_succ] with ω hω refine antitone_nat_of_succ_le fun n ↦ ?_ rw [predictablePart_add_one, Pi.add_apply, add_le_iff_nonpos_right] exact hω n diff --git a/LMLExplore/Probability/Martingale/ExactVille.lean b/LMLExplore/Probability/Martingale/ExactVille.lean index 36b33e6d..a3390e81 100644 --- a/LMLExplore/Probability/Martingale/ExactVille.lean +++ b/LMLExplore/Probability/Martingale/ExactVille.lean @@ -7,7 +7,7 @@ module public import LMLExplore.Probability.Martingale.Centering public import LMLExplore.Probability.Martingale.OptionalStopping -public import Mathlib.Probability.Process.HittingTime +public import LMLExplore.Probability.Process.HittingTime /-! # The exact Ville identity @@ -180,11 +180,6 @@ private theorem isStoppingTime_hittingAfter_Ici (hM : IsENNSupermartingale M ℱ IsStoppingTime ℱ (hittingAfter M (Ici b) m) := hM.adapted.isStoppingTime_hittingAfter measurableSet_Ici -/-- A hitting time after `m` is at least `m`, at the cast `(m : WithTop ℕ)`. -/ -private theorem natCast_le_hittingAfter (t : Set ℝ≥0∞) (ω : Ω) : - (m : WithTop ℕ) ≤ hittingAfter M t m ω := by - simpa using le_hittingAfter (u := M) (s := t) (n := m) ω - /-- On a set where the hitting time `T` of `[b, ∞]` is finite, `M` at `T` is `b` plus the overshoot `M T - b`. -/ private theorem setLIntegral_stoppedValueLimsup_hittingAfter (b : ℝ≥0∞) {t : Set Ω} @@ -218,7 +213,7 @@ theorem setLIntegral_eq_exact_ville_horizon (hM : IsENNSupermartingale M ℱ S) (fun ω ↦ min (hittingAfter M (Ici b) m ω) N) ω ∂P + ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P := by have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b - rw [hM.setLIntegral_eq_add_stoppedValueLimsup_min hP h0 hT (natCast_le_hittingAfter (Ici b)) + rw [hM.setLIntegral_eq_add_stoppedValueLimsup_min hP h0 hT (natCast_le_hittingAfter) hmN hs, setLIntegral_stoppedValueLimsup_hittingAfter b ((ℱ.le m _ hs).inter (ℱ.le N _ (hT.measurableSet_le_natCast N))) @@ -313,7 +308,7 @@ theorem setLIntegral_eq_exact_ville (hM : IsENNSupermartingale M ℱ S) (hP : P have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b have hTtop : MeasurableSet {ω | hittingAfter M (Ici b) m ω ≠ ⊤} := by exact (hT.measurable' (measurableSet_singleton ⊤)).compl - rw [hM.setLIntegral_eq_add_stoppedValueLimsup_add_iInf hP h0 hT (natCast_le_hittingAfter (Ici b)) + rw [hM.setLIntegral_eq_add_stoppedValueLimsup_add_iInf hP h0 hT (natCast_le_hittingAfter) hs, setLIntegral_stoppedValueLimsup_hittingAfter b ((ℱ.le m _ hs).inter hTtop) inter_subset_right] @@ -365,51 +360,6 @@ private theorem mul_measure_inter_exists_le_le (hM : IsENNSupermartingale M ℱ rw [hset, hM.setLIntegral_eq_exact_ville hP h0 b hs, add_assoc, add_assoc] exact le_self_add -/-- Ville's maximal inequality from time `m` on an `ℱ m`-measurable set `u` on which `M m ≤ c`, -for every `ℝ≥0∞`-valued supermartingale under a finite measure, with no integrability condition: -the process equal to `c` before time `m` and to `M` on `u` from time `m` on has finite initial -expectation. -/ -private theorem mul_measure_inter_exists_le_le_of_le (hM : IsENNSupermartingale M ℱ S) - (hP : P ∈ S) [IsFiniteMeasure P] {c : ℝ≥0∞} (hc : c ≠ ∞) {u : Set Ω} - (hu : MeasurableSet[ℱ m] u) (hMu : ∀ ω ∈ u, M m ω ≤ c) : - c * P (u ∩ {ω | ∃ n ≥ m, c ≤ M n ω}) ≤ ∫⁻ ω in u, M m ω ∂P := by - set M' : ℕ → Ω → ℝ≥0∞ := fun n ↦ if n < m then fun _ ↦ c else u.indicator (M n) - have hM'_le (n : ℕ) (hn : n ≤ m) (ω : Ω) : M' n ω ≤ c := by - rcases hn.lt_or_eq with hn | rfl - · simp [M', hn] - · by_cases hω : ω ∈ u - · simpa [M', indicator_of_mem hω] using hMu ω hω - · simp [M', indicator_of_notMem hω] - have hM' : IsENNSupermartingale M' ℱ {P} := by - refine ⟨fun n ↦ ?_, fun Q hQ n v hv ↦ ?_⟩ - · by_cases hn : n < m - · simp [M', hn] - · simpa [M', hn] using (hM.adapted n).indicator (ℱ.mono (not_lt.1 hn) _ hu) - rw [mem_singleton_iff] at hQ - subst hQ - by_cases hnm : n < m - · calc ∫⁻ ω in v, M' (n + 1) ω ∂Q ≤ ∫⁻ ω in v, c ∂Q := - lintegral_mono fun ω ↦ hM'_le (n + 1) hnm ω - _ = ∫⁻ ω in v, M' n ω ∂Q := by simp [M', hnm] - · have hn : ¬n + 1 < m := by omega - simp only [M', hn, hnm, ite_false] - rw [setLIntegral_indicator (ℱ.le m _ hu), setLIntegral_indicator (ℱ.le m _ hu)] - exact hM.setLIntegral_succ_le Q hP n _ ((ℱ.mono (not_lt.1 hnm) _ hu).inter hv) - have h0' : ∫⁻ ω, M' 0 ω ∂P ≠ ∞ := by - refine ((lintegral_mono (hM'_le 0 m.zero_le)).trans_lt ?_).ne - rw [lintegral_const] - exact ENNReal.mul_lt_top hc.lt_top (measure_lt_top P univ) - -- On `u`, `M'` agrees with `M` from time `m` on. - have hE : u ∩ {ω | ∃ n ≥ m, c ≤ M' n ω} = u ∩ {ω | ∃ n ≥ m, c ≤ M n ω} := by - ext ω - simp only [mem_inter_iff, mem_ofPred_eq] - refine and_congr_right fun hω ↦ exists_congr fun n ↦ and_congr_right fun hn ↦ ?_ - simp [M', not_lt.2 hn, indicator_of_mem hω] - have hM'm : ∫⁻ ω in u, M' m ω ∂P = ∫⁻ ω in u, M m ω ∂P := by - simp only [M', lt_irrefl, ite_false] - rw [setLIntegral_indicator (ℱ.le m _ hu), inter_self] - simpa only [hE, hM'm] using hM'.mul_measure_inter_exists_le_le (mem_singleton P) h0' c hu - /-- **The extended Ville inequality** [WR23, Theorem 4.1]. For every `ℝ≥0∞`-valued supermartingale under a finite measure, with no integrability condition, every time `m`, every `ℱ m`-measurable set `s` and every level `0 < c < ∞`, @@ -417,27 +367,16 @@ supermartingale under a finite measure, with no integrability condition, every t theorem measure_inter_exists_le_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] {c : ℝ≥0∞} (hc0 : c ≠ 0) (hc : c ≠ ∞) (hs : MeasurableSet[ℱ m] s) : P (s ∩ {ω | ∃ n ≥ m, c ≤ M n ω}) ≤ (∫⁻ ω in s, min (M m ω) c ∂P) / c := by + -- `M` capped at `c` is a supermartingale with finite initial expectation reaching `c` exactly + -- when `M` does. + have hMc := hM.inf (M := M) (N := fun _ _ ↦ c) ⟨fun _ ↦ measurable_const, fun _ _ _ _ _ ↦ le_rfl⟩ + have h0 : ∫⁻ ω, (M ⊓ fun _ _ ↦ c) 0 ω ∂P ≠ ∞ := by + refine ((lintegral_mono fun ω ↦ inf_le_right).trans_lt ?_).ne + rw [lintegral_const] + exact ENNReal.mul_lt_top hc.lt_top (measure_lt_top P univ) rw [ENNReal.le_div_iff_mul_le (.inl hc0) (.inl hc), mul_comm] - set E := {ω | ∃ n ≥ m, c ≤ M n ω} - set t := {ω | M m ω < c} - have ht : MeasurableSet[ℱ m] t := measurableSet_lt (hM.adapted m) measurable_const - have hmax := hM.mul_measure_inter_exists_le_le_of_le hP hc (hs.inter ht) fun ω hω ↦ hω.2.le - -- On `s \ t`, `c ≤ M m`, so that the event holds at time `m` and `min (M m) c = c`. - have hs' : MeasurableSet s := ℱ.le m _ hs - have ht' : MeasurableSet t := ℱ.le m _ ht - calc c * P (s ∩ E) ≤ c * (P (s ∩ t ∩ E) + P (s \ t)) := by - refine mul_le_mul_right ((measure_mono fun ω hω ↦ ?_).trans (measure_union_le _ _)) c - by_cases h : ω ∈ t - · exact Or.inl ⟨⟨hω.1, h⟩, hω.2⟩ - · exact Or.inr ⟨hω.1, h⟩ - _ = c * P (s ∩ t ∩ E) + ∫⁻ ω in s \ t, c ∂P := by rw [mul_add, setLIntegral_const, mul_comm] - _ ≤ ∫⁻ ω in s ∩ t, M m ω ∂P + ∫⁻ ω in s \ t, c ∂P := by gcongr - _ = ∫⁻ ω in s ∩ t, min (M m ω) c ∂P + ∫⁻ ω in s \ t, min (M m ω) c ∂P := by - congr 1 - · exact setLIntegral_congr_fun (hs'.inter ht') fun ω hω ↦ (min_eq_left hω.2.le).symm - · exact setLIntegral_congr_fun (hs'.diff ht') fun ω hω ↦ - (min_eq_right (not_lt.1 hω.2)).symm - _ = ∫⁻ ω in s, min (M m ω) c ∂P := lintegral_inter_add_sdiff _ s ht' + simpa only [Pi.inf_apply, le_inf_iff, le_refl, and_true] using + hMc.mul_measure_inter_exists_le_le hP h0 c hs /-- **Ville's inequality** [Vil39; RW, Fact 7.6]. For every `ℝ≥0∞`-valued supermartingale under a finite measure, with no integrability condition, and every level `0 < c < ∞`, the probability diff --git a/LMLExplore/Probability/Process/HittingTime.lean b/LMLExplore/Probability/Process/HittingTime.lean new file mode 100644 index 00000000..fc3c85cb --- /dev/null +++ b/LMLExplore/Probability/Process/HittingTime.lean @@ -0,0 +1,35 @@ +/- +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.HittingTime + +/-! +# Hitting times of processes indexed by `ℕ` + +For a process indexed by `ℕ`, Mathlib's `MeasureTheory.hittingAfter u s n` takes values in +`WithTop ℕ`, and `MeasureTheory.le_hittingAfter` bounds it below by the coercion +`WithTop.some n`. Stopping-time statements about `ℕ`-indexed processes use the cast +`(n : WithTop ℕ)` instead; this file restates the lower bound at that cast. + +## Main statements + +* `MeasureTheory.natCast_le_hittingAfter`: a hitting time after `n` is at least + `(n : WithTop ℕ)`. +-/ + +public section + +namespace MeasureTheory + +variable {Ω β : Type*} {u : ℕ → Ω → β} {s : Set β} {n : ℕ} + +/-- A hitting time after `n` of a process indexed by `ℕ` is at least the cast `(n : WithTop ℕ)`: +Mathlib's `MeasureTheory.le_hittingAfter` at the cast of a natural number. -/ +theorem natCast_le_hittingAfter (ω : Ω) : (n : WithTop ℕ) ≤ hittingAfter u s n ω := by + simpa using le_hittingAfter (u := u) (s := s) (n := n) ω + +end MeasureTheory From 381a8182cec6d3ab3d1e37150913f3b9d8d033b4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 11:36:28 +0100 Subject: [PATCH 6/6] refactor: use Mathlib's le_hittingAfter instead of natCast_le_hittingAfter MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Delete `LMLExplore/Probability/Process/HittingTime.lean`, whose only declaration `MeasureTheory.natCast_le_hittingAfter` restated Mathlib's `MeasureTheory.le_hittingAfter` at the cast `(n : WithTop ℕ)`. Its two uses in `ExactVille.lean` now pass `fun ω ↦ (Nat.cast_withTop m).trans_le (le_hittingAfter ω)` directly. Removed: `MeasureTheory.natCast_le_hittingAfter` (replaced by `(Nat.cast_withTop _).trans_le (MeasureTheory.le_hittingAfter _)`). Co-Authored-By: Claude Code --- .../Probability/Martingale/ExactVille.lean | 9 +++-- .../Probability/Process/HittingTime.lean | 35 ------------------- 2 files changed, 4 insertions(+), 40 deletions(-) delete mode 100644 LMLExplore/Probability/Process/HittingTime.lean diff --git a/LMLExplore/Probability/Martingale/ExactVille.lean b/LMLExplore/Probability/Martingale/ExactVille.lean index a3390e81..d7d33e8d 100644 --- a/LMLExplore/Probability/Martingale/ExactVille.lean +++ b/LMLExplore/Probability/Martingale/ExactVille.lean @@ -7,7 +7,6 @@ module public import LMLExplore.Probability.Martingale.Centering public import LMLExplore.Probability.Martingale.OptionalStopping -public import LMLExplore.Probability.Process.HittingTime /-! # The exact Ville identity @@ -213,8 +212,8 @@ theorem setLIntegral_eq_exact_ville_horizon (hM : IsENNSupermartingale M ℱ S) (fun ω ↦ min (hittingAfter M (Ici b) m ω) N) ω ∂P + ∫⁻ ω in s ∩ {ω | (N : WithTop ℕ) < hittingAfter M (Ici b) m ω}, M N ω ∂P := by have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b - rw [hM.setLIntegral_eq_add_stoppedValueLimsup_min hP h0 hT (natCast_le_hittingAfter) - hmN hs, + rw [hM.setLIntegral_eq_add_stoppedValueLimsup_min hP h0 hT + (fun ω ↦ (Nat.cast_withTop m).trans_le (le_hittingAfter ω)) hmN hs, setLIntegral_stoppedValueLimsup_hittingAfter b ((ℱ.le m _ hs).inter (ℱ.le N _ (hT.measurableSet_le_natCast N))) (fun ω hω ↦ ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hω.2)] @@ -308,8 +307,8 @@ theorem setLIntegral_eq_exact_ville (hM : IsENNSupermartingale M ℱ S) (hP : P have hT := hM.isStoppingTime_hittingAfter_Ici (m := m) b have hTtop : MeasurableSet {ω | hittingAfter M (Ici b) m ω ≠ ⊤} := by exact (hT.measurable' (measurableSet_singleton ⊤)).compl - rw [hM.setLIntegral_eq_add_stoppedValueLimsup_add_iInf hP h0 hT (natCast_le_hittingAfter) - hs, + rw [hM.setLIntegral_eq_add_stoppedValueLimsup_add_iInf hP h0 hT + (fun ω ↦ (Nat.cast_withTop m).trans_le (le_hittingAfter ω)) hs, setLIntegral_stoppedValueLimsup_hittingAfter b ((ℱ.le m _ hs).inter hTtop) inter_subset_right] diff --git a/LMLExplore/Probability/Process/HittingTime.lean b/LMLExplore/Probability/Process/HittingTime.lean deleted file mode 100644 index fc3c85cb..00000000 --- a/LMLExplore/Probability/Process/HittingTime.lean +++ /dev/null @@ -1,35 +0,0 @@ -/- -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.HittingTime - -/-! -# Hitting times of processes indexed by `ℕ` - -For a process indexed by `ℕ`, Mathlib's `MeasureTheory.hittingAfter u s n` takes values in -`WithTop ℕ`, and `MeasureTheory.le_hittingAfter` bounds it below by the coercion -`WithTop.some n`. Stopping-time statements about `ℕ`-indexed processes use the cast -`(n : WithTop ℕ)` instead; this file restates the lower bound at that cast. - -## Main statements - -* `MeasureTheory.natCast_le_hittingAfter`: a hitting time after `n` is at least - `(n : WithTop ℕ)`. --/ - -public section - -namespace MeasureTheory - -variable {Ω β : Type*} {u : ℕ → Ω → β} {s : Set β} {n : ℕ} - -/-- A hitting time after `n` of a process indexed by `ℕ` is at least the cast `(n : WithTop ℕ)`: -Mathlib's `MeasureTheory.le_hittingAfter` at the cast of a natural number. -/ -theorem natCast_le_hittingAfter (ω : Ω) : (n : WithTop ℕ) ≤ hittingAfter u s n ω := by - simpa using le_hittingAfter (u := u) (s := s) (n := n) ω - -end MeasureTheory