stoppedProcess_eq'' — Mathlib

English

An explicit decomposition of stoppedProcess as a sum of indicators over τ a ≤ n and indicators for τ a = i with i < n.

Русский

Явное разложение stoppedProcess как сумма индикаторов по τ a ≤ n и индикаторов для τ a = i при i < n.

LaTeX

$$$\text{stoppedProcess}(u, \tau, n) = \sum_{i \in \text{Iio}(n)} (\mathbf{1}_{\{τ = i\}} u_i) + \mathbf{1}_{\{τ ≤ n\}} u_n$$$

Lean4

theorem stoppedProcess_eq'' [LinearOrder ι] [LocallyFiniteOrderBot ι] [AddCommMonoid E] (n : ι) :
    stoppedProcess u τ n = Set.indicator {a | n ≤ τ a} (u n) + ∑ i ∈ Finset.Iio n, Set.indicator {ω | τ ω = i} (u i) :=
  by
  have h_mem : ∀ ω, τ ω < n → τ ω ∈ Finset.Iio n := fun ω h => Finset.mem_Iio.mpr h
  rw [stoppedProcess_eq_of_mem_finset n h_mem]
  congr with i
  simp

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