Progressively Measurable σ-algebra

This file defines the progressively measurable σ-algebra associated to a filtration, as well as the notion of predictable processes. We prove that predictable processes are progressively measurable and adapted. We also give an equivalent characterization of predictability for discrete processes.

Main definitions

• Filtration.rightCont: The right continuation of a filtration.
• Filtration.Predictable: The predictable σ-algebra associated to a filtration.
• Filtration.IsPredictable: A process is predictable if it is measurable with respect to the predictable σ-algebra.

Main results

• Filtration.IsPredictable.progMeasurable: A predictable process is progressively measurable.
• Filtration.IsPredictable.measurable_succ: u is a discrete predictable process iff u (n + 1) is 𝓕 n-measurable and u 0 is 𝓕 0-measurable.
• MeasureTheory.StronglyAdapted.isPredictable_of_leftContinuous: A left-continuous adapted process is predictable if the index set is DenselyOrdered.

Implementation note

To avoid requiring a TopologicalSpace instance on ι in the definition of rightCont, 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

  letI := Preorder.topology ι
  haveI : OrderTopology ι := ⟨rfl⟩

Notation

• Given a filtration 𝓕, its right continuation is denoted 𝓕₊ (type ₊ with ;_+).

theorem MeasureTheory.IsStronglyPredictable.const {Ω : Type u_2} {ι : Type u_4} {E : Type u_5} [Preorder ι] [OrderBot ι] [TopologicalSpace E] {c : E} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} : IsStronglyPredictable 𝓕 fun (x : ι) (x_1 : Ω) => c

theorem MeasureTheory.IsStronglyPredictable.mul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Mul E] [ContinuousMul E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) (hY : IsStronglyPredictable 𝓕 Y) : IsStronglyPredictable 𝓕 (X * Y)

theorem MeasureTheory.IsStronglyPredictable.add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Add E] [ContinuousAdd E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) (hY : IsStronglyPredictable 𝓕 Y) : IsStronglyPredictable 𝓕 (X + Y)

theorem MeasureTheory.IsStronglyPredictable.fun_mul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Mul E] [ContinuousMul E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) (hY : IsStronglyPredictable 𝓕 Y) : IsStronglyPredictable 𝓕 fun (i : ι) (i_1 : Ω) => X i i_1 * Y i i_1

Eta-expanded form of MeasureTheory.IsStronglyPredictable.mul

theorem MeasureTheory.IsStronglyPredictable.fun_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Add E] [ContinuousAdd E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) (hY : IsStronglyPredictable 𝓕 Y) : IsStronglyPredictable 𝓕 fun (i : ι) (i_1 : Ω) => X i i_1 + Y i i_1

Eta-expanded form of MeasureTheory.IsStronglyPredictable.add

theorem MeasureTheory.IsStronglyPredictable.inv {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Inv E] [ContinuousInv E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) : IsStronglyPredictable 𝓕 X⁻¹

theorem MeasureTheory.IsStronglyPredictable.neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Neg E] [ContinuousNeg E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) : IsStronglyPredictable 𝓕 (-X)

theorem MeasureTheory.IsStronglyPredictable.fun_neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Neg E] [ContinuousNeg E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) : IsStronglyPredictable 𝓕 fun (i : ι) (i_1 : Ω) => -X i i_1

Eta-expanded form of MeasureTheory.IsStronglyPredictable.neg

theorem MeasureTheory.IsStronglyPredictable.fun_inv {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Inv E] [ContinuousInv E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) : IsStronglyPredictable 𝓕 fun (i : ι) (i_1 : Ω) => (X i i_1)⁻¹

Eta-expanded form of MeasureTheory.IsStronglyPredictable.inv

theorem MeasureTheory.IsStronglyPredictable.sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Sub E] [ContinuousSub E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) (hY : IsStronglyPredictable 𝓕 Y) : IsStronglyPredictable 𝓕 (X - Y)

theorem MeasureTheory.IsStronglyPredictable.fun_sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [Sub E] [ContinuousSub E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) (hY : IsStronglyPredictable 𝓕 Y) : IsStronglyPredictable 𝓕 fun (i : ι) (i_1 : Ω) => X i i_1 - Y i i_1

Eta-expanded form of MeasureTheory.IsStronglyPredictable.sub

theorem MeasureTheory.IsStronglyPredictable.const_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [SMul ℝ E] [ContinuousSMul ℝ E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (c : ℝ) (hX : IsStronglyPredictable 𝓕 X) : IsStronglyPredictable 𝓕 (c • X)

theorem MeasureTheory.IsStronglyPredictable.fun_const_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] [TopologicalSpace E] [SMul ℝ E] [ContinuousSMul ℝ E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} (c : ℝ) (hX : IsStronglyPredictable 𝓕 X) : IsStronglyPredictable 𝓕 fun (i : ι) (i_1 : Ω) => c • X i i_1

