Theorems · Theorem · probability

MeasureTheory.stoppedProcess_eq_of_mem_finset

∀ {Ω : Type u_1} {ι : Type u_3} [inst : Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E}
  [inst_1 : LinearOrder ι] [inst_2 : AddCommMonoid E] {s : Finset ι} (n : ι),
  (∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) →
    MeasureTheory.stoppedProcess u τ n =
      {a | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)

Defined in

Mathlib.Probability.Process.Stopping

Cited by

2 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonemptyLinearOrderAddCommMonoid