Cadlag modification of quasimartingales

We build right-continuous and càdlàg modifications of real quasimartingales.

The construction is done in two steps. First, for a process X and an antitone family of events R d on which the paths of X along a countable dense set of times have left and right limits before d (IsRegularityFamily), we define processes rightContModifOf R X and cadlagModifOf R X from the right limits of X, and we prove their regularity and measurability properties. That part applies to processes with values in a normed group. Then, for a real quasimartingale X, the events regularitySet T X d, defined with the upcrossings of X, are almost sure and give the modifications rightContModifReal X and cadlagModifReal X.

See the file CadlagModificationBanach for martingales with values in a Banach space.

theorem Dense.exists_gt_of_not_isMax {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : Dense s) {a : α} (ha : ¬IsMax a) : ∃ b ∈ s, a < b

A dense set contains points above any point which is not maximal.

theorem Dense.exists_between_of_nhdsGT_neBot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : Dense s) {a b : α} [(nhdsWithin a (Set.Ioi a)).NeBot] (hab : a < b) : ∃ c ∈ s, a < c ∧ c < b

A dense set contains points in Ioo a b for a < b, if a is not isolated on the right. Version of Dense.exists_between for an order which may not be densely ordered.

theorem IsMax.nhdsGT_eq_bot {α : Type u_1} [Preorder α] [TopologicalSpace α] {a : α} (ha : IsMax a) : nhdsWithin a (Set.Ioi a) = ⊥

A maximal element is isolated on the right.

theorem not_isMax_of_nhdsGT_neBot {α : Type u_1} [Preorder α] [TopologicalSpace α] {a : α} [h : (nhdsWithin a (Set.Ioi a)).NeBot] : ¬IsMax a

A point which is not isolated on the right is not maximal.

theorem MeasureTheory.UniformIntegrable.tendsto_setIntegral {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [IsFiniteMeasure μ] {f : ℕ → Ω → E} {g : Ω → E} (hUI : UniformIntegrable f 1 μ) (hfg : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop (nhds (g ω))) (A : Set Ω) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω) in A, f n ω ∂μ) Filter.atTop (nhds (∫ (ω : Ω) in A, g ω ∂μ))

Vitali: if a uniformly integrable sequence converges almost everywhere, then its integrals on any set converge to the integral of the limit.

theorem MeasureTheory.Integrable.tendsto_setIntegral_sup_neg_natCast {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → ℝ} (hf : Integrable f μ) (A : Set Ω) : Filter.Tendsto (fun (k : ℕ) => ∫ (ω : Ω) in A, max (f ω) (-↑k) ∂μ) Filter.atTop (nhds (∫ (ω : Ω) in A, f ω ∂μ))

The integrals of the truncations f ⊔ (-k) of an integrable function f converge to the integral of f.

theorem MeasureTheory.uniformIntegrable_of_le_condExp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {κ : Type u_3} {f : κ → Ω → ℝ} {g : Ω → ℝ} {c : ℝ} {m : κ → MeasurableSpace Ω} (hm : ∀ (i : κ), m i ≤ mΩ) (hg : Integrable g μ) (hf : ∀ (i : κ), AEStronglyMeasurable (f i) μ) (hcf : ∀ (i : κ), ∀ᵐ (ω : Ω) ∂μ, c ≤ f i ω) (hfg : ∀ (i : κ), f i ≤ᵐ[μ] μ[g | m i]) : UniformIntegrable f 1 μ

A family of functions which is bounded from below by a constant and such that each function is bounded from above by a conditional expectation of a fixed integrable function is uniformly integrable.

theorem MeasureTheory.Submartingale.integral_abs_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_3} [Preorder ι] {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : Submartingale X 𝓕 μ) {t s u : ι} (hts : t ≤ s) (hsu : s ≤ u) : ∫ (ω : Ω), |X s ω| ∂μ ≤ 2 * ∫ (ω : Ω), max (X u ω) 0 ∂μ - ∫ (ω : Ω), X t ω ∂μ

L¹ bound for a submartingale on an interval.

def ProbabilityTheory.regularitySet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] (T : Set ι) (X : ι → Ω → ℝ) (d : ι) : Set Ω

In this set, the process is bounded and has finitely many upcrossings (of any interval) in T before time d

Equations

• ProbabilityTheory.regularitySet T X d = {ω : Ω | (∀ (q r : ℚ), q < r → ω ∉ ProbabilityTheory.infiniteAlt T d X ↑q ↑r) ∧ ∃ (M : ℕ), ∀ s ∈ T ∩ Set.Iic d, |X s ω| ≤ ↑M + 1}

