stoppedValue_const — Mathlib

English

For a finite set of indices, the stopped process equals the sum of indicator-valued contributions from each index, separated by the region where τ < n and where τ ≥ n.

Русский

Для конечного множества индексов остановленный процесс равен сумме вкладов-индикаторов по каждому индексу, разделённых по областям τ < n и τ ≥ n.

LaTeX

$$$\text{stoppedProcess}(u, \tau, n) = \mathbf{1}_{\{\tau \ge n\}} u_n + \sum_{i \in s, i

Lean4

theorem stoppedValue_const (u : ι → Ω → β) (i : ι) : (stoppedValue u fun _ => i) = u i :=
  rfl

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