stoppedValue_piecewise_const' — Mathlib

English

In the same setting as above, stoppedValue for a piecewise constant function equals the sum of indicator-based pieces: indicator of S times f(i) plus indicator of Sᶜ times f(j).

Русский

В той же конфигурации stoppedValue для кусочно константной функции равен сумме индикаторных частей: 1_S·f(i) + 1_{S^c}·f(j).

LaTeX

$$$\text{stoppedValue } f (s.piecewise (\text{const } i) (\text{const } j)) = s.indicator (f i) + s^c.indicator (f j)$$$

Lean4

theorem stoppedValue_piecewise_const' {ι' : Type*} {i j : ι'} {f : ι' → Ω → ℝ} :
    stoppedValue f (s.piecewise (fun _ => i) fun _ => j) = s.indicator (f i) + sᶜ.indicator (f j) := by ext ω;
  rw [stoppedValue]; by_cases hx : ω ∈ s <;> simp [hx]

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