theorem ProbabilityTheory.regularitySet_anti {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {T : Set ι} {X : ι → Ω → ℝ} {d₁ d₂ : ι} (hd : d₁ ≤ d₂) : regularitySet T X d₂ ⊆ regularitySet T X d₁

theorem ProbabilityTheory.ae_mem_regularitySet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {T : Set ι} (hT : T.Countable) (d : ι) (hdT : d ∈ T) : ∀ᵐ (ω : Ω) ∂μ, ω ∈ regularitySet T X d

theorem ProbabilityTheory.ae_mem_all_regularitySet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {T T' : Set ι} (hT : T.Countable) (hT' : T'.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ d ∈ T', ω ∈ regularitySet T X d

theorem ProbabilityTheory.measurableSet_altSet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [OrderBot ι] (hX : IsRealQuasimartingale 𝓕 X μ) (d : ι) (F : Finset ι) (hF : ∀ i ∈ F, i ≤ d) {q r : ℚ} (_hqr : q < r) (m : ℕ) : MeasurableSet (altSet X F (↑q) (↑r) m)

theorem ProbabilityTheory.measurableSet_infiniteAlt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [OrderBot ι] (hX : IsRealQuasimartingale 𝓕 X μ) {T : Set ι} (hT : T.Countable) (d : ι) {q r : ℚ} (hqr : q < r) : MeasurableSet (infiniteAlt T d X ↑q ↑r)

theorem ProbabilityTheory.measurableSet_regularitySet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [OrderBot ι] (hX : IsRealQuasimartingale 𝓕 X μ) {T : Set ι} (hT : T.Countable) (d : ι) : MeasurableSet (regularitySet T X d)

theorem ProbabilityTheory.right_limit_of_mem_regularitySet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} (x d : ι) {ω : Ω} (hxd : x < d) (hω : ω ∈ regularitySet T X d) : ∃ (l : ℝ), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (T ∩ Set.Ioi x)) (nhds l)

theorem ProbabilityTheory.left_limit_of_mem_regularitySet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} (x d : ι) {ω : Ω} (hxle : x ≤ d) (hω : ω ∈ regularitySet T X d) : ∃ (l : ℝ), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (T ∩ Set.Iio x)) (nhds l)

Regularity families

A regularity family for a process X along a set of times T is an antitone family of events R d such that on R d, the path of X along T has left and right limits at all times before d. The main example is regularitySet T X for a real process X.

From such a family we define the events regularitySetRight T R d, on which the paths are regular up to a time slightly after d. These are the events used to define the modifications of X.

def ProbabilityTheory.regularitySetRight {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] (T : Set ι) (R : ι → Set Ω) (d : ι) : Set Ω

The set of ω that belong to some R s, for s ∈ T with s > d or for s ≥ d isolated on the right (𝓝[>] s = ⊥: s is maximal or has a successor). Here R is an antitone family of sets, for example regularitySet T X for a real process X.

If d is not isolated on the right and T is dense, this is the set of ω that belong to R s for some s ∈ T with s > d (see regularitySetRight_eq_biUnion_gt). If d is isolated on the right, this is R d (see regularitySetRight_of_nhdsGT_eq_bot).

Equations

• ProbabilityTheory.regularitySetRight T R d = ⋃ s ∈ T ∩ Set.Ioi d ∪ {s : ι | nhdsWithin s (Set.Ioi s) = ⊥} ∩ Set.Ici d, R s

theorem ProbabilityTheory.mem_regularitySetRight_iff {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} {ω : Ω} : ω ∈ regularitySetRight T R d ↔ ∃ (s : ι), (s ∈ T ∧ d < s ∨ nhdsWithin s (Set.Ioi s) = ⊥ ∧ d ≤ s) ∧ ω ∈ R s

theorem ProbabilityTheory.regularitySetRight_of_nhdsGT_eq_bot {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} (hR : Antitone R) (hd : nhdsWithin d (Set.Ioi d) = ⊥) : regularitySetRight T R d = R d

theorem ProbabilityTheory.regularitySetRight_eq_biUnion_lt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} (hR : Antitone R) {t : ι} [hd : (nhdsWithin d (Set.Ioi d)).NeBot] (hdt : d < t) (hT : ∀ (s : ι), d < s → ∃ u ∈ T, d < u ∧ u ≤ s) : regularitySetRight T R d = ⋃ d' ∈ T ∩ Set.Ioc d t, R d'

theorem ProbabilityTheory.regularitySetRight_eq_biUnion_gt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} (hR : Antitone R) [hd : (nhdsWithin d (Set.Ioi d)).NeBot] (hT : ∀ (s : ι), d < s → ∃ u ∈ T, d < u ∧ u ≤ s) : regularitySetRight T R d = ⋃ d' ∈ T ∩ Set.Ioi d, R d'

theorem ProbabilityTheory.regularitySetRight_anti {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d₁ d₂ : ι} (hd : d₁ ≤ d₂) : regularitySetRight T R d₂ ⊆ regularitySetRight T R d₁

theorem ProbabilityTheory.ae_mem_regularitySetRight {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} (hR : ∀ᵐ (ω : Ω) ∂μ, ∀ d ∈ T ∪ {s : ι | nhdsWithin s (Set.Ioi s) = ⊥}, ω ∈ R d) (hTcof : ∀ (x : ι), ¬IsMax x → ∃ s ∈ T, x < s) : ∀ᵐ (ω : Ω) ∂μ, ∀ (d : ι), ω ∈ regularitySetRight T R d

If almost surely ω belongs to R d for all d ∈ T and all d isolated on the right, then almost surely ω belongs to all the sets regularitySetRight T R d.

theorem ProbabilityTheory.measurableSet_of_forall_gt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] [OrderTopology ι] [𝓕.IsRightContinuous] {t : ι} [(nhdsWithin t (Set.Ioi t)).NeBot] {A : Set Ω} (h : ∀ (s : ι), t < s → MeasurableSet A) : MeasurableSet A

For a right-continuous filtration and a time t that is not isolated on the right, a set that is 𝓕 s-measurable for every s > t is already 𝓕 t-measurable, since 𝓕 t = ⨅ s > t, 𝓕 s.

theorem ProbabilityTheory.measurableSet_regularitySetRight {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} [OrderTopology ι] [𝓕.IsRightContinuous] (hR : Antitone R) (hRm : ∀ (d : ι), MeasurableSet (R d)) (hT : T.Countable) (hTd : Dense T) (d : ι) : MeasurableSet (regularitySetRight T R d)

