English
For a finite set s with τ ω ∈ s for all ω, stoppedProcess u τ n equals the sum of an indicator-weighted u i over i ∈ s with i < n plus the u n term when τ ω ≥ n.
Русский
Для конечного множества s, где τ ω ∈ s для всех ω, stoppedProcess(u, τ, n) равен сумме индикаторов над i ∈ s с i < n и добавляет u n при τ ω ≥ n.
LaTeX
$$$\text{stoppedProcess}(u, \tau, n) = \mathbf{1}_{\{\tau ≥ n\}} u_n + \sum_{i \in s, i < n} \mathbf{1}_{\{\tau = i\}} u_i$$$
Lean4
theorem stoppedProcess_eq_of_mem_finset [LinearOrder ι] [AddCommMonoid E] {s : Finset ι} (n : ι)
(hbdd : ∀ ω, τ ω < n → τ ω ∈ s) :
stoppedProcess u τ n = Set.indicator {a | n ≤ τ a} (u n) + ∑ i ∈ s with i < n, Set.indicator {ω | τ ω = i} (u i) :=
by
ext ω
rw [Pi.add_apply, Finset.sum_apply]
rcases le_or_gt n (τ ω) with h | h
· rw [stoppedProcess_eq_of_le h, Set.indicator_of_mem, Finset.sum_eq_zero, add_zero]
· intro m hm
refine Set.indicator_of_notMem ?_ _
rw [Finset.mem_filter] at hm
exact (hm.2.trans_le h).ne'
· exact h
· rw [stoppedProcess_eq_of_ge (le_of_lt h), Finset.sum_eq_single_of_mem (τ ω)]
· rw [Set.indicator_of_notMem, zero_add, Set.indicator_of_mem] <;> rw [Set.mem_setOf]
exact not_le.2 h
· rw [Finset.mem_filter]
exact ⟨hbdd ω h, h⟩
· intro b _ hneq
rw [Set.indicator_of_notMem]
rw [Set.mem_setOf]
exact hneq.symm
