@[simp]

theorem MeasureTheory.stoppedProcess_of_eq_top {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {ω : Ω} {X : ι → Ω → E} [LinearOrder ι] (s : ι) (hτ : τ ω = ⊤) : stoppedProcess X τ s ω = X s ω

@[simp]

theorem MeasureTheory.stoppedProcess_of_eq_coe {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {ω : Ω} {t : ι} {X : ι → Ω → E} [LinearOrder ι] (s : ι) (hτ : τ ω = ↑t) : stoppedProcess X τ s ω = X (min s t) ω

theorem MeasureTheory.stoppedProcess_congr {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [Nonempty ι] {τ : Ω → WithTop ι} {X Y : ι → Ω → E} [LinearOrder ι] (h : X ≡ᵐ[P] Y) : stoppedProcess X τ ≡ᵐ[P] stoppedProcess Y τ

theorem MeasureTheory.stoppedProcess_indicator_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {X Y : ι → Ω → E} [LinearOrder ι] [AddZeroClass E] {s : Set Ω} : stoppedProcess (fun (i : ι) => s.indicator ((X + Y) i)) τ = stoppedProcess (fun (i : ι) => s.indicator (X i)) τ + stoppedProcess (fun (i : ι) => s.indicator (Y i)) τ

theorem MeasureTheory.stoppedProcess_indicator_sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {X Y : ι → Ω → E} [LinearOrder ι] [AddGroup E] {s : Set Ω} : stoppedProcess (fun (i : ι) => s.indicator ((X - Y) i)) τ = stoppedProcess (fun (i : ι) => s.indicator (X i)) τ - stoppedProcess (fun (i : ι) => s.indicator (Y i)) τ

theorem MeasureTheory.stoppedProcess_indicator_stoppedProcess_indicator_of_le {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {X : ι → Ω → E} [LinearOrder ι] [OrderBot ι] [Zero E] {σ : Ω → WithTop ι} (h : σ ≤ τ) : stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < σ ω}.indicator (stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < τ ω}.indicator (X i)) τ i)) σ = stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < σ ω}.indicator (X i)) σ

Stopping at τ and then at a smaller time σ is the same as stopping at σ, for the stopped processes used in the definition of local properties.

theorem Monotone.stoppedProcess_indicator {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {ω : Ω} {X : ι → Ω → E} [LinearOrder ι] [Preorder E] [Zero E] (hX : Monotone fun (x : ι) => X x ω) (s : Set Ω) (τ : Ω → WithTop ι) : Monotone fun (x : ι) => MeasureTheory.stoppedProcess (fun (i : ι) => s.indicator (X i)) τ x ω

If a trajectory of a process is monotone, then the corresponding trajectory of the stopped process is also monotone.

theorem Continuous.stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {X : ι → Ω → E} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [TopologicalSpace E] {ω : Ω} (hX : Continuous fun (x : ι) => X x ω) (τ : Ω → WithTop ι) : Continuous fun (x : ι) => MeasureTheory.stoppedProcess X τ x ω

If a trajectory of a process is continuous, then the corresponding trajectory of the stopped process is also continuous.

theorem IsRightContinuous.stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {ω : Ω} {X : ι → Ω → E} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [TopologicalSpace E] (hX : IsRightContinuous fun (x : ι) => X x ω) (τ : Ω → WithTop ι) : IsRightContinuous fun (x : ι) => MeasureTheory.stoppedProcess X τ x ω

If a trajectory of a process is right-continuous, then the corresponding trajectory of the stopped process is also right-continuous.

theorem IsCadlag.stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {ω : Ω} {X : ι → Ω → E} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [TopologicalSpace E] (hX : IsCadlag fun (x : ι) => X x ω) (τ : Ω → WithTop ι) : IsCadlag fun (x : ι) => MeasureTheory.stoppedProcess X τ x ω

If a trajectory of a process is càdlàg, then the corresponding trajectory of the stopped process is also càdlàg.

@[simp]

theorem MeasureTheory.stoppedValue.add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [Add E] {u v : ι → Ω → E} {τ : Ω → WithTop ι} : stoppedValue (u + v) τ = stoppedValue u τ + stoppedValue v τ

@[simp]

theorem MeasureTheory.stoppedValue.neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [Neg E] {u : ι → Ω → E} {τ : Ω → WithTop ι} : stoppedValue (-u) τ = -stoppedValue u τ

@[simp]

theorem MeasureTheory.stoppedValue.sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [Sub E] {u v : ι → Ω → E} {τ : Ω → WithTop ι} : stoppedValue (u - v) τ = stoppedValue u τ - stoppedValue v τ