theorem ProbabilityTheory.measurableSet_regularitySetRight' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} [OrderTopology ι] [SecondCountableTopology ι] (hRm : ∀ (d : ι), MeasurableSet (R d)) (hT : T.Countable) (d : ι) : MeasurableSet (regularitySetRight T R d)

theorem ProbabilityTheory.eventually_mem_regularitySetRight_of_mem {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} {ω : Ω} [OrderTopology ι] (hω : ω ∈ regularitySetRight T R d) : ∀ᶠ (y : ι) in nhdsWithin d (Set.Ioi d), ω ∈ regularitySetRight T R y

structure ProbabilityTheory.IsRegularityFamily {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {E : Type u_3} [TopologicalSpace E] (T : Set ι) (X : ι → Ω → E) (R : ι → Set Ω) : Prop

An antitone family of events R d is a regularity family for a process X along a set of times T if on R d, the path of X along T has right limits at all times before d and left limits at all times up to d.

• anti : Antitone R
• exists_tendsto_nhdsGT ⦃x d : ι⦄ ⦃ω : Ω⦄ (hxd : x < d) (hω : ω ∈ R d) : ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (T ∩ Set.Ioi x)) (nhds l)
• exists_tendsto_nhdsLT ⦃x d : ι⦄ ⦃ω : Ω⦄ (hxd : x ≤ d) (hω : ω ∈ R d) : ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (T ∩ Set.Iio x)) (nhds l)

theorem ProbabilityTheory.IsRegularityFamily.right_limit_of_mem_regularitySetRight {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} {ω : Ω} {E : Type u_3} [TopologicalSpace E] {X : ι → Ω → E} (hR : IsRegularityFamily T X R) {y : ι} (hω : ω ∈ regularitySetRight T R d) (hyd : y ≤ d) : ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin y (T ∩ Set.Ioi y)) (nhds l)

theorem ProbabilityTheory.IsRegularityFamily.left_limit_of_mem_regularitySetRight {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} {ω : Ω} {E : Type u_3} [TopologicalSpace E] {X : ι → Ω → E} (hR : IsRegularityFamily T X R) {y : ι} (hω : ω ∈ regularitySetRight T R d) (hyd : y ≤ d) : ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin y (T ∩ Set.Iio y)) (nhds l)

theorem ProbabilityTheory.IsRegularityFamily.tendsto_nhdsGT_rightLimWithin {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} {ω : Ω} [OrderTopology ι] {E : Type u_3} [TopologicalSpace E] {X : ι → Ω → E} (hR : IsRegularityFamily T X R) (hω : ω ∈ regularitySetRight T R d) : Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin d (T ∩ Set.Ioi d)) (nhds (Function.rightLimWithin (fun (x : ι) => X x ω) T d))

theorem ProbabilityTheory.IsRegularityFamily.tendsto_nhdsLT_leftLimWithin {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} {ω : Ω} [OrderTopology ι] {E : Type u_3} [TopologicalSpace E] {X : ι → Ω → E} (hR : IsRegularityFamily T X R) (hω : ω ∈ regularitySetRight T R d) : Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin d (T ∩ Set.Iio d)) (nhds (Function.leftLimWithin (fun (x : ι) => X x ω) T d))

theorem ProbabilityTheory.IsRegularityFamily.continuousWithinAt_rightLimWithin {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] {T : Set ι} {R : ι → Set Ω} {d : ι} {ω : Ω} [OrderTopology ι] {E : Type u_3} [TopologicalSpace E] {X : ι → Ω → E} (hR : IsRegularityFamily T X R) [T3Space E] (hTd : Dense T) (hT : ∀ (y : ι), nhdsWithin y (Set.Ioi y) = ⊥ → y ∈ T) (hω : ω ∈ regularitySetRight T R d) : ContinuousWithinAt (Function.rightLimWithin (fun (x : ι) => X x ω) T) (Set.Ici d) d

Pathwise regularization

For a fixed path h : ι → F admitting one-sided limits along a dense set T, the right-limit regularization r is right-continuous and inherits the left limits of h.

