English
If a finite set s contains all τ ω, then stoppedValue u τ equals the finite sum over i in s of indicator of {τ ω = i} times u i.
Русский
Если множество s содержит все значения τ(ω), то stoppedValue u τ равно сумме по i в s от индикатора {τ ω = i} умноженного на u i.
LaTeX
$$$\text{stoppedValue}(u, \tau) = \sum_{i \in s} \mathbf{1}_{\{\omega : \tau(\omega)=i\}} \; u_i$$$
Lean4
theorem stoppedValue_eq_of_mem_finset [AddCommMonoid E] {s : Finset ι} (hbdd : ∀ ω, τ ω ∈ s) :
stoppedValue u τ = ∑ i ∈ s, Set.indicator {ω | τ ω = i} (u i) :=
by
ext y
classical
rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
suffices {i ∈ s | y ∈ {ω : Ω | τ ω = i}} = ({τ y} : Finset ι) by rw [this, Finset.sum_singleton]
ext1 ω
simp only [Set.mem_setOf_eq, Finset.mem_filter, Finset.mem_singleton]
constructor <;> intro h
· exact h.2.symm
· refine ⟨?_, h.symm⟩; rw [h]; exact hbdd y
