English
Under τ ≤ π and a finite bound N with π ≤ N, the difference stoppedValue(u,π) − stoppedValue(u,τ) can be written as a sum over i = 0,...,N of indicator of {τ ≤ i < π} times (u(i+1) − u(i)).
Русский
При неравенстве τ ≤ π и ограничении π на N сумма разностей может быть записана как сумма по i от 0 до N индикаторной функции {τ ≤ i < π} умноженной на приращение (u(i+1) − u(i)).
LaTeX
$$$\text{stoppedValue } u\ π - \text{stoppedValue } u\ τ =\ ω \mapsto \sum_{i=0}^{N} \mathbf{1}_{\{ω\,|\, τ(ω) ≤ i \wedge i < π(ω)\}}(ω)\,(u(i+1,ω) - u(i,ω))$$$
Lean4
theorem stoppedValue_sub_eq_sum' [AddCommGroup β] (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ ω, π ω ≤ N) :
stoppedValue u π - stoppedValue u τ = fun ω =>
(∑ i ∈ Finset.range (N + 1), Set.indicator {ω | τ ω ≤ i ∧ i < π ω} (u (i + 1) - u i)) ω :=
by
rw [stoppedValue_sub_eq_sum hle]
ext ω
simp only [Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
refine Finset.sum_congr ?_ fun _ _ => rfl
ext i
simp only [Finset.mem_filter, Set.mem_setOf_eq, Finset.mem_range, Finset.mem_Ico]
exact ⟨fun h => ⟨lt_trans h.2 (Nat.lt_succ_iff.2 <| hbdd _), h⟩, fun h => h.2⟩