The regularization r y is the limit of h along T from the right of y, unless y is isolated on the right, in which case r y = h y (hypothesis hr') and we need y ∈ T.

theorem ProbabilityTheory.tendsto_rightLim_nhdsLT {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {F : Type u_3} [TopologicalSpace F] [RegularSpace F] {T : Set ι} {h r : ι → F} {x : ι} (hTd : Dense T) (hT : ∀ (y : ι), nhdsWithin y (Set.Ioi y) = ⊥ → y ∈ T) (hr : ∀ᶠ (y : ι) in nhdsWithin x (Set.Iio x), Filter.Tendsto h (nhdsWithin y (T ∩ Set.Ioi y)) (nhds (r y))) (hr' : ∀ (y : ι), nhdsWithin y (Set.Ioi y) = ⊥ → r y = h y) {L : F} (hL : Filter.Tendsto h (nhdsWithin x (T ∩ Set.Iio x)) (nhds L)) : Filter.Tendsto r (nhdsWithin x (Set.Iio x)) (nhds L)

The right-limit regularization inherits left limits of h along T.

theorem ProbabilityTheory.tendsto_rightLim_comp_of_lt {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {F : Type u_3} [TopologicalSpace F] [RegularSpace F] {T : Set ι} {h r : ι → F} {x : ι} (hTd : Dense T) {T' : Set ι} (hTT' : T ⊆ T') (hr : ∀ (y : ι), Filter.Tendsto h (nhdsWithin y (T ∩ Set.Ioi y)) (nhds (r y))) (hr' : ∀ (y : ι), nhdsWithin y (Set.Ioi y) = ⊥ → r y = h y) {u : ℕ → ι} {L : F} (hux : ∀ (k : ℕ), u k < x) (hutend : Filter.Tendsto u Filter.atTop (nhds x)) (huT' : ∀ (k : ℕ), nhdsWithin (u k) (Set.Ioi (u k)) = ⊥ → u k ∈ T') (hL : Filter.Tendsto h (nhdsWithin x (T' ∩ Set.Iio x)) (nhds L)) : Filter.Tendsto (fun (k : ℕ) => r (u k)) Filter.atTop (nhds L)

Along a strictly increasing sequence u → x from the left, the regularized values r (u k) tend to the left limit of h at x along T' ⊇ T.

theorem ProbabilityTheory.tendsto_rightLim_comp_of_gt {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {F : Type u_3} [TopologicalSpace F] [RegularSpace F] {T : Set ι} {h r : ι → F} {x : ι} (hTd : Dense T) {T' : Set ι} (hTT' : T ⊆ T') (hr : ∀ (y : ι), Filter.Tendsto h (nhdsWithin y (T ∩ Set.Ioi y)) (nhds (r y))) (hr' : ∀ (y : ι), nhdsWithin y (Set.Ioi y) = ⊥ → r y = h y) {u : ℕ → ι} {L : F} (hux : ∀ (k : ℕ), x < u k) (hutend : Filter.Tendsto u Filter.atTop (nhds x)) (huT' : ∀ (k : ℕ), nhdsWithin (u k) (Set.Ioi (u k)) = ⊥ → u k ∈ T') (hL : Filter.Tendsto h (nhdsWithin x (T' ∩ Set.Ioi x)) (nhds L)) : Filter.Tendsto (fun (k : ℕ) => r (u k)) Filter.atTop (nhds L)

Along a strictly decreasing sequence u → x from the right, the regularized values r (u k) tend to the right limit of h at x along T' ⊇ T.

Uncountable sets accumulate from the right

theorem ProbabilityTheory.exists_seq_gt_tendsto_of_not_countable {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {A : Set ι} (hA : ¬A.Countable) : ∃ (p : ι) (u : ℕ → ι), (∀ (k : ℕ), u k ∈ A) ∧ (∀ (k : ℕ), p < u k) ∧ Filter.Tendsto u Filter.atTop (nhds p)

Any uncountable set in a second-countable linear order admits a sequence of its elements converging to a point from the right.

theorem ProbabilityTheory.isRegularityFamily_regularitySet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → ℝ} {T : Set ι} : IsRegularityFamily T X (regularitySet T X)

The events regularitySet T X d form a regularity family for the real process X.

theorem ProbabilityTheory.ae_mem_all_regularitySet_union_nhdsGT_eq_bot {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → ℝ} {T : Set ι} [OrderBot ι] [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (hT : T.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ d ∈ T ∪ {s : ι | nhdsWithin s (Set.Ioi s) = ⊥}, ω ∈ regularitySet T X d

Almost surely, ω belongs to regularitySet T X d for all d ∈ T and all d isolated on the right.

theorem ProbabilityTheory.IsRealQuasimartingale.ae_mem_regularitySetRight {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → ℝ} {T : Set ι} [OrderBot ι] [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (hT : T.Countable) (hTcof : ∀ (x : ι), ¬IsMax x → ∃ s ∈ T, x < s) : ∀ᵐ (ω : Ω) ∂μ, ∀ (d : ι), ω ∈ regularitySetRight T (regularitySet T X) d

theorem ProbabilityTheory.ae_right_limit {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → ℝ} {T : Set ι} [OrderBot ι] [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (hT : T.Countable) (hTcof : ∀ (x : ι), ¬IsMax x → ∃ d ∈ T, x < d) : ∀ᵐ (ω : Ω) ∂μ, ∀ (x : ι), ∃ (l : ℝ), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (T ∩ Set.Ioi x)) (nhds l)

theorem ProbabilityTheory.ae_left_limit {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {T : Set ι} (hT : T.Countable) (hTcof : ∀ (x : ι), ¬IsMax x → ∃ d ∈ T, x ≤ d) : ∀ᵐ (ω : Ω) ∂μ, ∀ (x : ι), ∃ (l : ℝ), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (T ∩ Set.Iio x)) (nhds l)

theorem ProbabilityTheory.countable_not_rightLimWithin_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {T : Set ι} (hTc : T.Countable) (hTd : Dense T) : {t : ι | ¬(fun (ω : Ω) => Function.rightLimWithin (fun (x : ι) => X x ω) T t) =ᵐ[μ] X t}.Countable

The set of points where the right limit along a countable dense set T disagrees with X is countable.

Times used to define the modifications

noncomputable def ProbabilityTheory.regularityTimes (ι : Type u_3) [Preorder ι] [TopologicalSpace ι] [SecondCountableTopology ι] : Set ι

A countable dense set of times which contains all the times that are isolated on the right (the maximal element and the times which have a successor, if any). The modifications of a quasimartingale are defined from the limits of the process along this set.

At a time t isolated on the right, the modification is X t: we need those times in the set to ensure that the paths of the process restricted to the set, which have one-sided limits almost surely, control these values. If ι is densely ordered without maximal element, this set is denseCountable ι.

Equations

• ProbabilityTheory.regularityTimes ι = denseCountable ι ∪ {t : ι | nhdsWithin t (Set.Ioi t) = ⊥}

theorem ProbabilityTheory.mem_regularityTimes_of_nhdsGT_eq_bot {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] {t : ι} (ht : nhdsWithin t (Set.Ioi t) = ⊥) : t ∈ regularityTimes ι

theorem ProbabilityTheory.dense_regularityTimes {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] : Dense (regularityTimes ι)

theorem ProbabilityTheory.countable_regularityTimes {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] : (regularityTimes ι).Countable

Modifications defined from a regularity family

Let X be a process with values in a normed group and let R be a regularity family for X along regularityTimes ι. We define two processes from the right limits of X along regularityTimes ι.

rightContModifOf R X has the following properties:

• it is right-continuous, and has left limits at t on regularitySetRight (regularityTimes ι) R t
• if the filtration is right-continuous and the sets R d are 𝓕 d-measurable, then it is strongly adapted.

cadlagModifOf R X has the following properties:

• it is càdlàg
• if the filtration is right-continuous and complete, the sets R d are 𝓕 d-measurable and almost sure, then it is strongly adapted.

If the events R d are almost sure, the two processes are indistinguishable and are equal to X t almost surely

• at all times t which are isolated on the right
• at all times t at which X is right-continuous in probability
• at all times if X is a martingale with respect to a right-continuous filtration.

These constructions are used for real quasimartingales below, with R = regularitySet _ X, and for martingales with values in a Banach space.

theorem ProbabilityTheory.stronglyMeasurable_of_forall_gt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] [OrderTopology ι] {E : Type u_3} [NormedAddCommGroup E] [𝓕.IsRightContinuous] {t : ι} [(nhdsWithin t (Set.Ioi t)).NeBot] {f : Ω → E} (h : ∀ (s : ι), t < s → MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable f

For a right-continuous filtration and a time t that is not isolated on the right, a function that is 𝓕 s-strongly measurable for every s > t is 𝓕 t-strongly measurable.

theorem ProbabilityTheory.stronglyMeasurable_indicator_rightLimWithin {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {T : Set ι} [FirstCountableTopology ι] {m : MeasurableSpace Ω} {G : Set Ω} (hG : MeasurableSet G) {t : ι} {S : Set ι} (hS : S ∈ nhdsWithin t (T ∩ Set.Ioi t)) (hXS : ∀ s ∈ S, MeasureTheory.StronglyMeasurable (X s)) (hXt : MeasureTheory.StronglyMeasurable (X t)) (hlim : ∀ ω ∈ G, ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin t (T ∩ Set.Ioi t)) (nhds l)) : MeasureTheory.StronglyMeasurable (G.indicator fun (ω : Ω) => Function.rightLimWithin (fun (x : ι) => X x ω) T t)

The right limit of a process along T at time t, restricted to a measurable set on which that limit exists, is strongly measurable with respect to a sigma-algebra m as soon as the process is m-strongly measurable at all times of a right neighborhood of t in T.

noncomputable def ProbabilityTheory.rightContModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] (R : ι → Set Ω) (X : ι → Ω → E) (t : ι) (ω : Ω) : E

The right-continuous modification of a process X with regularity family R, defined from the right limits of X along the countable dense set regularityTimes ι.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.rightContModifOf_eq_indicator {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] (R : ι → Set Ω) (X : ι → Ω → E) (t : ι) : rightContModifOf R X t = (regularitySetRight (regularityTimes ι) R t).indicator fun (ω : Ω) => Function.rightLimWithin (fun (x : ι) => X x ω) (regularityTimes ι) t

theorem ProbabilityTheory.rightContModifOf_eq_zero {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} {x : ι} {ω : Ω} (hω : ω ∉ regularitySetRight (regularityTimes ι) R x) : (fun (x : ι) => rightContModifOf R X x ω) =ᶠ[nhdsWithin x (Set.Ioi x)] 0

theorem ProbabilityTheory.tendsto_rightContModifOf_rightLimWithin {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) {x : ι} {ω : Ω} (hω : ω ∈ regularitySetRight (regularityTimes ι) R x) : Filter.Tendsto (fun (x : ι) => rightContModifOf R X x ω) (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLimWithin (fun (x : ι) => X x ω) (regularityTimes ι) x))

theorem ProbabilityTheory.tendsto_rightContModifOf_leftLimWithin {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) {x : ι} {ω : Ω} (hω : ω ∈ regularitySetRight (regularityTimes ι) R x) : Filter.Tendsto (fun (x : ι) => rightContModifOf R X x ω) (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLimWithin (fun (x : ι) => X x ω) (regularityTimes ι) x))

theorem ProbabilityTheory.continuousWithinAt_rightContModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) (x : ι) (ω : Ω) : ContinuousWithinAt (fun (x : ι) => rightContModifOf R X x ω) (Set.Ioi x) x

The paths of rightContModifOf R X are right-continuous.

theorem ProbabilityTheory.stronglyMeasurable_rightContModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hRm : ∀ (d : ι), MeasurableSet (R d)) (t : ι) : MeasureTheory.StronglyMeasurable (rightContModifOf R X t)

theorem ProbabilityTheory.stronglyAdapted_rightContModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) [𝓕.IsRightContinuous] (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hRm : ∀ (d : ι), MeasurableSet (R d)) : MeasureTheory.StronglyAdapted 𝓕 (rightContModifOf R X)

theorem ProbabilityTheory.rightContModifOf_ae_eq_of_rightLimWithin_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t) {t : ι} (ht : (fun (ω : Ω) => Function.rightLimWithin (fun (x : ι) => X x ω) (regularityTimes ι) t) =ᵐ[μ] X t) : rightContModifOf R X t =ᵐ[μ] X t

theorem ProbabilityTheory.rightContModifOf_ae_eq_of_nhdsGT_eq_bot {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t) {t : ι} (ht : nhdsWithin t (Set.Ioi t) = ⊥) : rightContModifOf R X t =ᵐ[μ] X t

At a time t which is isolated on the right, rightContModifOf R X t is a.e. equal to X t.

theorem ProbabilityTheory.exists_seq_tendsto_rightContModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t) (hR : IsRegularityFamily (regularityTimes ι) X R) {t u : ι} [(nhdsWithin t (Set.Ioi t)).NeBot] (htu : t < u) : ∃ (w : ℕ → ι), (∀ (n : ℕ), t < w n) ∧ (∀ (n : ℕ), w n ≤ u) ∧ Filter.Tendsto w Filter.atTop (nhdsWithin t (Set.Ioi t)) ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => X (w n) ω) Filter.atTop (nhds (rightContModifOf R X t ω))

If t is not isolated on the right, there is a sequence of times w n ∈ (t, u] tending to t along which X converges almost surely to rightContModifOf R X t.

theorem ProbabilityTheory.rightContModifOf_ae_eq_of_tendstoInMeasure {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t) [MeasureTheory.IsFiniteMeasure μ] (hR : IsRegularityFamily (regularityTimes ι) X R) (hX : MeasureTheory.StronglyAdapted 𝓕 X) (t : ι) (hXRC : MeasureTheory.TendstoInMeasure μ X (nhdsWithin t (Set.Ioi t)) (X t)) : rightContModifOf R X t =ᵐ[μ] X t

At a time t at which X is right-continuous in probability, rightContModifOf R X t is a.e. equal to X t.

theorem MeasureTheory.Martingale.rightContModifOf_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ ProbabilityTheory.regularitySetRight (ProbabilityTheory.regularityTimes ι) R t) [NormedSpace ℝ E] [CompleteSpace E] [IsFiniteMeasure μ] [𝓕.IsRightContinuous] (hX : Martingale X 𝓕 μ) (hR : ProbabilityTheory.IsRegularityFamily (ProbabilityTheory.regularityTimes ι) X R) (hRm : ∀ (d : ι), MeasurableSet (R d)) (t : ι) : ProbabilityTheory.rightContModifOf R X t =ᵐ[μ] X t

The right-continuous modification of a martingale with respect to a right-continuous filtration is a modification.

noncomputable def ProbabilityTheory.cadlagModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] (R : ι → Set Ω) (X : ι → Ω → E) (t : ι) (ω : Ω) : E

The càdlàg modification of a process X with regularity family R, defined from the right limits of X along the countable dense set regularityTimes ι.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.cadlagModifOf_ae_eq_rightContModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t) : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), cadlagModifOf R X t ω = rightContModifOf R X t ω

theorem ProbabilityTheory.cadlagModifOf_ae_eq_of_rightContModifOf_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t) {t : ι} (ht : rightContModifOf R X t =ᵐ[μ] X t) : cadlagModifOf R X t =ᵐ[μ] X t

