English
For any n, stoppedProcess u τ n equals the sum of an indicator part at n+1 with u n plus the sum up to n of indicators for τ = i with u i.
Русский
Для любого n остановленный процесс равен сумме: 1_{τ≥n+1}·u n + ∑_{i≤n} 1_{τ=i}·u i.
LaTeX
$$$\text{stoppedProcess } u\ τ\ n = 1_{\{a:\, n+1 ≤ τ a\}}(a)\, u n + \sum_{i=0}^{n} 1_{\{a:\, τ a = i\}}(a)\, u i$$$
Lean4
theorem stoppedProcess_eq' (n : ℕ) :
stoppedProcess u τ n =
Set.indicator {a | n + 1 ≤ τ a} (u n) + ∑ i ∈ Finset.range (n + 1), Set.indicator {a | τ a = i} (u i) :=
by
have : {a | n ≤ τ a}.indicator (u n) = {a | n + 1 ≤ τ a}.indicator (u n) + {a | τ a = n}.indicator (u n) :=
by
ext x
rw [add_comm, Pi.add_apply, ← Set.indicator_union_of_notMem_inter]
· simp_rw [@eq_comm _ _ n, @le_iff_eq_or_lt _ _ n, Nat.succ_le_iff, Set.setOf_or]
· rintro ⟨h₁, h₂⟩
rw [Set.mem_setOf] at h₁ h₂
exact (Nat.succ_le_iff.1 h₂).ne h₁.symm
rw [stoppedProcess_eq, this, Finset.sum_range_succ_comm, ← add_assoc]
