stoppedValue_eq' — Mathlib

English

Under mild conditions, stoppedValue u τ equals a finite combination of indicators on τ ω = i weighted by u i, for i in a finite set.

Русский

При умеренных условиях stoppedValue выражается как конечная комбинация индикаторов τ ω = i, взвешенная значениями u i.

LaTeX

$$$\text{stoppedValue}(u, \tau) = \sum_{i \in s} \mathbf{1}_{\{\omega : \tau(\omega)=i\}} u_i$$$

Lean4

theorem stoppedValue_eq' [Preorder ι] [LocallyFiniteOrderBot ι] [AddCommMonoid E] {N : ι} (hbdd : ∀ ω, τ ω ≤ N) :
    stoppedValue u τ = ∑ i ∈ Finset.Iic N, Set.indicator {ω | τ ω = i} (u i) :=
  stoppedValue_eq_of_mem_finset fun ω => Finset.mem_Iic.mpr (hbdd ω)

Похожие утверждения