theorem ProbabilityTheory.measurableSet_forall_mem_regularitySetRight {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {R : ι → Set Ω} (hRm : ∀ (d : ι), MeasurableSet (R d)) : MeasurableSet {ω : Ω | ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t}

theorem ProbabilityTheory.continuousWithinAt_cadlagModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) (x : ι) (ω : Ω) : ContinuousWithinAt (fun (x : ι) => cadlagModifOf R X x ω) (Set.Ioi x) x

theorem ProbabilityTheory.exists_tendsto_nhdsLT_cadlagModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) (x : ι) (ω : Ω) : ∃ (l : E), Filter.Tendsto (fun (x : ι) => cadlagModifOf R X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)

theorem ProbabilityTheory.isCadlag_cadlagModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) (ω : Ω) : IsCadlag fun (x : ι) => cadlagModifOf R X x ω

The paths of cadlagModifOf R X are càdlàg.

theorem ProbabilityTheory.stronglyMeasurable_cadlagModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hRm : ∀ (d : ι), MeasurableSet (R d)) (t : ι) : MeasureTheory.StronglyMeasurable (cadlagModifOf R X t)

theorem ProbabilityTheory.stronglyAdapted_cadlagModifOf {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {R : ι → Set Ω} (hR : IsRegularityFamily (regularityTimes ι) X R) [𝓕.IsRightContinuous] [𝓕.IsComplete μ] (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hRm : ∀ (d : ι), MeasurableSet (R d)) (hRae : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) R t) : MeasureTheory.StronglyAdapted 𝓕 (cadlagModifOf R X)

