source
@[simp]
theorem MeasureTheory.stoppedProcess_const {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u₀ : Ω → β} {τ : Ω → WithTop ι} :
stoppedProcess (fun (x : ι) => u₀) τ = fun (x : ι) => u₀
source
@[simp]
theorem MeasureTheory.stoppedProcess_neg {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Neg β] {u : ι → Ω → β} {τ : Ω → WithTop ι} :
stoppedProcess (-u) τ = -stoppedProcess u τ
source
@[simp]
theorem MeasureTheory.stoppedProcess_add {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Add β] {u v : ι → Ω → β} {τ : Ω → WithTop ι} :
stoppedProcess (u + v) τ = stoppedProcess u τ + stoppedProcess v τ
source
@[simp]
theorem MeasureTheory.stoppedProcess_sub {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Sub β] {u v : ι → Ω → β} {τ : Ω → WithTop ι} :
stoppedProcess (u - v) τ = stoppedProcess u τ - stoppedProcess v τ
source
@[simp]
theorem MeasureTheory.stoppedProcess_const_smul {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [SMul ℝ β] (c : ℝ) {u : ι → Ω → β} {τ : Ω → WithTop ι} :
stoppedProcess (c • u) τ = c • stoppedProcess u τ
source
theorem MeasureTheory.stoppedProcess_indicator_comm {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Zero β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {s : Set Ω} (i : ι) :
stoppedProcess (fun (i : ι) => s.indicator (u i)) τ i = s.indicator (stoppedProcess u τ i)
source
theorem MeasureTheory.stoppedProcess_indicator_comm' {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Zero β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {s : Set Ω} :
stoppedProcess (fun (i : ι) => s.indicator (u i)) τ = fun (i : ι) => s.indicator (stoppedProcess u τ i)
source
theorem MeasureTheory.stoppedValue_stoppedProcess_apply {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {ω : Ω} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} (hω : σ ω ≠ ⊤) :
stoppedValue (stoppedProcess u τ) σ ω = stoppedValue u (fun (ω : Ω) => min (σ ω) (τ ω)) ω
source
@[simp]
theorem MeasureTheory.stoppedProcess_stoppedProcess {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} :
stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u (σ ⊓ τ)
source
theorem MeasureTheory.stoppedProcess_stoppedProcess' {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} :
stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u fun (ω : Ω) => min (σ ω) (τ ω)
source
theorem MeasureTheory.stoppedProcess_stoppedProcess_of_le_right {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} (h : σ ≤ τ) :
stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u σ
source
theorem MeasureTheory.stoppedProcess_stoppedProcess_of_le_left {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} (h : τ ≤ σ) :
stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u τ
source
theorem MeasureTheory.stoppedProcess_eq_stoppedValue_apply {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ : Ω → WithTop ι} (i : ι) (ω : Ω) :
stoppedProcess u τ i ω = stoppedValue u (fun (ω : Ω) => min (↑i) (τ ω)) ω