stoppedValue_eq — Mathlib

English

If all τ ω ≤ N for some fixed N, then stoppedValue u τ is the finite sum over i = 0,...,N of indicator of {τ ω = i} times u i.

Русский

Если для всех ω выполняется τ ω ≤ N, то stoppedValue u τ равен конечной сумме от i=0 до N: 1_{τ ω = i} · u i.

LaTeX

$$$\text{stoppedValue } u\ τ = \omega \mapsto \sum_{i=0}^{N} \mathbf{1}_{\{ω'\,|\, τ(ω') = i\}}(ω)\,(u(i,ω))$$$

Lean4

theorem stoppedValue_eq {N : ℕ} (hbdd : ∀ ω, τ ω ≤ N) :
    stoppedValue u τ = fun x => (∑ i ∈ Finset.range (N + 1), Set.indicator {ω | τ ω = i} (u i)) x :=
  stoppedValue_eq_of_mem_finset fun ω => Finset.mem_range_succ_iff.mpr (hbdd ω)

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