stoppedProcess_eq — Mathlib

English

For any n, the stopped process equals the sum of the indicator of {τ ≥ n} times u n plus the sum over i < n of indicator {τ = i} times u i.

Русский

Для любого n останленный процесс равен сумме по i < n: 1_{τ ≥ n}·u n + ∑_{i<n} 1_{τ=i}·u i.

LaTeX

$$$\text{stoppedProcess } u\ τ\ n = \mathbf{1}_{\{a:\, n ≤ τ a\}}(a)\, u n + \sum_{i=0}^{n-1} \mathbf{1}_{\{a:\, τ a = i\}}(a)\, u i$$$

Lean4

theorem stoppedProcess_eq (n : ℕ) :
    stoppedProcess u τ n =
      Set.indicator {a | n ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω | τ ω = i} (u i) :=
  by
  rw [stoppedProcess_eq'' n]
  congr with i
  rw [Finset.mem_Iio, Finset.mem_range]

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