English
If there is a uniform bound N on τ ω, then stoppedValue u τ equals the finite sum over i = 0,...,N of indicator of {τ ω = i} times u i.
Русский
При равномерном ограничении τ ω на N, stoppedValue u τ равен конечной сумме по i от 0 до N индикаторной функции {τ ω = i}·u i.
LaTeX
$$${N : \mathbb{N}} \to \big( \forall ω, τ(ω) ≤ N \big) \Rightarrow \ stoppedValue\ u\ τ = \omega \mapsto \sum_{i=0}^{N} \mathbf{1}_{\{τ ω = i\}}(ω)\, u(i,ω)$$$
Lean4
theorem piContent_eq_measure_pi [Fintype ι] {s : Set (Π i, X i)} (hs : MeasurableSet s) :
piContent μ s = Measure.pi μ s :=
by
let e : @Finset.univ ι _ ≃ ι :=
{ toFun i := i
invFun i := ⟨i, mem_univ i⟩ }
have : s = cylinder univ (MeasurableEquiv.piCongrLeft X e ⁻¹' s) := rfl
nth_rw 1 [this]
dsimp [e]
rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← Measure.pi_map_piCongrLeft e, ←
Measure.map_apply (by fun_prop) hs];
rfl