Right-continuous modification of a quasimartingale

For a real quasimartingale X we define a process rightContModifReal X with the following properties:

• rightContModifReal X is right-continuous
• rightContModifReal X has left limits almost everywhere
• for all t outside a countable set, rightContModifReal X t =ᵐ[μ] X t
• if t is isolated on the right (for example if t is a maximal element of ι or has a successor), then rightContModifReal X t =ᵐ[μ] X t
• if X is right-continuous in probability, then rightContModifReal X is a modification of X.
• if the filtration is right-continuous, then rightContModifReal X is adapted.

Note that if X is not right-continuous in probability, we can still obtain a modification by changing the value of rightContModifReal X on a countable set of times, with the drawback that the right-continuity then holds only outside that countable set.

noncomputable def ProbabilityTheory.rightContModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] (X : ι → Ω → ℝ) : ι → Ω → ℝ

The right-continuous modification of a real quasimartingale, defined from the right limits along the countable dense set regularityTimes ι.

Equations

• ProbabilityTheory.rightContModifReal X = ProbabilityTheory.rightContModifOf (ProbabilityTheory.regularitySet (ProbabilityTheory.regularityTimes ι) X) X

theorem ProbabilityTheory.continuousWithinAt_rightContModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} (x : ι) (ω : Ω) : ContinuousWithinAt (fun (x : ι) => rightContModifReal X x ω) (Set.Ioi x) x

