Càdlàg modification of martingales with values in a Banach space

We extend the construction of the càdlàg modification of a real quasimartingale (see the file BrownianMotion.StochasticIntegral.Quasimartingale.CadlagModification) to martingales with values in a Banach space E, which is not assumed to be separable.

Main definitions

• rightContModif X: the right-continuous modification of X. It is strongly adapted if the filtration is right-continuous.
• cadlagModif X: the càdlàg modification of X. It is strongly adapted if the filtration is right-continuous and complete.

Those two processes are rightContModifOf R X and cadlagModifOf R X for the regularity family R = vectorRegularitySet (regularityTimes ι) X (see isRegularityFamily_vectorRegularitySet). The properties of the modifications which do not depend on the way the regularity family is built are proved in the file CadlagModification.

Main statements

• isCadlag_cadlagModif: the paths of cadlagModif X are càdlàg.
• Martingale.rightContModif_ae_eq, Martingale.cadlagModif_ae_eq: for a martingale X with respect to a right-continuous filtration, these processes are modifications of X.
• Martingale.exists_isCadlag_modification: a martingale with values in a Banach space, with respect to a right-continuous and complete filtration, has a modification which is a martingale with càdlàg paths.

theorem exists_tendsto_of_tendsto_norm_sub {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {l : Filter α} {x : α → E} {K D : Set E} (hK : IsCompact K) (hxK : ∀ᶠ (a : α) in l, x a ∈ K) (hD : K ⊆ closure D) (h : ∀ e ∈ D, ∃ (c : ℝ), Filter.Tendsto (fun (a : α) => ‖x a - e‖) l (nhds c)) : ∃ (y : E), Filter.Tendsto x l (nhds y)

If a function x takes values in a compact set K eventually along a filter l, and if the distances ‖x a - e‖ converge along l for all e in a set D whose closure contains K, then x converges along l.

theorem ProbabilityTheory.exists_isCompact_condExp_mem {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedSpace ℝ E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (ξ : MeasureTheory.SimpleFunc Ω E) : ∃ (K : Set E), IsCompact K ∧ ∀ m ≤ mΩ, ∀ᵐ (ω : Ω) ∂μ, μ[⇑ξ | m] ω ∈ K

The conditional expectations of a simple function take values in a fixed compact set.

theorem ProbabilityTheory.measure_exists_norm_gt_le {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {T : Set ι} [NormedSpace ℝ E] [CompleteSpace E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] {N : ι → Ω → E} (hN : MeasureTheory.Martingale N 𝓕 μ) (hT : T.Countable) (d : ι) {ε : ℝ} (hε : 0 < ε) : μ {ω : Ω | ∃ s ∈ T ∩ Set.Iic d, ε < ‖N s ω‖} ≤ ENNReal.ofReal ((8 * ∫ (ω : Ω), ‖N d ω‖ ∂μ) / ε)

Maximal inequality for the norm of a martingale along a countable set of times.

theorem ProbabilityTheory.ae_totallyBounded_image {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} {T : Set ι} [NormedSpace ℝ E] [CompleteSpace E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Martingale X 𝓕 μ) (hT : T.Countable) (d : ι) : ∀ᵐ (ω : Ω) ∂μ, TotallyBounded ((fun (x : ι) => X x ω) '' (T ∩ Set.Iic d))

Almost surely, the path of a martingale along a countable set of times which is bounded from above is totally bounded.

theorem MeasureTheory.Martingale.submartingale_norm_sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → E} [NormedSpace ℝ E] [CompleteSpace E] [IsFiniteMeasure μ] (hX : Martingale X 𝓕 μ) (e : E) : Submartingale (fun (t : ι) (ω : Ω) => ‖X t ω - e‖) 𝓕 μ

The distance of a martingale to a fixed vector is a submartingale.

noncomputable def ProbabilityTheory.denseValues {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] (T : Set ι) (X : ι → Ω → E) : Set E

A countable set whose closure contains the values of X t for all t ∈ T, if there is such a set (which is the case if T is countable and X is strongly adapted).

Equations

• ProbabilityTheory.denseValues T X = if h : TopologicalSpace.IsSeparable (⋃ t ∈ T, Set.range (X t)) then Exists.choose h else ∅

theorem ProbabilityTheory.countable_denseValues {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {T : Set ι} : (denseValues T X).Countable

theorem ProbabilityTheory.iUnion_range_subset_closure_denseValues {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {X : ι → Ω → E} {T : Set ι} (hT : T.Countable) (hX : ∀ t ∈ T, TopologicalSpace.IsSeparable (Set.range (X t))) : ⋃ t ∈ T, Set.range (X t) ⊆ closure (denseValues T X)

def ProbabilityTheory.vectorRegularitySet {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] (T : Set ι) (X : ι → Ω → E) (d : ι) : Set Ω

In this set, the path of the process along T before time d is totally bounded, and its distance to any point e of the countable set denseValues T X is regular: ω belongs to the regularitySet of the real process ‖X t - e‖. We also require that the closure of denseValues T X contains the values of X along T, which does not depend on ω and is true as soon as T is countable and X is strongly adapted.

On this set, the path of the process along T has left and right limits at all times before d: see right_limit_of_mem_vectorRegularitySet and left_limit_of_mem_vectorRegularitySet.

Equations

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

theorem ProbabilityTheory.vectorRegularitySet_anti {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} {T : Set ι} {d₁ d₂ : ι} (hd : d₁ ≤ d₂) : vectorRegularitySet T X d₂ ⊆ vectorRegularitySet T X d₁

theorem ProbabilityTheory.measurableSet_totallyBounded_image {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {T : Set ι} (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hT : T.Countable) (d : ι) : MeasurableSet {ω : Ω | TotallyBounded ((fun (x : ι) => X x ω) '' (T ∩ Set.Iic d))}

theorem ProbabilityTheory.measurableSet_vectorRegularitySet {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} {T : Set ι} [NormedSpace ℝ E] [CompleteSpace E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Martingale X 𝓕 μ) (hT : T.Countable) (d : ι) : MeasurableSet (vectorRegularitySet T X d)

theorem ProbabilityTheory.ae_mem_all_vectorRegularitySet {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} {T : Set ι} [NormedSpace ℝ E] [CompleteSpace E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Martingale X 𝓕 μ) {T' : Set ι} (hT : T.Countable) (hT' : T'.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ d ∈ T', ω ∈ vectorRegularitySet T X d

theorem ProbabilityTheory.exists_isCompact_of_mem_vectorRegularitySet {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} {T : Set ι} [CompleteSpace E] {d : ι} {ω : Ω} (hω : ω ∈ vectorRegularitySet T X d) : ∃ (K : Set E), IsCompact K ∧ K ⊆ closure (denseValues T X) ∧ ∀ s ∈ T ∩ Set.Iic d, X s ω ∈ K

On vectorRegularitySet T X d, the path along T before d stays in a compact set, whose points are limits of points of denseValues T X.

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

theorem ProbabilityTheory.left_limit_of_mem_vectorRegularitySet {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} {T : Set ι} [TopologicalSpace ι] [CompleteSpace E] [OrderTopology ι] {x d : ι} {ω : Ω} (hxd : x ≤ d) (hω : ω ∈ vectorRegularitySet T X d) : ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (T ∩ Set.Iio x)) (nhds l)

theorem ProbabilityTheory.isRegularityFamily_vectorRegularitySet {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} {T : Set ι} [TopologicalSpace ι] [CompleteSpace E] [OrderTopology ι] : IsRegularityFamily T X (vectorRegularitySet T X)

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

Right-continuous and càdlàg modifications

The modifications are the processes rightContModifOf and cadlagModifOf for the regularity family vectorRegularitySet (regularityTimes ι) X. For a martingale X with values in a Banach space,

• rightContModif X is right-continuous, and has left limits almost everywhere
• cadlagModif X is càdlàg
• if the filtration is right-continuous, then rightContModif X is strongly adapted and both processes are modifications of X
• if the filtration is right-continuous and complete, then cadlagModif X is strongly adapted, hence a martingale.

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

The right-continuous modification of a martingale with values in a Banach space.

Equations

• ProbabilityTheory.rightContModif X = ProbabilityTheory.rightContModifOf (ProbabilityTheory.vectorRegularitySet (ProbabilityTheory.regularityTimes ι) X) X

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

The càdlàg modification of a martingale with values in a Banach space.

Equations

• ProbabilityTheory.cadlagModif X = ProbabilityTheory.cadlagModifOf (ProbabilityTheory.vectorRegularitySet (ProbabilityTheory.regularityTimes ι) X) X

theorem ProbabilityTheory.continuousWithinAt_rightContModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] (x : ι) (ω : Ω) : ContinuousWithinAt (fun (x : ι) => rightContModif X x ω) (Set.Ioi x) x

The paths of rightContModif X are right-continuous.

theorem ProbabilityTheory.isCadlag_cadlagModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] (ω : Ω) : IsCadlag fun (x : ι) => cadlagModif X x ω

The paths of cadlagModif X are càdlàg.

theorem MeasureTheory.Martingale.ae_mem_regularitySetRight_vectorRegularitySet {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [NormedSpace ℝ E] [OrderBot ι] [IsFiniteMeasure μ] (hX : Martingale X 𝓕 μ) : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), ω ∈ ProbabilityTheory.regularitySetRight (ProbabilityTheory.regularityTimes ι) (ProbabilityTheory.vectorRegularitySet (ProbabilityTheory.regularityTimes ι) X) t

Almost surely, ω belongs to all the events used to define the modifications of a martingale with values in a Banach space.

theorem ProbabilityTheory.stronglyMeasurable_rightContModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [NormedSpace ℝ E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Martingale X 𝓕 μ) (t : ι) : MeasureTheory.StronglyMeasurable (rightContModif X t)

theorem ProbabilityTheory.stronglyAdapted_rightContModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [NormedSpace ℝ E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] [𝓕.IsRightContinuous] (hX : MeasureTheory.Martingale X 𝓕 μ) : MeasureTheory.StronglyAdapted 𝓕 (rightContModif X)

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

The right-continuous modification of a martingale with values in a Banach space, with respect to a right-continuous filtration, is a modification.

theorem ProbabilityTheory.cadlagModif_ae_eq_rightContModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [NormedSpace ℝ E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Martingale X 𝓕 μ) : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : ι), cadlagModif X t ω = rightContModif X t ω

theorem ProbabilityTheory.stronglyMeasurable_cadlagModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [NormedSpace ℝ E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Martingale X 𝓕 μ) (t : ι) : MeasureTheory.StronglyMeasurable (cadlagModif X t)

theorem ProbabilityTheory.stronglyAdapted_cadlagModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [NormedSpace ℝ E] [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] [𝓕.IsRightContinuous] [𝓕.IsComplete μ] (hX : MeasureTheory.Martingale X 𝓕 μ) : MeasureTheory.StronglyAdapted 𝓕 (cadlagModif X)

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

The càdlàg modification of a martingale with values in a Banach space, with respect to a right-continuous filtration, is a modification.

theorem MeasureTheory.Martingale.martingale_cadlagModif {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [NormedSpace ℝ E] [OrderBot ι] [IsFiniteMeasure μ] [𝓕.IsRightContinuous] [𝓕.IsComplete μ] (hX : Martingale X 𝓕 μ) : Martingale (ProbabilityTheory.cadlagModif X) 𝓕 μ

The càdlàg modification of a martingale with values in a Banach space, with respect to a right-continuous and complete filtration, is a martingale.