From 7b9a84d12b65945bcf4a7839e36602528e4e6137 Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Mon, 29 Dec 2025 12:41:29 +0100 Subject: [PATCH 1/5] initial commit --- Mathlib/Probability/Process/Filtration.lean | 163 ++++++++++++++++++++ 1 file changed, 163 insertions(+) diff --git a/Mathlib/Probability/Process/Filtration.lean b/Mathlib/Probability/Process/Filtration.lean index 3b3dba152e8c11..6ca6d278e5a4c7 100644 --- a/Mathlib/Probability/Process/Filtration.lean +++ b/Mathlib/Probability/Process/Filtration.lean @@ -22,6 +22,9 @@ This file defines filtrations of a measurable space and σ-finite filtrations. `μ` if for all `i`, `μ.trim (f.le i)` is σ-finite. * `MeasureTheory.Filtration.natural`: the smallest filtration that makes a process adapted. That notion `adapted` is not defined yet in this file. See `MeasureTheory.adapted`. +* `MeasureTheory.Filtration.rightCont`: the right-continuation of a filtration. +* `MeasureTheory.Filtration.IsRightContinuous`: a filtration is right-continuous if it is equal + to its right-continuation. ## Main results @@ -245,6 +248,166 @@ end OfSet namespace Filtration +section IsRightContinuous + +open scoped Classical in +/-- Given a filtration `𝓕`, its **right continuation** is the filtration `𝓕₊` defined as follows: +- If `i` is isolated on the right, then `𝓕₊ i := 𝓕 i`; +- Otherwise, `𝓕₊ i := ⨅ j > i, 𝓕 j`. +It is sometimes simply defined as `𝓕₊ i := ⨅ j > i, 𝓕 j` when the index type is `ℝ`. In the +general case this is not ideal however. If `i` is maximal for instance, then `𝓕₊ i = ⊤`, which +is inconvenient because `𝓕₊` is not a `Filtration ι m` anymore. If the index type +is discrete (such as `ℕ`), then we would have `𝓕 = 𝓕₊` (i.e. `𝓕` is right-continuous) only if +`𝓕` is constant. + +To avoid requiring a `TopologicalSpace` instance on `ι` in the definition, we endow `ι` with +the order topology `Preorder.topology` inside the definition. Say you write a statement about +`𝓕₊` which does not require a `TopologicalSpace` structure on `ι`, +but you wish to use a statement which requires a topology (such as `rightCont_def`). +Then you can endow `ι` with +the order topology by writing +```lean + letI := Preorder.topology ι + haveI : OrderTopology ι := ⟨rfl⟩ +``` -/ +noncomputable def rightCont [PartialOrder ι] (𝓕 : Filtration ι m) : Filtration ι m := + letI : TopologicalSpace ι := Preorder.topology ι + { seq i := if (𝓝[>] i).NeBot then ⨅ j > i, 𝓕 j else 𝓕 i + mono' i j hij := by + simp only [gt_iff_lt] + split_ifs with hi hj hj + · exact le_iInf₂ fun k hkj ↦ iInf₂_le k (hij.trans_lt hkj) + · obtain rfl | hj := eq_or_ne j i + · contradiction + · exact iInf₂_le j (lt_of_le_of_ne hij hj.symm) + · exact le_iInf₂ fun k hk ↦ 𝓕.mono (hij.trans hk.le) + · exact 𝓕.mono hij + le' i := by + split_ifs with hi + · obtain ⟨j, hj⟩ := (frequently_gt_nhds i).exists + exact iInf₂_le_of_le j hj (𝓕.le j) + · exact 𝓕.le i } + +@[inherit_doc] scoped postfix:max "₊" => rightCont + +open scoped Classical in +lemma rightCont_def [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] + (𝓕 : Filtration ι m) (i : ι) : + 𝓕₊ i = if (𝓝[>] i).NeBot then ⨅ j > i, 𝓕 j else 𝓕 i := by + simp only [rightCont, OrderTopology.topology_eq_generate_intervals] + +lemma rightCont_eq_of_nhdsGT_eq_bot [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] + (𝓕 : Filtration ι m) {i : ι} (hi : 𝓝[>] i = ⊥) : + 𝓕₊ i = 𝓕 i := by + rw [rightCont_def, hi, neBot_iff, ne_self_iff_false, if_false] + +/-- If the index type is a `SuccOrder`, then `𝓕₊ = 𝓕`. -/ +lemma rightCont_eq_self [LinearOrder ι] [SuccOrder ι] (𝓕 : Filtration ι m) : + 𝓕₊ = 𝓕 := by + letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩ + ext _ + rw [rightCont_eq_of_nhdsGT_eq_bot _ SuccOrder.nhdsGT] + +lemma rightCont_eq_of_isMax [PartialOrder ι] (𝓕 : Filtration ι m) {i : ι} (hi : IsMax i) : + 𝓕₊ i = 𝓕 i := by + letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩ + exact rightCont_eq_of_nhdsGT_eq_bot _ (hi.Ioi_eq ▸ nhdsWithin_empty i) + +lemma rightCont_eq_of_exists_gt [LinearOrder ι] (𝓕 : Filtration ι m) {i : ι} + (hi : ∃ j > i, Set.Ioo i j = ∅) : + 𝓕₊ i = 𝓕 i := by + letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩ + obtain ⟨j, hij, hIoo⟩ := hi + have hcov : i ⋖ j := covBy_iff_Ioo_eq.mpr ⟨hij, hIoo⟩ + exact rightCont_eq_of_nhdsGT_eq_bot _ <| CovBy.nhdsGT hcov + +/-- If `i` is not isolated on the right, then `𝓕₊ i = ⨅ j > i, 𝓕 j`. This is for instance the case +when `ι` is a densely ordered linear order with no maximal elements and equipped with the order +topology, see `rightCont_eq`. -/ +lemma rightCont_eq_of_neBot_nhdsGT [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] + (𝓕 : Filtration ι m) (i : ι) [(𝓝[>] i).NeBot] : + 𝓕₊ i = ⨅ j > i, 𝓕 j := by + rw [rightCont_def, if_pos ‹(𝓝[>] i).NeBot›] + +lemma rightCont_eq_of_not_isMax [LinearOrder ι] [DenselyOrdered ι] + (𝓕 : Filtration ι m) {i : ι} (hi : ¬IsMax i) : + 𝓕₊ i = ⨅ j > i, 𝓕 j := by + letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩ + have : (𝓝[>] i).NeBot := nhdsGT_neBot_of_exists_gt (not_isMax_iff.mp hi) + exact rightCont_eq_of_neBot_nhdsGT _ _ + +/-- If `ι` is a densely ordered linear order with no maximal elements, then no point is isolated +on the right, so that `𝓕₊ i = ⨅ j > i, 𝓕 j` holds for all `i`. This is in particular the +case when `ι := ℝ≥0`. -/ +lemma rightCont_eq [LinearOrder ι] [DenselyOrdered ι] [NoMaxOrder ι] + (𝓕 : Filtration ι m) (i : ι) : + 𝓕₊ i = ⨅ j > i, 𝓕 j := 𝓕.rightCont_eq_of_not_isMax (not_isMax i) + +variable [PartialOrder ι] + +lemma le_rightCont (𝓕 : Filtration ι m) : 𝓕 ≤ 𝓕₊ := by + letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩ + intro i + by_cases hne : (𝓝[>] i).NeBot + · rw [rightCont_eq_of_neBot_nhdsGT] + exact le_iInf₂ fun _ he => 𝓕.mono he.le + · rw [rightCont_def, if_neg hne] + +lemma rightCont_self (𝓕 : Filtration ι m) : 𝓕₊₊ = 𝓕₊ := by + letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩ + apply le_antisymm _ 𝓕₊.le_rightCont + intro i + by_cases hne : (𝓝[>] i).NeBot + · have hineq : (⨅ j > i, 𝓕₊ j) ≤ ⨅ j > i, 𝓕 j := by + apply le_iInf₂ fun u hu => ?_ + have hiou : Set.Ioo i u ∈ 𝓝[>] i := by + rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] + exact ⟨Set.Iio u, (isOpen_Iio' u).mem_nhds hu, fun _ hx ↦ ⟨hx.2, hx.1⟩⟩ + obtain ⟨v, hv⟩ := hne.nonempty_of_mem hiou + have hle₁ : (⨅ j > i, 𝓕₊ j) ≤ 𝓕₊ v := iInf₂_le_of_le v hv.1 le_rfl + have hle₂ : 𝓕₊ v ≤ 𝓕 u := by + by_cases hnv : (𝓝[>] v).NeBot + · simpa [rightCont_eq_of_neBot_nhdsGT] using iInf₂_le_of_le u hv.2 le_rfl + · simpa [rightCont_def, hnv] using 𝓕.mono hv.2.le + exact hle₁.trans hle₂ + simpa [rightCont_eq_of_neBot_nhdsGT] using hineq + · rw [rightCont_def, if_neg hne] + +/-- A filtration `𝓕` is right continuous if it is equal to its right continuation `𝓕₊`. -/ +class IsRightContinuous (𝓕 : Filtration ι m) where + /-- The right continuity property. -/ + RC : 𝓕₊ ≤ 𝓕 + +lemma IsRightContinuous.eq {𝓕 : Filtration ι m} [h : IsRightContinuous 𝓕] : + 𝓕 = 𝓕₊ := le_antisymm 𝓕.le_rightCont h.RC + +lemma isRightContinuous_rightCont (𝓕 : Filtration ι m) : 𝓕₊.IsRightContinuous := + ⟨(rightCont_self 𝓕).le⟩ + +lemma IsRightContinuous.measurableSet {𝓕 : Filtration ι m} [IsRightContinuous 𝓕] {i : ι} + {s : Set Ω} (hs : MeasurableSet[𝓕₊ i] s) : + MeasurableSet[𝓕 i] s := IsRightContinuous.eq (𝓕 := 𝓕) ▸ hs + +/-- A filtration `𝓕` is said to satisfy the usual conditions if it is right continuous and `𝓕 0` + and consequently `𝓕 t` is complete (i.e. contains all null sets) for all `t`. -/ +class HasUsualConditions [OrderBot ι] (𝓕 : Filtration ι m) (μ : Measure Ω := by volume_tac) + extends IsRightContinuous 𝓕 where + /-- `𝓕 ⊥` contains all the null sets. -/ + IsComplete ⦃s : Set Ω⦄ (hs : μ s = 0) : MeasurableSet[𝓕 ⊥] s + +variable [OrderBot ι] + +instance {𝓕 : Filtration ι m} {μ : Measure Ω} [u : HasUsualConditions 𝓕 μ] {i : ι} : + @Measure.IsComplete Ω (𝓕 i) (μ.trim <| 𝓕.le _) := + ⟨fun _ hs ↦ 𝓕.mono bot_le _ <| u.2 (measure_eq_zero_of_trim_eq_zero (Filtration.le 𝓕 _) hs)⟩ + +lemma HasUsualConditions.measurableSet_of_null + (𝓕 : Filtration ι m) {μ : Measure Ω} [u : HasUsualConditions 𝓕 μ] (s : Set Ω) (hs : μ s = 0) : + MeasurableSet[𝓕 ⊥] s := + u.2 hs + +end IsRightContinuous + variable {β : ι → Type*} [∀ i, TopologicalSpace (β i)] [∀ i, MetrizableSpace (β i)] [mβ : ∀ i, MeasurableSpace (β i)] [∀ i, BorelSpace (β i)] [Preorder ι] From addc4e9714c52c1e39c128fc6165c5bb3d3ae445 Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Mon, 29 Dec 2025 13:03:04 +0100 Subject: [PATCH 2/5] some work --- .../Probability/Process/LocalProperty.lean | 425 ++++++++++++++++++ Mathlib/Probability/Process/Stopping.lean | 110 +++++ 2 files changed, 535 insertions(+) create mode 100644 Mathlib/Probability/Process/LocalProperty.lean diff --git a/Mathlib/Probability/Process/LocalProperty.lean b/Mathlib/Probability/Process/LocalProperty.lean new file mode 100644 index 00000000000000..3e8e3792783339 --- /dev/null +++ b/Mathlib/Probability/Process/LocalProperty.lean @@ -0,0 +1,425 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Kexing Ying +-/ +import Mathlib.Probability.Process.Stopping + +/-! # Local properties of processes + +-/ + +open MeasureTheory Filter Filtration +open scoped ENNReal Topology + +namespace ProbabilityTheory + +variable {ι Ω E : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} + +/-- A localizing sequence is a sequence of stopping times that tends almost surely to infinity. -/ +structure IsPreLocalizingSequence [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] + (𝓕 : Filtration ι mΩ) (τ : ℕ → Ω → WithTop ι) (P : Measure Ω := by volume_tac) : + Prop where + isStoppingTime : ∀ n, IsStoppingTime 𝓕 (τ n) + tendsto_top : ∀ᵐ ω ∂P, Tendsto (τ · ω) atTop (𝓝 ⊤) + +/-- A localizing sequence is a sequence of stopping times that is almost surely increasing and +tends almost surely to infinity. -/ +structure IsLocalizingSequence [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] + (𝓕 : Filtration ι mΩ) (τ : ℕ → Ω → WithTop ι) + (P : Measure Ω := by volume_tac) extends IsPreLocalizingSequence 𝓕 τ P where + mono : ∀ᵐ ω ∂P, Monotone (τ · ω) + +lemma isLocalizingSequence_const_top [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] + (𝓕 : Filtration ι mΩ) (P : Measure Ω) : IsLocalizingSequence 𝓕 (fun _ _ ↦ ⊤) P where + isStoppingTime n := by simp [IsStoppingTime] + mono := ae_of_all _ fun _ _ _ _ ↦ by simp + tendsto_top := by filter_upwards [] with ω using tendsto_const_nhds + +section LinearOrder + +variable [LinearOrder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} + +lemma IsLocalizingSequence.min [TopologicalSpace ι] [OrderTopology ι] {τ σ : ℕ → Ω → WithTop ι} + (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : IsLocalizingSequence 𝓕 σ P) : + IsLocalizingSequence 𝓕 (min τ σ) P where + isStoppingTime n := (hτ.isStoppingTime n).min (hσ.isStoppingTime n) + mono := by filter_upwards [hτ.mono, hσ.mono] with ω hτω hσω; exact hτω.min hσω + tendsto_top := by + filter_upwards [hτ.tendsto_top, hσ.tendsto_top] with ω hτω hσω using hτω.min hσω + +variable [OrderBot ι] + +/-- A stochastic process `X` is said to satisfy a property `p` locally with respect to a +filtration `𝓕` if there exists a localizing sequence `(τ_n)` such that for all `n`, the stopped +process of `fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)` satisfies `p`. -/ +def Locally [TopologicalSpace ι] [OrderTopology ι] [Zero E] + (p : (ι → Ω → E) → Prop) (𝓕 : Filtration ι mΩ) + (X : ι → Ω → E) (P : Measure Ω := by volume_tac) : Prop := + ∃ τ : ℕ → Ω → WithTop ι, IsLocalizingSequence 𝓕 τ P ∧ + ∀ n, p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n)) + +section Locally + +variable [TopologicalSpace ι] [OrderTopology ι] + +/-- A localizing sequence, witness of the local property of the stochastic process. -/ +noncomputable +def Locally.localSeq [Zero E] (hX : Locally p 𝓕 X P) : + ℕ → Ω → WithTop ι := + hX.choose + +lemma Locally.IsLocalizingSequence [Zero E] (hX : Locally p 𝓕 X P) : + IsLocalizingSequence 𝓕 (hX.localSeq) P := + hX.choose_spec.1 + +lemma Locally.stoppedProcess [Zero E] (hX : Locally p 𝓕 X P) (n : ℕ) : + p (stoppedProcess (fun i ↦ {ω | ⊥ < hX.localSeq n ω}.indicator (X i)) (hX.localSeq n)) := + hX.choose_spec.2 n + +lemma locally_of_prop [Zero E] (hp : p X) : Locally p 𝓕 X P := + ⟨fun n _ ↦ (⊤ : WithTop ι), isLocalizingSequence_const_top _ _, by simpa⟩ + +lemma Locally.mono [Zero E] (hpq : ∀ X, p X → q X) (hpX : Locally p 𝓕 X P) : + Locally q 𝓕 X P := + ⟨hpX.localSeq, hpX.IsLocalizingSequence, fun n ↦ hpq _ <| hpX.stoppedProcess n⟩ + +lemma Locally.of_and [Zero E] (hX : Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P) : + Locally p 𝓕 X P ∧ Locally q 𝓕 X P := + ⟨hX.mono <| fun _ ↦ And.left, hX.mono <| fun _ ↦ And.right⟩ + +lemma Locally.of_and_left [Zero E] (hX : Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P) : + Locally p 𝓕 X P := + hX.of_and.left + +lemma Locally.of_and_right [Zero E] (hX : Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P) : + Locally q 𝓕 X P := + hX.of_and.right + +end Locally + +variable [Zero E] + +/-- A property of stochastic processes is said to be stable if it is preserved under taking +the stopped process by a stopping time. -/ +def IsStable + (𝓕 : Filtration ι mΩ) (p : (ι → Ω → E) → Prop) : Prop := + ∀ X : ι → Ω → E, p X → ∀ τ : Ω → WithTop ι, IsStoppingTime 𝓕 τ → + p (stoppedProcess (fun i ↦ {ω | ⊥ < τ ω}.indicator (X i)) τ) + +lemma IsStable.and (p q : (ι → Ω → E) → Prop) + (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) : + IsStable 𝓕 (fun X ↦ p X ∧ q X) := + fun _ hX τ hτ ↦ ⟨hp _ hX.left τ hτ, hq _ hX.right τ hτ⟩ + +variable [TopologicalSpace ι] [OrderTopology ι] + +lemma IsStable.isStable_locally (hp : IsStable 𝓕 p) : + IsStable 𝓕 (fun Y ↦ Locally p 𝓕 Y P) := by + intro X hX τ hτ + refine ⟨hX.localSeq, hX.IsLocalizingSequence, fun n ↦ ?_⟩ + simp_rw [← stoppedProcess_indicator_comm', Set.indicator_indicator, Set.inter_comm, + ← Set.indicator_indicator, stoppedProcess_stoppedProcess, inf_comm] + rw [stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess] + exact hp _ (hX.stoppedProcess n) τ hτ + +lemma locally_and (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) : + Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P ↔ Locally p 𝓕 X P ∧ Locally q 𝓕 X P := by + refine ⟨Locally.of_and, fun ⟨hpX, hqX⟩ ↦ + ⟨_, hpX.IsLocalizingSequence.min hqX.IsLocalizingSequence, fun n ↦ ⟨?_, ?_⟩⟩⟩ + · convert hp _ (hpX.stoppedProcess n) _ <| hqX.IsLocalizingSequence.isStoppingTime n using 1 + ext i ω + rw [stoppedProcess_indicator_comm] + simp_rw [Pi.inf_apply, lt_inf_iff, inf_comm (hpX.localSeq n)] + rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, + (_ : {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω} + = {ω | ⊥ < hpX.localSeq n ω} ∩ {ω | ⊥ < hqX.localSeq n ω}), Set.inter_comm] + · simp_rw [← Set.indicator_indicator] + rfl + · rfl + · convert hq _ (hqX.stoppedProcess n) _ <| hpX.IsLocalizingSequence.isStoppingTime n using 1 + ext i ω + rw [stoppedProcess_indicator_comm] + simp_rw [Pi.inf_apply, lt_inf_iff] + rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, + (_ : {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω} + = {ω | ⊥ < hpX.localSeq n ω} ∩ {ω | ⊥ < hqX.localSeq n ω})] + · simp_rw [← Set.indicator_indicator] + rfl + · rfl + +end LinearOrder + +section ConditionallyCompleteLinearOrderBot + +variable [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] + [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι] + {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} + +lemma measure_iInter_of_ae_antitone {ι : Type*} + [Countable ι] [Preorder ι] [IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2] + {s : ι → Set Ω} (hs : ∀ᵐ ω ∂P, Antitone (s · ω)) + (hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) P) (hfin : ∃ (i : ι), P (s i) ≠ ⊤) : + P (⋂ (i : ι), s i) = ⨅ (i : ι), P (s i) := by + set t : ι → Set Ω := fun i ↦ ⋂ j ≤ i, s j with ht + have hst (i : ι) : s i =ᵐ[P] t i := by + filter_upwards [hs] with ω hω + suffices ω ∈ s i ↔ ω ∈ t i by + exact propext this + simp only [ht, Set.mem_iInter] + refine ⟨fun (h : s i ω) j hj ↦ ?_, fun h ↦ h i le_rfl⟩ + change s j ω + specialize hω hj + simp only [le_Prop_eq] at hω + exact hω h + rw [measure_congr <| EventuallyEq.countable_iInter hst, Antitone.measure_iInter] + · exact iInf_congr <| fun i ↦ measure_congr <| (hst i).symm + · intros i j hij + simp only [ht] + rw [(_ : ⋂ k ≤ j, s k = (⋂ k ≤ i, s k) ∩ (⋂ k ∈ {k | k ≤ j ∧ ¬ k ≤ i}, s k))] + · exact Set.inter_subset_left + · ext ω + simp only [Set.mem_iInter, Set.mem_setOf_eq, Set.mem_inter_iff, and_imp] + grind + · exact fun _ ↦ NullMeasurableSet.iInter <| fun j ↦ NullMeasurableSet.iInter <| fun _ ↦ hsm j + · obtain ⟨i, hi⟩ := hfin + refine ⟨i, (lt_of_le_of_lt ?_ <| lt_top_iff_ne_top.2 hi).ne⟩ + rw [measure_congr (hst i)] + +lemma isLocalizingSequence_of_isPreLocalizingSequence + {τ : ℕ → Ω → WithTop ι} [IsRightContinuous 𝓕] (hτ : IsPreLocalizingSequence 𝓕 τ P) : + IsLocalizingSequence 𝓕 (fun i ω ↦ ⨅ j ≥ i, τ j ω) P where + isStoppingTime (n : ℕ) := IsStoppingTime.iInf {j | j ≥ n} (fun j ↦ hτ.isStoppingTime j) + mono := ae_of_all _ <| fun ω n m hnm ↦ iInf_le_iInf_of_subset <| fun k hk ↦ hnm.trans hk + tendsto_top := by + filter_upwards [hτ.tendsto_top] with ω hω + replace hω := hω.liminf_eq + rw [liminf_eq_iSup_iInf_of_nat] at hω + rw [← hω] + refine tendsto_atTop_iSup ?_ + intro n m hnm + simp only [ge_iff_le, le_iInf_iff, iInf_le_iff] + intro k hk i hi + grind + +/-- A stable property holds locally `p` for `X` if there exists a pre-localizing sequence `τ` for +which the stopped process of `fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)` satisfies `p`. -/ +lemma locally_of_isPreLocalizingSequence [Zero E] {τ : ℕ → Ω → WithTop ι} + (hp : IsStable 𝓕 p) [IsRightContinuous 𝓕] (hτ : IsPreLocalizingSequence 𝓕 τ P) + (hpτ : ∀ n, p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))) : + Locally p 𝓕 X P := by + refine ⟨_, isLocalizingSequence_of_isPreLocalizingSequence hτ, fun n ↦ ?_⟩ + have := hp _ (hpτ n) (fun ω ↦ ⨅ j ≥ n, τ j ω) <| + (isLocalizingSequence_of_isPreLocalizingSequence hτ).isStoppingTime n + rw [stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess_of_le_right + (τ := fun ω ↦ τ n ω) (fun _ ↦ (iInf_le _ n).trans <| iInf_le _ le_rfl), + ← stoppedProcess_indicator_comm'] + convert this using 2 + ext i ω + rw [stoppedProcess_indicator_comm', Set.indicator_indicator] + congr 1 + ext ω' + simp only [ge_iff_le, Set.mem_setOf_eq, Set.mem_inter_iff] + exact ⟨fun h ↦ ⟨h, lt_of_lt_of_le h <| (iInf_le _ n).trans (iInf_le _ le_rfl)⟩, fun h ↦ h.1⟩ + +section + +omit [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι] +variable [SecondCountableTopology ι] [IsFiniteMeasure P] + +lemma isPreLocalizingSequence_of_isLocalizingSequence_aux' + {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι} + (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : ∀ n, IsLocalizingSequence 𝓕 (σ n) P) : + ∃ T : ℕ → ι, Tendsto T atTop atTop + ∧ ∀ n, ∃ k, P {ω | σ n k ω < min (τ n ω) (T n)} ≤ (1 / 2) ^ n := by + obtain ⟨T, -, hT⟩ := Filter.exists_seq_monotone_tendsto_atTop_atTop ι + refine ⟨T, hT, fun n ↦ ?_⟩ + by_contra hn; push_neg at hn + suffices (1 / 2) ^ n ≤ P (⋂ k : ℕ, {ω | σ n k ω < min (τ n ω) (T n)}) by + refine (by simp : ¬ (1 / 2 : ℝ≥0∞) ^ n ≤ 0) <| this.trans <| nonpos_iff_eq_zero.2 ?_ + rw [measure_eq_zero_iff_ae_notMem] + filter_upwards [(hσ n).tendsto_top] with ω hTop hmem + rw [WithTop.tendsto_atTop_nhds_top_iff] at hTop + simp only [Set.mem_iInter, Set.mem_setOf_eq] at hmem + obtain ⟨N, hN⟩ := hTop (T n) + specialize hN N le_rfl + specialize hmem N + grind + rw [measure_iInter_of_ae_antitone, le_iInf_iff] + · exact fun k ↦ (hn k).le + · filter_upwards [(hσ n).mono] with ω hω + intros i j hij + specialize hω hij + simp only [lt_inf_iff, le_Prop_eq] at * + change σ n j ω < τ n ω ∧ σ n j ω < T n → σ n i ω < τ n ω ∧ σ n i ω < T n + grind + · intro i + refine MeasurableSet.nullMeasurableSet ?_ + have hMσ := ((hσ n).isStoppingTime i).measurable + have hMτ := (hτ.isStoppingTime n).measurable + simp_rw [lt_inf_iff] + rw [(_ : {ω | σ n i ω < τ n ω ∧ σ n i ω < T n} = {ω | σ n i ω < τ n ω} ∩ {ω | σ n i ω < T n})] + · exact MeasurableSet.inter + (measurableSet_lt ((hσ n).isStoppingTime i).measurable' (hτ.isStoppingTime n).measurable') + <| measurableSet_lt ((hσ n).isStoppingTime i).measurable' measurable_const + · rfl + · exact ⟨0, measure_ne_top P _⟩ + +/-- Auxliary defintion for `isPreLocalizingSequence_of_isLocalizingSequence` which constructs a +strictly increasing sequence from a given sequence. -/ +def mkStrictMonoAux (x : ℕ → ℕ) : ℕ → ℕ +| 0 => x 0 +| n + 1 => max (x (n + 1)) (mkStrictMonoAux x n) + 1 + +lemma mkStrictMonoAux_strictMono (x : ℕ → ℕ) : StrictMono (mkStrictMonoAux x) := by + refine strictMono_nat_of_lt_succ <| fun n ↦ ?_ + simp only [mkStrictMonoAux] + exact lt_of_le_of_lt (le_max_right (x (n + 1)) _) (lt_add_one (max (x (n + 1)) _)) + +lemma le_mkStrictMonoAux (x : ℕ → ℕ) : ∀ n, x n ≤ mkStrictMonoAux x n +| 0 => by simp [mkStrictMonoAux] +| n + 1 => by + simp only [mkStrictMonoAux] + exact (le_max_left (x (n + 1)) (mkStrictMonoAux x n)).trans <| + Nat.le_add_right (max (x (n + 1)) (mkStrictMonoAux x n)) 1 + +lemma isPreLocalizingSequence_of_isLocalizingSequence_aux + {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι} + (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : ∀ n, IsLocalizingSequence 𝓕 (σ n) P) : + ∃ nk : ℕ → ℕ, StrictMono nk ∧ ∃ T : ℕ → ι, Tendsto T atTop atTop + ∧ ∀ n, P {ω | σ n (nk n) ω < min (τ n ω) (T n)} ≤ (1 / 2) ^ n := by + obtain ⟨T, hT, h⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux' hτ hσ + choose nk hnk using h + refine ⟨mkStrictMonoAux nk, mkStrictMonoAux_strictMono nk, T, hT, fun n ↦ + le_trans (EventuallyLE.measure_le ?_) (hnk n)⟩ + filter_upwards [(hσ n).mono] with ω hω + specialize hω (le_mkStrictMonoAux nk n) + simp only [lt_inf_iff, le_Prop_eq] + change σ n (mkStrictMonoAux nk n) ω < τ n ω ∧ σ n (mkStrictMonoAux nk n) ω < T n → + σ n (nk n) ω < τ n ω ∧ σ n (nk n) ω < T n + grind + +lemma isPreLocalizingSequence_of_isLocalizingSequence + [NoMaxOrder ι] {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι} + (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : ∀ n, IsLocalizingSequence 𝓕 (σ n) P) : + ∃ nk : ℕ → ℕ, StrictMono nk + ∧ IsPreLocalizingSequence 𝓕 (fun i ω ↦ (τ i ω) ⊓ (σ i (nk i) ω)) P := by + obtain ⟨nk, hnk, T, hT, hP⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux hτ hσ + refine ⟨nk, hnk, fun n ↦ (hτ.isStoppingTime n).min ((hσ _).isStoppingTime _), ?_⟩ + have : ∑' n, P {ω | σ n (nk n) ω < min (τ n ω) (T n)} < ∞ := + lt_of_le_of_lt (ENNReal.summable.tsum_mono ENNReal.summable hP) + (tsum_geometric_lt_top.2 <| by norm_num) + have hτTop := hτ.tendsto_top + filter_upwards [ae_eventually_notMem this.ne, hτTop] with ω hω hωτ + replace hT := hωτ.min hT.tendsto_withTop_atTop_nhds_top + simp_rw [eventually_atTop, not_lt, ← eventually_atTop] at hω + rw [min_self] at hT + rw [← min_self ⊤] + refine hωτ.min <| tendsto_of_tendsto_of_tendsto_of_le_of_le' hT tendsto_const_nhds hω ?_ + simp only [le_top, eventually_atTop, ge_iff_le, implies_true, exists_const] + +variable [DenselyOrdered ι] [NoMaxOrder ι] [Zero E] + +/-- A stable property holding locally is idempotent. -/ +lemma locally_locally + [IsRightContinuous 𝓕] (hp : IsStable 𝓕 p) : + Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P := by + refine ⟨fun hL ↦ ?_, fun hL ↦ ?_⟩ + · have hLL := hL.stoppedProcess + choose τ hτ₁ hτ₂ using hLL + obtain ⟨nk, hnk, hpre⟩ := isPreLocalizingSequence_of_isLocalizingSequence + hL.IsLocalizingSequence hτ₁ + refine locally_of_isPreLocalizingSequence hp hpre <| fun n ↦ ?_ + specialize hτ₂ n (nk n) + convert hτ₂ using 1 + ext i ω + rw [stoppedProcess_indicator_comm', stoppedProcess_indicator_comm', + stoppedProcess_stoppedProcess, stoppedProcess_indicator_comm'] + simp only [lt_inf_iff, Set.indicator_indicator] + congr 1 + · ext ω'; simp only [And.comm, Set.mem_setOf_eq, Set.mem_inter_iff] + · simp_rw [inf_comm] + rfl + · exact ⟨hL.localSeq, hL.IsLocalizingSequence, fun n ↦ locally_of_prop <| hL.stoppedProcess n⟩ + +/-- If `p` implies `q` locally, then `p` locally implies `q` locally. -/ +lemma locally_induction [IsRightContinuous 𝓕] + (hpq : ∀ Y, p Y → Locally q 𝓕 Y P) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) : + Locally q 𝓕 X P := + (locally_locally hq).1 <| hpX.mono hpq + +lemma locally_induction₂ {r : (ι → Ω → E) → Prop} [IsRightContinuous 𝓕] + (hrpq : ∀ Y, r Y → p Y → Locally q 𝓕 Y P) + (hr : IsStable 𝓕 r) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) + (hrX : Locally r 𝓕 X P) (hpX : Locally p 𝓕 X P) : + Locally q 𝓕 X P := + locally_induction (p := fun Y ↦ r Y ∧ p Y) (and_imp.2 <| hrpq ·) hq + <| (locally_and hr hp).2 ⟨hrX, hpX⟩ + +end + +end ConditionallyCompleteLinearOrderBot + +section LinearOrder + +variable [LinearOrder ι] [OrderBot ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} + +open Classical in +/-- Given a property on paths which holds almost surely for a stochastic process, we construct a +localizing sequence by setting the stopping time to be ∞ whenever the property holds. -/ +noncomputable +def LocalizingSequence_of_prop (X : ι → Ω → E) (p : (ι → E) → Prop) : ℕ → Ω → WithTop ι := + Function.const _ <| fun ω ↦ if p (X · ω) then ⊤ else ⊥ + +lemma isStoppingTime_ae_const [HasUsualConditions 𝓕 P] (τ : Ω → WithTop ι) (c : WithTop ι) + (hτ : τ =ᵐ[P] Function.const _ c) : + IsStoppingTime 𝓕 τ := by + intros i + suffices P {ω | τ ω ≤ i} = 0 ∨ P {ω | τ ω ≤ ↑i}ᶜ = 0 by + obtain h | h := this + · exact 𝓕.mono bot_le _ <| HasUsualConditions.IsComplete h + · exact (𝓕.mono bot_le _ <| HasUsualConditions.IsComplete h).of_compl + obtain hle | hgt := le_or_gt c i + · refine Or.inr <| ae_iff.1 ?_ + filter_upwards [hτ] with ω rfl using hle + · refine Or.inl ?_ + rw [← compl_compl {ω | τ ω ≤ i}] + refine ae_iff.1 ?_ + filter_upwards [hτ] with ω hω + simp [hω, hgt] + +variable [TopologicalSpace ι] [OrderTopology ι] + +lemma isLocalizingSequence_ae [HasUsualConditions 𝓕 P] {p : (ι → E) → Prop} + (hpX : ∀ᵐ ω ∂P, p (X · ω)) : + IsLocalizingSequence 𝓕 (LocalizingSequence_of_prop X p) P where + isStoppingTime n := by + refine isStoppingTime_ae_const (P := P) _ ⊤ ?_ + filter_upwards [hpX] with ω hω + rw [LocalizingSequence_of_prop, Function.const_apply, Function.const_apply, if_pos hω] + mono := ae_of_all _ <| fun ω i j hij ↦ by simp [LocalizingSequence_of_prop] + tendsto_top := by + filter_upwards [hpX] with ω hω + simp [LocalizingSequence_of_prop, if_pos hω] + +variable [Zero E] + +open Classical in +lemma locally_of_ae [HasUsualConditions 𝓕 P] {p : (ι → E) → Prop} (hpX : ∀ᵐ ω ∂P, p (X · ω)) + (hp₀ : p (0 : ι → E)) : + Locally (fun X ↦ ∀ ω, p (X · ω)) 𝓕 X P := by + refine ⟨_, isLocalizingSequence_ae hpX, fun _ ω ↦ ?_⟩ + by_cases hω : p (X · ω) + · convert hω using 2 + rw [stoppedProcess_eq_of_le, Set.indicator_of_mem] + · simp [LocalizingSequence_of_prop, if_pos hω] + · simp [LocalizingSequence_of_prop, if_pos hω] + · convert hp₀ using 2 + rw [stoppedProcess_eq_of_ge, Set.indicator_of_notMem] + · rfl + · simp [LocalizingSequence_of_prop, if_neg hω] + · simp [LocalizingSequence_of_prop, if_neg hω] + +end LinearOrder + +end ProbabilityTheory diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean index 90d0b534ba5437..27901b67a66016 100644 --- a/Mathlib/Probability/Process/Stopping.lean +++ b/Mathlib/Probability/Process/Stopping.lean @@ -270,6 +270,104 @@ theorem isStoppingTime_of_measurableSet_eq [Preorder ι] [Countable ι] {f : Fil end Countable +section IsRightContinuous + +open Filtration + +variable [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] + [DenselyOrdered ι] [FirstCountableTopology ι] {f : Filtration ι m} + +lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous [NoMaxOrder ι] + {τ : Ω → WithTop ι} [hf : f.IsRightContinuous] (hτ : ∀ i, MeasurableSet[f i] {ω | τ ω < i}) : + IsStoppingTime f τ := by + intro i + obtain ⟨u, hu₁, hu₂, hu₃⟩ := exists_seq_strictAnti_tendsto i + refine MeasurableSet.of_compl ?_ + rw [(_ : {ω | τ ω ≤ i}ᶜ = ⋃ n, {ω | u n ≤ τ ω})] + · refine hf.measurableSet ?_ + simp_rw [f.rightCont_eq, MeasurableSpace.measurableSet_iInf] + intros j hj + obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hj).exists + rw [(_ : ⋃ n, {ω | u n ≤ τ ω} = ⋃ n ≥ N, {ω | u n ≤ τ ω})] + · refine MeasurableSet.iUnion <| fun n ↦ MeasurableSet.iUnion <| fun hn ↦ + f.mono ((hu₁.antitone hn).trans hN) _ <| MeasurableSet.of_compl ?_ + rw [(by ext; simp : {ω | u n ≤ τ ω}ᶜ = {ω | τ ω < u n})] + exact hτ (u n) + · ext ω + simp only [Set.mem_iUnion, Set.mem_setOf_eq, ge_iff_le, exists_prop] + constructor + · rintro ⟨i, hle⟩ + refine ⟨i + N, N.le_add_left i, le_trans ?_ hle⟩ + norm_cast + exact hu₁.antitone <| i.le_add_right N + · rintro ⟨i, -, hi⟩ + exact ⟨i, hi⟩ + · ext ω + simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, Set.mem_iUnion] + constructor + · intro h + by_cases hτ : τ ω = ⊤ + · exact ⟨0, hτ ▸ le_top⟩ + · have hlt : i < (τ ω).untop hτ := by + rwa [WithTop.lt_untop_iff] + obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hlt).exists + refine ⟨N, WithTop.coe_le_iff.2 <| fun n hn ↦ hN.trans ?_⟩ + simp [hn, WithTop.untop_coe] + · rintro ⟨j, hj⟩ + refine lt_of_lt_of_le ?_ hj + norm_cast + exact hu₂ _ + +lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous' + {τ : Ω → WithTop ι} [hf : f.IsRightContinuous] + (hτ1 : ∀ i, ¬ IsMax i → MeasurableSet[f i] {ω | τ ω < i}) + (hτ2 : ∀ i, IsMax i → MeasurableSet[f i] {ω | τ ω ≤ i}) : + IsStoppingTime f τ := by + intro i + by_cases hmax : IsMax i + · rw [hf.eq, f.rightCont_eq_of_isMax hmax] + exact hτ2 i hmax + rw [hf.eq, f.rightCont_eq_of_not_isMax hmax] + rw [not_isMax_iff] at hmax + obtain ⟨j, hj⟩ := hmax + obtain ⟨u, hu₁, hu₂, hu₃⟩ := exists_seq_strictAnti_tendsto' hj + refine MeasurableSet.of_compl ?_ + rw [(_ : {ω | τ ω ≤ i}ᶜ = ⋃ n, {ω | u n ≤ τ ω})] + · simp_rw [MeasurableSpace.measurableSet_iInf] + intros j hj + obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hj).exists + rw [(_ : ⋃ n, {ω | u n ≤ τ ω} = ⋃ n > N, {ω | u n ≤ τ ω})] + · refine MeasurableSet.iUnion <| fun n ↦ MeasurableSet.iUnion <| fun hn ↦ + f.mono ((hu₁ hn).le.trans hN) _ <| MeasurableSet.of_compl ?_ + rw [(by ext; simp : {ω | u n ≤ τ ω}ᶜ = {ω | τ ω < u n})] + refine hτ1 (u n) <| not_isMax_iff.2 ⟨u N, hu₁ hn⟩ + · ext ω + simp only [Set.mem_iUnion, Set.mem_setOf_eq, gt_iff_lt, exists_prop] + constructor + · rintro ⟨i, hle⟩ + refine ⟨i + N + 1, by linarith, le_trans ?_ hle⟩ + norm_cast + exact hu₁.antitone (by linarith) + · rintro ⟨i, -, hi⟩ + exact ⟨i, hi⟩ + · ext ω + simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, Set.mem_iUnion] + constructor + · intro h + by_cases hτ : τ ω = ⊤ + · exact ⟨0, hτ ▸ le_top⟩ + · have hlt : i < (τ ω).untop hτ := by + rwa [WithTop.lt_untop_iff] + obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hlt).exists + refine ⟨N, WithTop.coe_le_iff.2 <| fun n hn ↦ hN.trans ?_⟩ + simp [hn, WithTop.untop_coe] + · rintro ⟨j, hj⟩ + refine lt_of_lt_of_le ?_ hj + norm_cast + exact (hu₂ j).1 + +end IsRightContinuous + end MeasurableSet namespace IsStoppingTime @@ -296,6 +394,18 @@ protected theorem min_const [LinearOrder ι] {f : Filtration ι m} {τ : Ω → (hτ : IsStoppingTime f τ) (i : ι) : IsStoppingTime f fun ω => min (τ ω) i := hτ.min (isStoppingTime_const f i) +protected lemma iInf [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] + [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι] + {f : Filtration ι m} {τ : ℕ → Ω → WithTop ι} (s : Set ℕ) + [f.IsRightContinuous] (hτ : ∀ n, IsStoppingTime f (τ n)) : + IsStoppingTime f (fun ω ↦ ⨅ (n) (_ : n ∈ s), τ n ω) := by + refine isStoppingTime_of_measurableSet_lt_of_isRightContinuous <| + fun i ↦ MeasurableSet.of_compl ?_ + rw [(_ : {ω | ⨅ n ∈ s, τ n ω < i}ᶜ = ⋂ n ∈ s, {ω | i ≤ τ n ω})] + · exact MeasurableSet.iInter <| fun n ↦ MeasurableSet.iInter <| fun hn ↦ (hτ n).measurableSet_ge i + · ext ω + simp + theorem add_const [AddGroup ι] [Preorder ι] [AddRightMono ι] [AddLeftMono ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) {i : ι} (hi : 0 ≤ i) : IsStoppingTime f fun ω => τ ω + i := by From c7cd7e986564fe68f7214ef844cb866050ae8777 Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Mon, 29 Dec 2025 13:03:31 +0100 Subject: [PATCH 3/5] del --- .../Probability/Process/LocalProperty.lean | 425 ------------------ 1 file changed, 425 deletions(-) delete mode 100644 Mathlib/Probability/Process/LocalProperty.lean diff --git a/Mathlib/Probability/Process/LocalProperty.lean b/Mathlib/Probability/Process/LocalProperty.lean deleted file mode 100644 index 3e8e3792783339..00000000000000 --- a/Mathlib/Probability/Process/LocalProperty.lean +++ /dev/null @@ -1,425 +0,0 @@ -/- -Copyright (c) 2025 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne, Kexing Ying --/ -import Mathlib.Probability.Process.Stopping - -/-! # Local properties of processes - --/ - -open MeasureTheory Filter Filtration -open scoped ENNReal Topology - -namespace ProbabilityTheory - -variable {ι Ω E : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} - -/-- A localizing sequence is a sequence of stopping times that tends almost surely to infinity. -/ -structure IsPreLocalizingSequence [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] - (𝓕 : Filtration ι mΩ) (τ : ℕ → Ω → WithTop ι) (P : Measure Ω := by volume_tac) : - Prop where - isStoppingTime : ∀ n, IsStoppingTime 𝓕 (τ n) - tendsto_top : ∀ᵐ ω ∂P, Tendsto (τ · ω) atTop (𝓝 ⊤) - -/-- A localizing sequence is a sequence of stopping times that is almost surely increasing and -tends almost surely to infinity. -/ -structure IsLocalizingSequence [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] - (𝓕 : Filtration ι mΩ) (τ : ℕ → Ω → WithTop ι) - (P : Measure Ω := by volume_tac) extends IsPreLocalizingSequence 𝓕 τ P where - mono : ∀ᵐ ω ∂P, Monotone (τ · ω) - -lemma isLocalizingSequence_const_top [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] - (𝓕 : Filtration ι mΩ) (P : Measure Ω) : IsLocalizingSequence 𝓕 (fun _ _ ↦ ⊤) P where - isStoppingTime n := by simp [IsStoppingTime] - mono := ae_of_all _ fun _ _ _ _ ↦ by simp - tendsto_top := by filter_upwards [] with ω using tendsto_const_nhds - -section LinearOrder - -variable [LinearOrder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} - -lemma IsLocalizingSequence.min [TopologicalSpace ι] [OrderTopology ι] {τ σ : ℕ → Ω → WithTop ι} - (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : IsLocalizingSequence 𝓕 σ P) : - IsLocalizingSequence 𝓕 (min τ σ) P where - isStoppingTime n := (hτ.isStoppingTime n).min (hσ.isStoppingTime n) - mono := by filter_upwards [hτ.mono, hσ.mono] with ω hτω hσω; exact hτω.min hσω - tendsto_top := by - filter_upwards [hτ.tendsto_top, hσ.tendsto_top] with ω hτω hσω using hτω.min hσω - -variable [OrderBot ι] - -/-- A stochastic process `X` is said to satisfy a property `p` locally with respect to a -filtration `𝓕` if there exists a localizing sequence `(τ_n)` such that for all `n`, the stopped -process of `fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)` satisfies `p`. -/ -def Locally [TopologicalSpace ι] [OrderTopology ι] [Zero E] - (p : (ι → Ω → E) → Prop) (𝓕 : Filtration ι mΩ) - (X : ι → Ω → E) (P : Measure Ω := by volume_tac) : Prop := - ∃ τ : ℕ → Ω → WithTop ι, IsLocalizingSequence 𝓕 τ P ∧ - ∀ n, p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n)) - -section Locally - -variable [TopologicalSpace ι] [OrderTopology ι] - -/-- A localizing sequence, witness of the local property of the stochastic process. -/ -noncomputable -def Locally.localSeq [Zero E] (hX : Locally p 𝓕 X P) : - ℕ → Ω → WithTop ι := - hX.choose - -lemma Locally.IsLocalizingSequence [Zero E] (hX : Locally p 𝓕 X P) : - IsLocalizingSequence 𝓕 (hX.localSeq) P := - hX.choose_spec.1 - -lemma Locally.stoppedProcess [Zero E] (hX : Locally p 𝓕 X P) (n : ℕ) : - p (stoppedProcess (fun i ↦ {ω | ⊥ < hX.localSeq n ω}.indicator (X i)) (hX.localSeq n)) := - hX.choose_spec.2 n - -lemma locally_of_prop [Zero E] (hp : p X) : Locally p 𝓕 X P := - ⟨fun n _ ↦ (⊤ : WithTop ι), isLocalizingSequence_const_top _ _, by simpa⟩ - -lemma Locally.mono [Zero E] (hpq : ∀ X, p X → q X) (hpX : Locally p 𝓕 X P) : - Locally q 𝓕 X P := - ⟨hpX.localSeq, hpX.IsLocalizingSequence, fun n ↦ hpq _ <| hpX.stoppedProcess n⟩ - -lemma Locally.of_and [Zero E] (hX : Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P) : - Locally p 𝓕 X P ∧ Locally q 𝓕 X P := - ⟨hX.mono <| fun _ ↦ And.left, hX.mono <| fun _ ↦ And.right⟩ - -lemma Locally.of_and_left [Zero E] (hX : Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P) : - Locally p 𝓕 X P := - hX.of_and.left - -lemma Locally.of_and_right [Zero E] (hX : Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P) : - Locally q 𝓕 X P := - hX.of_and.right - -end Locally - -variable [Zero E] - -/-- A property of stochastic processes is said to be stable if it is preserved under taking -the stopped process by a stopping time. -/ -def IsStable - (𝓕 : Filtration ι mΩ) (p : (ι → Ω → E) → Prop) : Prop := - ∀ X : ι → Ω → E, p X → ∀ τ : Ω → WithTop ι, IsStoppingTime 𝓕 τ → - p (stoppedProcess (fun i ↦ {ω | ⊥ < τ ω}.indicator (X i)) τ) - -lemma IsStable.and (p q : (ι → Ω → E) → Prop) - (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) : - IsStable 𝓕 (fun X ↦ p X ∧ q X) := - fun _ hX τ hτ ↦ ⟨hp _ hX.left τ hτ, hq _ hX.right τ hτ⟩ - -variable [TopologicalSpace ι] [OrderTopology ι] - -lemma IsStable.isStable_locally (hp : IsStable 𝓕 p) : - IsStable 𝓕 (fun Y ↦ Locally p 𝓕 Y P) := by - intro X hX τ hτ - refine ⟨hX.localSeq, hX.IsLocalizingSequence, fun n ↦ ?_⟩ - simp_rw [← stoppedProcess_indicator_comm', Set.indicator_indicator, Set.inter_comm, - ← Set.indicator_indicator, stoppedProcess_stoppedProcess, inf_comm] - rw [stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess] - exact hp _ (hX.stoppedProcess n) τ hτ - -lemma locally_and (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) : - Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P ↔ Locally p 𝓕 X P ∧ Locally q 𝓕 X P := by - refine ⟨Locally.of_and, fun ⟨hpX, hqX⟩ ↦ - ⟨_, hpX.IsLocalizingSequence.min hqX.IsLocalizingSequence, fun n ↦ ⟨?_, ?_⟩⟩⟩ - · convert hp _ (hpX.stoppedProcess n) _ <| hqX.IsLocalizingSequence.isStoppingTime n using 1 - ext i ω - rw [stoppedProcess_indicator_comm] - simp_rw [Pi.inf_apply, lt_inf_iff, inf_comm (hpX.localSeq n)] - rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, - (_ : {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω} - = {ω | ⊥ < hpX.localSeq n ω} ∩ {ω | ⊥ < hqX.localSeq n ω}), Set.inter_comm] - · simp_rw [← Set.indicator_indicator] - rfl - · rfl - · convert hq _ (hqX.stoppedProcess n) _ <| hpX.IsLocalizingSequence.isStoppingTime n using 1 - ext i ω - rw [stoppedProcess_indicator_comm] - simp_rw [Pi.inf_apply, lt_inf_iff] - rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, - (_ : {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω} - = {ω | ⊥ < hpX.localSeq n ω} ∩ {ω | ⊥ < hqX.localSeq n ω})] - · simp_rw [← Set.indicator_indicator] - rfl - · rfl - -end LinearOrder - -section ConditionallyCompleteLinearOrderBot - -variable [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] - [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι] - {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} - -lemma measure_iInter_of_ae_antitone {ι : Type*} - [Countable ι] [Preorder ι] [IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2] - {s : ι → Set Ω} (hs : ∀ᵐ ω ∂P, Antitone (s · ω)) - (hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) P) (hfin : ∃ (i : ι), P (s i) ≠ ⊤) : - P (⋂ (i : ι), s i) = ⨅ (i : ι), P (s i) := by - set t : ι → Set Ω := fun i ↦ ⋂ j ≤ i, s j with ht - have hst (i : ι) : s i =ᵐ[P] t i := by - filter_upwards [hs] with ω hω - suffices ω ∈ s i ↔ ω ∈ t i by - exact propext this - simp only [ht, Set.mem_iInter] - refine ⟨fun (h : s i ω) j hj ↦ ?_, fun h ↦ h i le_rfl⟩ - change s j ω - specialize hω hj - simp only [le_Prop_eq] at hω - exact hω h - rw [measure_congr <| EventuallyEq.countable_iInter hst, Antitone.measure_iInter] - · exact iInf_congr <| fun i ↦ measure_congr <| (hst i).symm - · intros i j hij - simp only [ht] - rw [(_ : ⋂ k ≤ j, s k = (⋂ k ≤ i, s k) ∩ (⋂ k ∈ {k | k ≤ j ∧ ¬ k ≤ i}, s k))] - · exact Set.inter_subset_left - · ext ω - simp only [Set.mem_iInter, Set.mem_setOf_eq, Set.mem_inter_iff, and_imp] - grind - · exact fun _ ↦ NullMeasurableSet.iInter <| fun j ↦ NullMeasurableSet.iInter <| fun _ ↦ hsm j - · obtain ⟨i, hi⟩ := hfin - refine ⟨i, (lt_of_le_of_lt ?_ <| lt_top_iff_ne_top.2 hi).ne⟩ - rw [measure_congr (hst i)] - -lemma isLocalizingSequence_of_isPreLocalizingSequence - {τ : ℕ → Ω → WithTop ι} [IsRightContinuous 𝓕] (hτ : IsPreLocalizingSequence 𝓕 τ P) : - IsLocalizingSequence 𝓕 (fun i ω ↦ ⨅ j ≥ i, τ j ω) P where - isStoppingTime (n : ℕ) := IsStoppingTime.iInf {j | j ≥ n} (fun j ↦ hτ.isStoppingTime j) - mono := ae_of_all _ <| fun ω n m hnm ↦ iInf_le_iInf_of_subset <| fun k hk ↦ hnm.trans hk - tendsto_top := by - filter_upwards [hτ.tendsto_top] with ω hω - replace hω := hω.liminf_eq - rw [liminf_eq_iSup_iInf_of_nat] at hω - rw [← hω] - refine tendsto_atTop_iSup ?_ - intro n m hnm - simp only [ge_iff_le, le_iInf_iff, iInf_le_iff] - intro k hk i hi - grind - -/-- A stable property holds locally `p` for `X` if there exists a pre-localizing sequence `τ` for -which the stopped process of `fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)` satisfies `p`. -/ -lemma locally_of_isPreLocalizingSequence [Zero E] {τ : ℕ → Ω → WithTop ι} - (hp : IsStable 𝓕 p) [IsRightContinuous 𝓕] (hτ : IsPreLocalizingSequence 𝓕 τ P) - (hpτ : ∀ n, p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))) : - Locally p 𝓕 X P := by - refine ⟨_, isLocalizingSequence_of_isPreLocalizingSequence hτ, fun n ↦ ?_⟩ - have := hp _ (hpτ n) (fun ω ↦ ⨅ j ≥ n, τ j ω) <| - (isLocalizingSequence_of_isPreLocalizingSequence hτ).isStoppingTime n - rw [stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess_of_le_right - (τ := fun ω ↦ τ n ω) (fun _ ↦ (iInf_le _ n).trans <| iInf_le _ le_rfl), - ← stoppedProcess_indicator_comm'] - convert this using 2 - ext i ω - rw [stoppedProcess_indicator_comm', Set.indicator_indicator] - congr 1 - ext ω' - simp only [ge_iff_le, Set.mem_setOf_eq, Set.mem_inter_iff] - exact ⟨fun h ↦ ⟨h, lt_of_lt_of_le h <| (iInf_le _ n).trans (iInf_le _ le_rfl)⟩, fun h ↦ h.1⟩ - -section - -omit [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι] -variable [SecondCountableTopology ι] [IsFiniteMeasure P] - -lemma isPreLocalizingSequence_of_isLocalizingSequence_aux' - {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι} - (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : ∀ n, IsLocalizingSequence 𝓕 (σ n) P) : - ∃ T : ℕ → ι, Tendsto T atTop atTop - ∧ ∀ n, ∃ k, P {ω | σ n k ω < min (τ n ω) (T n)} ≤ (1 / 2) ^ n := by - obtain ⟨T, -, hT⟩ := Filter.exists_seq_monotone_tendsto_atTop_atTop ι - refine ⟨T, hT, fun n ↦ ?_⟩ - by_contra hn; push_neg at hn - suffices (1 / 2) ^ n ≤ P (⋂ k : ℕ, {ω | σ n k ω < min (τ n ω) (T n)}) by - refine (by simp : ¬ (1 / 2 : ℝ≥0∞) ^ n ≤ 0) <| this.trans <| nonpos_iff_eq_zero.2 ?_ - rw [measure_eq_zero_iff_ae_notMem] - filter_upwards [(hσ n).tendsto_top] with ω hTop hmem - rw [WithTop.tendsto_atTop_nhds_top_iff] at hTop - simp only [Set.mem_iInter, Set.mem_setOf_eq] at hmem - obtain ⟨N, hN⟩ := hTop (T n) - specialize hN N le_rfl - specialize hmem N - grind - rw [measure_iInter_of_ae_antitone, le_iInf_iff] - · exact fun k ↦ (hn k).le - · filter_upwards [(hσ n).mono] with ω hω - intros i j hij - specialize hω hij - simp only [lt_inf_iff, le_Prop_eq] at * - change σ n j ω < τ n ω ∧ σ n j ω < T n → σ n i ω < τ n ω ∧ σ n i ω < T n - grind - · intro i - refine MeasurableSet.nullMeasurableSet ?_ - have hMσ := ((hσ n).isStoppingTime i).measurable - have hMτ := (hτ.isStoppingTime n).measurable - simp_rw [lt_inf_iff] - rw [(_ : {ω | σ n i ω < τ n ω ∧ σ n i ω < T n} = {ω | σ n i ω < τ n ω} ∩ {ω | σ n i ω < T n})] - · exact MeasurableSet.inter - (measurableSet_lt ((hσ n).isStoppingTime i).measurable' (hτ.isStoppingTime n).measurable') - <| measurableSet_lt ((hσ n).isStoppingTime i).measurable' measurable_const - · rfl - · exact ⟨0, measure_ne_top P _⟩ - -/-- Auxliary defintion for `isPreLocalizingSequence_of_isLocalizingSequence` which constructs a -strictly increasing sequence from a given sequence. -/ -def mkStrictMonoAux (x : ℕ → ℕ) : ℕ → ℕ -| 0 => x 0 -| n + 1 => max (x (n + 1)) (mkStrictMonoAux x n) + 1 - -lemma mkStrictMonoAux_strictMono (x : ℕ → ℕ) : StrictMono (mkStrictMonoAux x) := by - refine strictMono_nat_of_lt_succ <| fun n ↦ ?_ - simp only [mkStrictMonoAux] - exact lt_of_le_of_lt (le_max_right (x (n + 1)) _) (lt_add_one (max (x (n + 1)) _)) - -lemma le_mkStrictMonoAux (x : ℕ → ℕ) : ∀ n, x n ≤ mkStrictMonoAux x n -| 0 => by simp [mkStrictMonoAux] -| n + 1 => by - simp only [mkStrictMonoAux] - exact (le_max_left (x (n + 1)) (mkStrictMonoAux x n)).trans <| - Nat.le_add_right (max (x (n + 1)) (mkStrictMonoAux x n)) 1 - -lemma isPreLocalizingSequence_of_isLocalizingSequence_aux - {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι} - (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : ∀ n, IsLocalizingSequence 𝓕 (σ n) P) : - ∃ nk : ℕ → ℕ, StrictMono nk ∧ ∃ T : ℕ → ι, Tendsto T atTop atTop - ∧ ∀ n, P {ω | σ n (nk n) ω < min (τ n ω) (T n)} ≤ (1 / 2) ^ n := by - obtain ⟨T, hT, h⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux' hτ hσ - choose nk hnk using h - refine ⟨mkStrictMonoAux nk, mkStrictMonoAux_strictMono nk, T, hT, fun n ↦ - le_trans (EventuallyLE.measure_le ?_) (hnk n)⟩ - filter_upwards [(hσ n).mono] with ω hω - specialize hω (le_mkStrictMonoAux nk n) - simp only [lt_inf_iff, le_Prop_eq] - change σ n (mkStrictMonoAux nk n) ω < τ n ω ∧ σ n (mkStrictMonoAux nk n) ω < T n → - σ n (nk n) ω < τ n ω ∧ σ n (nk n) ω < T n - grind - -lemma isPreLocalizingSequence_of_isLocalizingSequence - [NoMaxOrder ι] {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι} - (hτ : IsLocalizingSequence 𝓕 τ P) (hσ : ∀ n, IsLocalizingSequence 𝓕 (σ n) P) : - ∃ nk : ℕ → ℕ, StrictMono nk - ∧ IsPreLocalizingSequence 𝓕 (fun i ω ↦ (τ i ω) ⊓ (σ i (nk i) ω)) P := by - obtain ⟨nk, hnk, T, hT, hP⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux hτ hσ - refine ⟨nk, hnk, fun n ↦ (hτ.isStoppingTime n).min ((hσ _).isStoppingTime _), ?_⟩ - have : ∑' n, P {ω | σ n (nk n) ω < min (τ n ω) (T n)} < ∞ := - lt_of_le_of_lt (ENNReal.summable.tsum_mono ENNReal.summable hP) - (tsum_geometric_lt_top.2 <| by norm_num) - have hτTop := hτ.tendsto_top - filter_upwards [ae_eventually_notMem this.ne, hτTop] with ω hω hωτ - replace hT := hωτ.min hT.tendsto_withTop_atTop_nhds_top - simp_rw [eventually_atTop, not_lt, ← eventually_atTop] at hω - rw [min_self] at hT - rw [← min_self ⊤] - refine hωτ.min <| tendsto_of_tendsto_of_tendsto_of_le_of_le' hT tendsto_const_nhds hω ?_ - simp only [le_top, eventually_atTop, ge_iff_le, implies_true, exists_const] - -variable [DenselyOrdered ι] [NoMaxOrder ι] [Zero E] - -/-- A stable property holding locally is idempotent. -/ -lemma locally_locally - [IsRightContinuous 𝓕] (hp : IsStable 𝓕 p) : - Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P := by - refine ⟨fun hL ↦ ?_, fun hL ↦ ?_⟩ - · have hLL := hL.stoppedProcess - choose τ hτ₁ hτ₂ using hLL - obtain ⟨nk, hnk, hpre⟩ := isPreLocalizingSequence_of_isLocalizingSequence - hL.IsLocalizingSequence hτ₁ - refine locally_of_isPreLocalizingSequence hp hpre <| fun n ↦ ?_ - specialize hτ₂ n (nk n) - convert hτ₂ using 1 - ext i ω - rw [stoppedProcess_indicator_comm', stoppedProcess_indicator_comm', - stoppedProcess_stoppedProcess, stoppedProcess_indicator_comm'] - simp only [lt_inf_iff, Set.indicator_indicator] - congr 1 - · ext ω'; simp only [And.comm, Set.mem_setOf_eq, Set.mem_inter_iff] - · simp_rw [inf_comm] - rfl - · exact ⟨hL.localSeq, hL.IsLocalizingSequence, fun n ↦ locally_of_prop <| hL.stoppedProcess n⟩ - -/-- If `p` implies `q` locally, then `p` locally implies `q` locally. -/ -lemma locally_induction [IsRightContinuous 𝓕] - (hpq : ∀ Y, p Y → Locally q 𝓕 Y P) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) : - Locally q 𝓕 X P := - (locally_locally hq).1 <| hpX.mono hpq - -lemma locally_induction₂ {r : (ι → Ω → E) → Prop} [IsRightContinuous 𝓕] - (hrpq : ∀ Y, r Y → p Y → Locally q 𝓕 Y P) - (hr : IsStable 𝓕 r) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) - (hrX : Locally r 𝓕 X P) (hpX : Locally p 𝓕 X P) : - Locally q 𝓕 X P := - locally_induction (p := fun Y ↦ r Y ∧ p Y) (and_imp.2 <| hrpq ·) hq - <| (locally_and hr hp).2 ⟨hrX, hpX⟩ - -end - -end ConditionallyCompleteLinearOrderBot - -section LinearOrder - -variable [LinearOrder ι] [OrderBot ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} - -open Classical in -/-- Given a property on paths which holds almost surely for a stochastic process, we construct a -localizing sequence by setting the stopping time to be ∞ whenever the property holds. -/ -noncomputable -def LocalizingSequence_of_prop (X : ι → Ω → E) (p : (ι → E) → Prop) : ℕ → Ω → WithTop ι := - Function.const _ <| fun ω ↦ if p (X · ω) then ⊤ else ⊥ - -lemma isStoppingTime_ae_const [HasUsualConditions 𝓕 P] (τ : Ω → WithTop ι) (c : WithTop ι) - (hτ : τ =ᵐ[P] Function.const _ c) : - IsStoppingTime 𝓕 τ := by - intros i - suffices P {ω | τ ω ≤ i} = 0 ∨ P {ω | τ ω ≤ ↑i}ᶜ = 0 by - obtain h | h := this - · exact 𝓕.mono bot_le _ <| HasUsualConditions.IsComplete h - · exact (𝓕.mono bot_le _ <| HasUsualConditions.IsComplete h).of_compl - obtain hle | hgt := le_or_gt c i - · refine Or.inr <| ae_iff.1 ?_ - filter_upwards [hτ] with ω rfl using hle - · refine Or.inl ?_ - rw [← compl_compl {ω | τ ω ≤ i}] - refine ae_iff.1 ?_ - filter_upwards [hτ] with ω hω - simp [hω, hgt] - -variable [TopologicalSpace ι] [OrderTopology ι] - -lemma isLocalizingSequence_ae [HasUsualConditions 𝓕 P] {p : (ι → E) → Prop} - (hpX : ∀ᵐ ω ∂P, p (X · ω)) : - IsLocalizingSequence 𝓕 (LocalizingSequence_of_prop X p) P where - isStoppingTime n := by - refine isStoppingTime_ae_const (P := P) _ ⊤ ?_ - filter_upwards [hpX] with ω hω - rw [LocalizingSequence_of_prop, Function.const_apply, Function.const_apply, if_pos hω] - mono := ae_of_all _ <| fun ω i j hij ↦ by simp [LocalizingSequence_of_prop] - tendsto_top := by - filter_upwards [hpX] with ω hω - simp [LocalizingSequence_of_prop, if_pos hω] - -variable [Zero E] - -open Classical in -lemma locally_of_ae [HasUsualConditions 𝓕 P] {p : (ι → E) → Prop} (hpX : ∀ᵐ ω ∂P, p (X · ω)) - (hp₀ : p (0 : ι → E)) : - Locally (fun X ↦ ∀ ω, p (X · ω)) 𝓕 X P := by - refine ⟨_, isLocalizingSequence_ae hpX, fun _ ω ↦ ?_⟩ - by_cases hω : p (X · ω) - · convert hω using 2 - rw [stoppedProcess_eq_of_le, Set.indicator_of_mem] - · simp [LocalizingSequence_of_prop, if_pos hω] - · simp [LocalizingSequence_of_prop, if_pos hω] - · convert hp₀ using 2 - rw [stoppedProcess_eq_of_ge, Set.indicator_of_notMem] - · rfl - · simp [LocalizingSequence_of_prop, if_neg hω] - · simp [LocalizingSequence_of_prop, if_neg hω] - -end LinearOrder - -end ProbabilityTheory From 7e102fef37cc188f16e04df3399def211cc95c2a Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Mon, 29 Dec 2025 13:17:50 +0100 Subject: [PATCH 4/5] add biInf --- Mathlib/Probability/Process/Stopping.lean | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean index 27901b67a66016..e370e0facb15e0 100644 --- a/Mathlib/Probability/Process/Stopping.lean +++ b/Mathlib/Probability/Process/Stopping.lean @@ -394,18 +394,26 @@ protected theorem min_const [LinearOrder ι] {f : Filtration ι m} {τ : Ω → (hτ : IsStoppingTime f τ) (i : ι) : IsStoppingTime f fun ω => min (τ ω) i := hτ.min (isStoppingTime_const f i) -protected lemma iInf [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] +protected lemma biInf [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι] - {f : Filtration ι m} {τ : ℕ → Ω → WithTop ι} (s : Set ℕ) - [f.IsRightContinuous] (hτ : ∀ n, IsStoppingTime f (τ n)) : + {κ : Type*} {f : Filtration ι m} {τ : κ → Ω → WithTop ι} {s : Set κ} (hs : s.Countable) + [f.IsRightContinuous] (hτ : ∀ n ∈ s, IsStoppingTime f (τ n)) : IsStoppingTime f (fun ω ↦ ⨅ (n) (_ : n ∈ s), τ n ω) := by refine isStoppingTime_of_measurableSet_lt_of_isRightContinuous <| fun i ↦ MeasurableSet.of_compl ?_ rw [(_ : {ω | ⨅ n ∈ s, τ n ω < i}ᶜ = ⋂ n ∈ s, {ω | i ≤ τ n ω})] - · exact MeasurableSet.iInter <| fun n ↦ MeasurableSet.iInter <| fun hn ↦ (hτ n).measurableSet_ge i + · exact MeasurableSet.biInter hs <| fun n hn ↦ (hτ n hn).measurableSet_ge i · ext ω simp +protected lemma iInf [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] + [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι] + {κ : Type*} [Countable κ] {f : Filtration ι m} {τ : κ → Ω → WithTop ι} + [f.IsRightContinuous] (hτ : ∀ n, IsStoppingTime f (τ n)) : + IsStoppingTime f (fun ω ↦ ⨅ n, τ n ω) := by + convert IsStoppingTime.biInf (κ := κ) Set.countable_univ (fun n _ => hτ n) using 2 + simp + theorem add_const [AddGroup ι] [Preorder ι] [AddRightMono ι] [AddLeftMono ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) {i : ι} (hi : 0 ≤ i) : IsStoppingTime f fun ω => τ ω + i := by From 212b4fe8d85ac5b9f95c168ccb713917fb66e336 Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Sun, 4 Jan 2026 15:09:33 +0100 Subject: [PATCH 5/5] minor --- Mathlib/Probability/Process/Stopping.lean | 51 ++++------------------- 1 file changed, 8 insertions(+), 43 deletions(-) diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean index e370e0facb15e0..3553f66146454f 100644 --- a/Mathlib/Probability/Process/Stopping.lean +++ b/Mathlib/Probability/Process/Stopping.lean @@ -277,47 +277,6 @@ open Filtration variable [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] {f : Filtration ι m} -lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous [NoMaxOrder ι] - {τ : Ω → WithTop ι} [hf : f.IsRightContinuous] (hτ : ∀ i, MeasurableSet[f i] {ω | τ ω < i}) : - IsStoppingTime f τ := by - intro i - obtain ⟨u, hu₁, hu₂, hu₃⟩ := exists_seq_strictAnti_tendsto i - refine MeasurableSet.of_compl ?_ - rw [(_ : {ω | τ ω ≤ i}ᶜ = ⋃ n, {ω | u n ≤ τ ω})] - · refine hf.measurableSet ?_ - simp_rw [f.rightCont_eq, MeasurableSpace.measurableSet_iInf] - intros j hj - obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hj).exists - rw [(_ : ⋃ n, {ω | u n ≤ τ ω} = ⋃ n ≥ N, {ω | u n ≤ τ ω})] - · refine MeasurableSet.iUnion <| fun n ↦ MeasurableSet.iUnion <| fun hn ↦ - f.mono ((hu₁.antitone hn).trans hN) _ <| MeasurableSet.of_compl ?_ - rw [(by ext; simp : {ω | u n ≤ τ ω}ᶜ = {ω | τ ω < u n})] - exact hτ (u n) - · ext ω - simp only [Set.mem_iUnion, Set.mem_setOf_eq, ge_iff_le, exists_prop] - constructor - · rintro ⟨i, hle⟩ - refine ⟨i + N, N.le_add_left i, le_trans ?_ hle⟩ - norm_cast - exact hu₁.antitone <| i.le_add_right N - · rintro ⟨i, -, hi⟩ - exact ⟨i, hi⟩ - · ext ω - simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, Set.mem_iUnion] - constructor - · intro h - by_cases hτ : τ ω = ⊤ - · exact ⟨0, hτ ▸ le_top⟩ - · have hlt : i < (τ ω).untop hτ := by - rwa [WithTop.lt_untop_iff] - obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hlt).exists - refine ⟨N, WithTop.coe_le_iff.2 <| fun n hn ↦ hN.trans ?_⟩ - simp [hn, WithTop.untop_coe] - · rintro ⟨j, hj⟩ - refine lt_of_lt_of_le ?_ hj - norm_cast - exact hu₂ _ - lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous' {τ : Ω → WithTop ι} [hf : f.IsRightContinuous] (hτ1 : ∀ i, ¬ IsMax i → MeasurableSet[f i] {ω | τ ω < i}) @@ -325,9 +284,9 @@ lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous' IsStoppingTime f τ := by intro i by_cases hmax : IsMax i - · rw [hf.eq, f.rightCont_eq_of_isMax hmax] + · rw [← hf.eq, f.rightCont_eq_of_isMax hmax] exact hτ2 i hmax - rw [hf.eq, f.rightCont_eq_of_not_isMax hmax] + rw [← hf.eq, f.rightCont_eq_of_not_isMax hmax] rw [not_isMax_iff] at hmax obtain ⟨j, hj⟩ := hmax obtain ⟨u, hu₁, hu₂, hu₃⟩ := exists_seq_strictAnti_tendsto' hj @@ -366,6 +325,12 @@ lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous' norm_cast exact (hu₂ j).1 +lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous [NoMaxOrder ι] + {τ : Ω → WithTop ι} [f.IsRightContinuous] (hτ : ∀ i, MeasurableSet[f i] {ω | τ ω < i}) : + IsStoppingTime f τ := + isStoppingTime_of_measurableSet_lt_of_isRightContinuous' (fun i _ ↦ hτ i) + <| fun i hi ↦ False.elim <| (not_isMax i) hi + end IsRightContinuous end MeasurableSet