theorem ProbabilityTheory.measurable_rightContModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] (hX : IsRealQuasimartingale 𝓕 X μ) (t : ι) : Measurable (rightContModifReal X t)

theorem ProbabilityTheory.stronglyAdapted_rightContModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [𝓕.IsRightContinuous] (hX : IsRealQuasimartingale 𝓕 X μ) : MeasureTheory.StronglyAdapted 𝓕 (rightContModifReal X)

theorem ProbabilityTheory.adapted_rightContModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [𝓕.IsRightContinuous] (hX : IsRealQuasimartingale 𝓕 X μ) : MeasureTheory.Adapted 𝓕 (rightContModifReal X)

theorem ProbabilityTheory.IsRealQuasimartingale.ae_mem_regularitySetRight_regularityTimes {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ regularitySetRight (regularityTimes ι) (regularitySet (regularityTimes ι) X) t

Almost surely, ω belongs to all the events used to define the modifications of a real quasimartingale.

theorem ProbabilityTheory.rightContModifReal_ae_eq_of_rightLimWithin_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {t : ι} (ht : (fun (ω : Ω) => Function.rightLimWithin (fun (x : ι) => X x ω) (regularityTimes ι) t) =ᵐ[μ] X t) : rightContModifReal X t =ᵐ[μ] X t

theorem ProbabilityTheory.rightContModifReal_ae_eq_of_nhdsGT_eq_bot {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {t : ι} (ht : nhdsWithin t (Set.Ioi t) = ⊥) : rightContModifReal X t =ᵐ[μ] X t

At a time t which is isolated on the right, the right-continuous modification is a.e. equal to X t.

theorem ProbabilityTheory.rightContModifReal_ae_eq_of_isMax {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {t : ι} (ht : IsMax t) : rightContModifReal X t =ᵐ[μ] X t

At a maximal time t, the right-continuous modification is a.e. equal to X t.

theorem ProbabilityTheory.countable_not_rightContModifReal_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) : {t : ι | ¬rightContModifReal X t =ᵐ[μ] X t}.Countable

The set of points where the right modification of a real quasimartingale along a countable dense set T disagrees with X is countable.

theorem ProbabilityTheory.rightContModifReal_ae_eq_of_tendstoInMeasure {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (t : ι) (hXRC : MeasureTheory.TendstoInMeasure μ X (nhdsWithin t (Set.Ioi t)) (X t)) : rightContModifReal X t =ᵐ[μ] X t

Càdlàg modification of a quasimartingale

For a real quasimartingale X we define a process cadlagModifReal X with the following properties:

• cadlagModifReal X is càdlàg
• for all t outside a countable set, cadlagModifReal X t =ᵐ[μ] X t
• if t is isolated on the right (for example if t is a maximal element of ι or has a successor), then cadlagModifReal X t =ᵐ[μ] X t
• if X is right-continuous in probability, then cadlagModifReal X is a modification of X.
• if the filtration is right-continuous and complete, then cadlagModifReal X is adapted.

TODO: if t ↦ μ[X t] is right-continuous (in particular if X is a martingale), then cadlagModifReal X is a modification of X without the assumption that X is right-continuous in probability.

noncomputable def ProbabilityTheory.cadlagModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] (X : ι → Ω → ℝ) : ι → Ω → ℝ

The càdlàg modification of a real quasimartingale, defined from the right limits along the countable dense set regularityTimes ι.

Equations

• ProbabilityTheory.cadlagModifReal X = ProbabilityTheory.cadlagModifOf (ProbabilityTheory.regularitySet (ProbabilityTheory.regularityTimes ι) X) X

theorem ProbabilityTheory.continuousWithinAt_cadlagModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} (x : ι) (ω : Ω) : ContinuousWithinAt (fun (x : ι) => cadlagModifReal X x ω) (Set.Ioi x) x

theorem ProbabilityTheory.exists_tendsto_nhdsLT_cadlagModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} (x : ι) (ω : Ω) : ∃ (l : ℝ), Filter.Tendsto (fun (x : ι) => cadlagModifReal X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)

theorem ProbabilityTheory.isCadlag_cadlagModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} (ω : Ω) : IsCadlag fun (x : ι) => cadlagModifReal X x ω

theorem ProbabilityTheory.measurable_cadlagModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] (hX : IsRealQuasimartingale 𝓕 X μ) (t : ι) : Measurable (cadlagModifReal X t)

theorem ProbabilityTheory.cadlagModifReal_ae_eq_rightContModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), cadlagModifReal X t ω = rightContModifReal X t ω

