Local properties of processes

theorem ProbabilityTheory.locally_and_of_isStable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [Zero E] [TopologicalSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} (hp : IsStable 𝓕 p) (hpX : p X) (hqX : Locally q 𝓕 X P) : Locally (fun (Y : ι → Ω → E) => p Y ∧ q Y) 𝓕 X P

theorem ProbabilityTheory.locally_of_ae {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [𝓕.IsComplete P] {p : (ι → E) → Prop} (hpX : ∀ᵐ (ω : Ω) ∂P, p fun (x : ι) => X x ω) (hp₀ : p 0) : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), p fun (x : ι) => X x ω) 𝓕 X P

If the filtration satisfies the usual conditions, then a property of the paths of a process that holds almost surely holds locally.

theorem ProbabilityTheory.Locally.ae {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} (p : (ι → E) → ι → Prop) (hp_congr : ∀ (X Y : ι → E) (i : ι), (∃ (k : ι), i < k ∧ ∀ j < k, X j = Y j) → (p X i ↔ p Y i)) (hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω) (i : ι), p (fun (x : ι) => X x ω) i) 𝓕 X P) : ∀ᵐ (ω : Ω) ∂P, ∀ (i : ι), p (fun (x : ι) => X x ω) i

theorem ProbabilityTheory.isStable_pathwise {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} (p : (ι → E) → ι → Prop) (hp_zero : ∀ (i : ι), p 0 i) (hp_stop : ∀ (X : ι → E) (a : ι), (∀ (i : ι), p X i) → ∀ (i : ι), a ≤ i → p (fun (x : ι) => X (min x a)) i) (hp_congr : ∀ (X Y : ι → E) (i : ι), (∃ (k : ι), i < k ∧ ∀ j < k, X j = Y j) → (p X i ↔ p Y i)) : IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (ω : Ω) (i : ι), p (fun (x : ι) => X x ω) i

theorem ProbabilityTheory.locally_iff_ae {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [𝓕.IsComplete P] (p : (ι → E) → ι → Prop) (hp_zero : ∀ (i : ι), p 0 i) (hp_congr : ∀ (X Y : ι → E) (i : ι), (∃ (k : ι), i < k ∧ ∀ j < k, X j = Y j) → (p X i ↔ p Y i)) : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω) (i : ι), p (fun (x : ι) => X x ω) i) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, ∀ (i : ι), p (fun (x : ι) => X x ω) i

theorem ProbabilityTheory.Locally.rightContinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] (hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) 𝓕 X P) : ∀ᵐ (ω : Ω) ∂P, IsRightContinuous fun (x : ι) => X x ω

theorem ProbabilityTheory.Locally.left_limit {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] (hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω) (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)) 𝓕 X P) : ∀ᵐ (ω : Ω) ∂P, ∀ (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)

theorem ProbabilityTheory.Locally.isCadlag {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] (hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P) : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => X x ω

theorem ProbabilityTheory.Locally.continuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] (hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), Continuous fun (x : ι) => X x ω) 𝓕 X P) : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω

theorem ProbabilityTheory.isStable_rightContinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace E] : IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω

The processes with right-continuous paths are a stable class.

theorem ProbabilityTheory.isStable_left_limit {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace E] : IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (ω : Ω) (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)

The processes with left limits are a stable class.

theorem ProbabilityTheory.isStable_isCadlag {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace E] : IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω

The càdlàg processes are a stable class.

theorem ProbabilityTheory.isStable_continuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace E] : IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (ω : Ω), Continuous fun (x : ι) => X x ω

theorem ProbabilityTheory.locally_rightContinuous_iff {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] [𝓕.IsComplete P] : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, IsRightContinuous fun (x : ι) => X x ω

theorem ProbabilityTheory.locally_left_limit_iff {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] [𝓕.IsComplete P] : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω) (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, ∀ (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)

theorem ProbabilityTheory.locally_isCadlag_iff {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] [𝓕.IsComplete P] : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => X x ω

theorem ProbabilityTheory.locally_continuous_iff {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] [𝓕.IsComplete P] : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), Continuous fun (x : ι) => X x ω) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω

theorem ProbabilityTheory.locally_isCadlag_iff_locally_ae {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [NoMaxOrder ι] [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure P] {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] {X : ι → Ω → E} : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P ↔ Locally (fun (X : ι → Ω → E) => ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => X x ω) 𝓕 X P

theorem ProbabilityTheory.rightContinuous_indicator {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} [TopologicalSpace ι] (hC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (s : Set Ω) (ω : Ω) : IsRightContinuous fun (t : ι) => s.indicator (X t) ω

theorem ProbabilityTheory.stronglyAdapted_indicator {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [OrderBot ι] (hX : MeasureTheory.StronglyAdapted 𝓕 X) {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : MeasureTheory.StronglyAdapted 𝓕 fun (i : ι) => {ω : Ω | ⊥ < τ ω}.indicator (X i)

theorem ProbabilityTheory.isStronglyProgressive_indicator {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [NormedAddCommGroup E] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [OrderBot ι] [MeasurableSpace ι] (hX : MeasureTheory.IsStronglyProgressive 𝓕 X) {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : MeasureTheory.IsStronglyProgressive 𝓕 fun (i : ι) => {ω : Ω | ⊥ < τ ω}.indicator (X i)

theorem ProbabilityTheory.isStable_isStronglyProgressive {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [NormedAddCommGroup E] {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] [SecondCountableTopology ι] [TopologicalSpace.PseudoMetrizableSpace ι] [OrderBot ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] : IsStable 𝓕 fun (x : ι → Ω → E) => MeasureTheory.IsStronglyProgressive 𝓕 x

The class of strongly progressive processes is stable.

theorem ProbabilityTheory.isStable_isStronglyPredictable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [NormedAddCommGroup E] {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace ι] [SecondCountableTopology ι] [TopologicalSpace.PseudoMetrizableSpace ι] [OrderBot ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] [DenselyOrdered ι] : IsStable 𝓕 fun (x : ι → Ω → E) => MeasureTheory.IsStronglyPredictable 𝓕 x

The class of strongly predictable processes is stable.