Eta-expanded form of MeasureTheory.IsStronglyPredictable.const_smul

theorem MeasureTheory.measurableSet_predictable_univ_prod {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {s : Set Ω} (hs : MeasurableSet s) : MeasurableSet (Set.univ ×ˢ s)

theorem MeasureTheory.measurableSet_predictable_Iic_prod {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {s : Set Ω} (hs : MeasurableSet s) {i : ι} : MeasurableSet (Set.Iic i ×ˢ s)

theorem MeasureTheory.IsStronglyPredictable.indicator_of_bot {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {E : Type u_3} [TopologicalSpace E] [Zero E] {X : ι → Ω → E} (hX : IsStronglyPredictable 𝓕 X) {s : Set Ω} (hs : MeasurableSet s) : IsStronglyPredictable 𝓕 fun (i : ι) => s.indicator (X i)

The product of a strongly predictable process with the indicator of a 𝓕 ⊥-measurable set is strongly predictable.

theorem MeasureTheory.StronglyAdapted.isStronglyPredictable_of_leftContinuous {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {β : Type u_3} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] {X : ι → Ω → β} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [DenselyOrdered ι] (h_adap : StronglyAdapted 𝓕 X) (h_cont : ∀ (ω : Ω) (a : ι), ContinuousWithinAt (fun (x : ι) => X x ω) (Set.Iio a) a) : IsStronglyPredictable 𝓕 X

theorem MeasureTheory.continuousWithinAt_indicator_coe_le {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {E : Type u_4} [TopologicalSpace E] [Zero E] (c : WithTop ι) (x : E) (a : ι) : ContinuousWithinAt ({t : ι | ↑t ≤ c}.indicator fun (x_1 : ι) => x) (Set.Iio a) a

The indicator of {t | t ≤ c} is left-continuous.

theorem MeasureTheory.continuousWithinAt_indicator_lt_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {E : Type u_4} [TopologicalSpace E] [Zero E] (c : WithTop ι) (x : E) (a : ι) : ContinuousWithinAt ({t : ι | c < ↑t}.indicator fun (x_1 : ι) => x) (Set.Iio a) a

The indicator of {t | c < t} is left-continuous.

theorem MeasureTheory.IsStronglyPredictable.stoppedProcess {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {β : Type u_3} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] {X : ι → Ω → β} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [TopologicalSpace.PseudoMetrizableSpace ι] [AddMonoid β] [ContinuousAdd β] {τ : Ω → WithTop ι} (hX : IsStronglyPredictable 𝓕 X) (hτ : IsStoppingTime 𝓕 τ) : IsStronglyPredictable 𝓕 (MeasureTheory.stoppedProcess X τ)

A strongly predictable process stopped at a stopping time is strongly predictable.

instance MeasureTheory.Filtration.IsComplete.toFinite {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] {𝓕 : Filtration ι m} {μ : Measure Ω} [SFinite μ] [𝓕.IsComplete μ] : 𝓕.IsComplete μ.toFinite

Completeness of a filtration only depends on the null sets of the measure, and μ.toFinite has the same null sets as μ.

def MeasureTheory.Filtration.predictableRectangles {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [OrderBot ι] (𝓕 : Filtration ι m) : Set (Set (ι × Ω))

The class of predictable rectangles associated to a filtration 𝓕 is the family of sets (i, j] ×ˢ A for i < j in ι and A ∈ 𝓕 i, together with {⊥} ×ˢ A for A ∈ 𝓕 ⊥.

Equations

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

theorem MeasureTheory.Filtration.singletonBot_prod_mem_predictableRectangles {Ω : Type u_4} {ι : Type u_5} {m : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] (𝓕 : Filtration ι m) {A : Set Ω} (hA : MeasurableSet A) : {⊥} ×ˢ A ∈ 𝓕.predictableRectangles

theorem MeasureTheory.Filtration.Ioc_prod_mem_predictableRectangles {Ω : Type u_4} {ι : Type u_5} {m : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] (𝓕 : Filtration ι m) (i j : ι) {A : Set Ω} (hA : MeasurableSet A) : Set.Ioc i j ×ˢ A ∈ 𝓕.predictableRectangles

theorem MeasureTheory.Filtration.isSetSemiring_predictableRectangles {Ω : Type u_4} {ι : Type u_5} {m : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] (𝓕 : Filtration ι m) : IsSetSemiring 𝓕.predictableRectangles

The predictable rectangles associated with a filtration form a semiring of sets.

theorem MeasureTheory.Filtration.predictable_le_prod {Ω : Type u_4} {m : MeasurableSpace Ω} {T : Type u_6} [LinearOrder T] [TopologicalSpace T] [OrderBot T] [OrderTopology T] [MeasurableSpace T] [BorelSpace T] (𝓕 : Filtration T m) : 𝓕.predictable ≤ Prod.instMeasurableSpace

The predictable σ-algebra is a sub-σ-algebra of the product σ-algebra.