theorem ProbabilityTheory.cadlagModifReal_ae_eq_of_rightContModifReal_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {t : ι} (ht : rightContModifReal X t =ᵐ[μ] X t) : cadlagModifReal X t =ᵐ[μ] X t

theorem ProbabilityTheory.cadlagModifReal_ae_eq_of_rightLimWithin_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {t : ι} (ht : (fun (ω : Ω) => Function.rightLimWithin (fun (x : ι) => X x ω) (regularityTimes ι) t) =ᵐ[μ] X t) : cadlagModifReal X t =ᵐ[μ] X t

theorem ProbabilityTheory.cadlagModifReal_ae_eq_of_nhdsGT_eq_bot {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {t : ι} (ht : nhdsWithin t (Set.Ioi t) = ⊥) : cadlagModifReal X t =ᵐ[μ] X t

At a time t which is isolated on the right, the càdlàg modification is a.e. equal to X t.

theorem ProbabilityTheory.cadlagModifReal_ae_eq_of_isMax {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {t : ι} (ht : IsMax t) : cadlagModifReal X t =ᵐ[μ] X t

At a maximal time t, the càdlàg modification is a.e. equal to X t.

theorem ProbabilityTheory.countable_not_cadlagModifReal_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) : {t : ι | ¬cadlagModifReal X t =ᵐ[μ] X t}.Countable

The set of points where the cadlag modification of a real quasimartingale along a countable dense set T disagrees with X is countable.

theorem ProbabilityTheory.cadlagModifReal_ae_eq_of_tendstoInMeasure {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (t : ι) (hXRC : MeasureTheory.TendstoInMeasure μ X (nhdsWithin t (Set.Ioi t)) (X t)) : cadlagModifReal X t =ᵐ[μ] X t

theorem ProbabilityTheory.stronglyAdapted_cadlagModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] [𝓕.IsRightContinuous] [𝓕.IsComplete μ] (hX : IsRealQuasimartingale 𝓕 X μ) : MeasureTheory.StronglyAdapted 𝓕 (cadlagModifReal X)

theorem ProbabilityTheory.adapted_cadlagModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] [𝓕.IsRightContinuous] [𝓕.IsComplete μ] (hX : IsRealQuasimartingale 𝓕 X μ) : MeasureTheory.Adapted 𝓕 (cadlagModifReal X)

theorem MeasureTheory.Martingale.integral_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SigmaFiniteFiltration μ 𝓕] {X : ι → Ω → ℝ} (hX : Martingale X 𝓕 μ) (i j : ι) : ∫ (ω : Ω), X i ω ∂μ = ∫ (ω : Ω), X j ω ∂μ

theorem ProbabilityTheory.exists_seq_tendsto_rightContModifReal {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : IsRealQuasimartingale 𝓕 X μ) {t u : ι} [(nhdsWithin t (Set.Ioi t)).NeBot] (htu : t < u) : ∃ (w : ℕ → ι), (∀ (n : ℕ), t < w n) ∧ (∀ (n : ℕ), w n ≤ u) ∧ Filter.Tendsto w Filter.atTop (nhdsWithin t (Set.Ioi t)) ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => X (w n) ω) Filter.atTop (nhds (rightContModifReal X t ω))

If t is not isolated on the right, there is a sequence of times w n ∈ (t, u] tending to t along which a quasimartingale X converges almost surely to rightContModifReal X t.

theorem MeasureTheory.Martingale.rightContModifReal_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [IsFiniteMeasure μ] {X : ι → Ω → ℝ} [𝓕.IsRightContinuous] (hX : Martingale X 𝓕 μ) (t : ι) : ProbabilityTheory.rightContModifReal X t =ᵐ[μ] X t

The right-continuous modification of a martingale with respect to a right-continuous filtration is a modification.

theorem MeasureTheory.Martingale.cadlagModifReal_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [IsFiniteMeasure μ] {X : ι → Ω → ℝ} [𝓕.IsRightContinuous] (hX : Martingale X 𝓕 μ) (t : ι) : ProbabilityTheory.cadlagModifReal X t =ᵐ[μ] X t

The càdlàg modification of a martingale with respect to a right-continuous filtration is a modification.

theorem MeasureTheory.Submartingale.rightContModifReal_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [IsFiniteMeasure μ] {X : ι → Ω → ℝ} [𝓕.IsRightContinuous] (hX : Submartingale X 𝓕 μ) (t : ι) (hXRC : Filter.Tendsto (fun (s : ι) => ∫ (x : Ω), X s x ∂μ) (nhdsWithin t (Set.Ioi t)) (nhds (∫ (x : Ω), X t x ∂μ))) : ProbabilityTheory.rightContModifReal X t =ᵐ[μ] X t

The right-continuous modification of a submartingale with respect to a right-continuous filtration is a modification at the times where the expectation is right-continuous.

theorem MeasureTheory.Submartingale.cadlagModifReal_ae_eq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [IsFiniteMeasure μ] {X : ι → Ω → ℝ} [𝓕.IsRightContinuous] (hX : Submartingale X 𝓕 μ) (t : ι) (hXRC : Filter.Tendsto (fun (s : ι) => ∫ (x : Ω), X s x ∂μ) (nhdsWithin t (Set.Ioi t)) (nhds (∫ (x : Ω), X t x ∂μ))) : ProbabilityTheory.cadlagModifReal X t =ᵐ[μ] X t

The càdlàg modification of a submartingale with respect to a right-continuous filtration is a modification at the times where the expectation is right-continuous.