condExp_stopping_time_ae_eq_restrict_eq

English

If τ ω ≤ N for all ω, then stoppedValue u τ is the finite sum ∑_{i=0}^{N} 1_{τ ω = i} · u i.

Русский

Если для всех ω выполнено τ ω ≤ N, то stoppedValue u τ равен сумме по i от 0 до N с весом 1_{τ ω = i} · u i.

LaTeX

$$$\text{stoppedValue } u\ τ = ω \mapsto \sum_{i=0}^{N} \mathbf{1}_{\{ω\mid τ ω = i\}}(ω)\, u(i,ω)$$$

Lean4

theorem condExp_stopping_time_ae_eq_restrict_eq [FirstCountableTopology ι] [SigmaFiniteFiltration μ ℱ]
    (hτ : IsStoppingTime ℱ τ) [SigmaFinite (μ.trim hτ.measurableSpace_le)] (i : ι) :
    μ[f|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] μ[f|ℱ i] :=
  by
  refine
    condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i) (hτ.measurableSet_eq' i) fun t => ?_
  rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

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