From 7b9a84d12b65945bcf4a7839e36602528e4e6137 Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Mon, 29 Dec 2025 12:41:29 +0100 Subject: [PATCH 1/3] 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 8381c2bcced55a96bb6210ebd56ef85319379b44 Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Fri, 2 Jan 2026 17:35:07 +0100 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Sebastien Gouezel --- Mathlib/Probability/Process/Filtration.lean | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/Mathlib/Probability/Process/Filtration.lean b/Mathlib/Probability/Process/Filtration.lean index 6ca6d278e5a4c7..0897191b9a03d3 100644 --- a/Mathlib/Probability/Process/Filtration.lean +++ b/Mathlib/Probability/Process/Filtration.lean @@ -256,7 +256,7 @@ open scoped Classical in - 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 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. @@ -264,13 +264,12 @@ To avoid requiring a `TopologicalSpace` instance on `ΞΉ` in the definition, we e 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 +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 := +noncomputable irreducible_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 @@ -336,7 +335,7 @@ lemma rightCont_eq_of_not_isMax [LinearOrder ΞΉ] [DenselyOrdered ΞΉ] 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 +/-- If `ΞΉ` is a densely ordered linear order with no maximal element, 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 ΞΉ] @@ -353,7 +352,7 @@ lemma le_rightCont (𝓕 : Filtration ΞΉ m) : 𝓕 ≀ π“•β‚Š := by exact le_iInfβ‚‚ fun _ he => 𝓕.mono he.le Β· rw [rightCont_def, if_neg hne] -lemma rightCont_self (𝓕 : Filtration ΞΉ m) : π“•β‚Šβ‚Š = π“•β‚Š := by +@[simp] lemma rightCont_self (𝓕 : Filtration ΞΉ m) : π“•β‚Šβ‚Š = π“•β‚Š := by letI := Preorder.topology ΞΉ; haveI : OrderTopology ΞΉ := ⟨rfl⟩ apply le_antisymm _ π“•β‚Š.le_rightCont intro i @@ -375,8 +374,8 @@ lemma rightCont_self (𝓕 : Filtration ΞΉ m) : π“•β‚Šβ‚Š = π“•β‚Š := by /-- A filtration `𝓕` is right continuous if it is equal to its right continuation `π“•β‚Š`. -/ class IsRightContinuous (𝓕 : Filtration ΞΉ m) where - /-- The right continuity property. -/ - RC : π“•β‚Š ≀ 𝓕 + /-- The right continuity property. -/ + RC : π“•β‚Š ≀ 𝓕 lemma IsRightContinuous.eq {𝓕 : Filtration ΞΉ m} [h : IsRightContinuous 𝓕] : 𝓕 = π“•β‚Š := le_antisymm 𝓕.le_rightCont h.RC From e5d6e0dd50dae14eb1afde065237b8d49f5b32ca Mon Sep 17 00:00:00 2001 From: Kexing Ying Date: Fri, 2 Jan 2026 17:42:16 +0100 Subject: [PATCH 3/3] reviews --- Mathlib/Probability/Process/Filtration.lean | 39 ++++++--------------- 1 file changed, 10 insertions(+), 29 deletions(-) diff --git a/Mathlib/Probability/Process/Filtration.lean b/Mathlib/Probability/Process/Filtration.lean index 0897191b9a03d3..aacfe0cc3c19f8 100644 --- a/Mathlib/Probability/Process/Filtration.lean +++ b/Mathlib/Probability/Process/Filtration.lean @@ -263,7 +263,7 @@ is discrete (such as `β„•`), then we would have `𝓕 = π“•β‚Š` (i.e. `𝓕` is 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`). +but you wish to use a statement which requires a topology (such as `rightCont_apply`). Then you can endow `ΞΉ` with the order topology by writing ```lean letI := Preorder.topology ΞΉ @@ -290,7 +290,7 @@ noncomputable irreducible_def rightCont [PartialOrder ΞΉ] (𝓕 : Filtration ΞΉ @[inherit_doc] scoped postfix:max "β‚Š" => rightCont open scoped Classical in -lemma rightCont_def [PartialOrder ΞΉ] [TopologicalSpace ΞΉ] [OrderTopology ΞΉ] +lemma rightCont_apply [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] @@ -298,10 +298,10 @@ lemma rightCont_def [PartialOrder ΞΉ] [TopologicalSpace ΞΉ] [OrderTopology ΞΉ] 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] + rw [rightCont_apply, 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) : +@[simp] lemma rightCont_eq_self [LinearOrder ΞΉ] [SuccOrder ΞΉ] (𝓕 : Filtration ΞΉ m) : π“•β‚Š = 𝓕 := by letI := Preorder.topology ΞΉ; haveI : OrderTopology ΞΉ := ⟨rfl⟩ ext _ @@ -326,7 +326,7 @@ 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β€Ί] + rw [rightCont_apply, if_pos β€Ή(𝓝[>] i).NeBotβ€Ί] lemma rightCont_eq_of_not_isMax [LinearOrder ΞΉ] [DenselyOrdered ΞΉ] (𝓕 : Filtration ΞΉ m) {i : ΞΉ} (hi : Β¬IsMax i) : @@ -350,7 +350,7 @@ lemma le_rightCont (𝓕 : Filtration ΞΉ m) : 𝓕 ≀ π“•β‚Š := by 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] + Β· rw [rightCont_apply, if_neg hne] @[simp] lemma rightCont_self (𝓕 : Filtration ΞΉ m) : π“•β‚Šβ‚Š = π“•β‚Š := by letI := Preorder.topology ΞΉ; haveI : OrderTopology ΞΉ := ⟨rfl⟩ @@ -367,10 +367,10 @@ lemma le_rightCont (𝓕 : Filtration ΞΉ m) : 𝓕 ≀ π“•β‚Š := by 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 + Β· simpa [rightCont_apply, hnv] using 𝓕.mono hv.2.le exact hle₁.trans hleβ‚‚ simpa [rightCont_eq_of_neBot_nhdsGT] using hineq - Β· rw [rightCont_def, if_neg hne] + Β· rw [rightCont_apply, if_neg hne] /-- A filtration `𝓕` is right continuous if it is equal to its right continuation `π“•β‚Š`. -/ class IsRightContinuous (𝓕 : Filtration ΞΉ m) where @@ -378,33 +378,14 @@ class IsRightContinuous (𝓕 : Filtration ΞΉ m) where RC : π“•β‚Š ≀ 𝓕 lemma IsRightContinuous.eq {𝓕 : Filtration ΞΉ m} [h : IsRightContinuous 𝓕] : - 𝓕 = π“•β‚Š := le_antisymm 𝓕.le_rightCont h.RC + π“•β‚Š = 𝓕 := (le_antisymm 𝓕.le_rightCont h.RC).symm -lemma isRightContinuous_rightCont (𝓕 : Filtration ΞΉ m) : π“•β‚Š.IsRightContinuous := - ⟨(rightCont_self 𝓕).le⟩ +instance {𝓕 : 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)]