stronglyMeasurable_stoppedValue_of_le

English

Under suitable order/measure-theoretic assumptions, the map i ↦ min(i, τ(ω)) is progressively measurable.

Русский

При подходящих предпосылках порядок/измеримости отображения i ↦ min(i, τ(ω)) является прогрессивно измеримым.

LaTeX

$$$\text{ProgMeasurable}(f, i \mapsto \min(i, \tau(·)))$$$

Lean4

theorem stronglyMeasurable_stoppedValue_of_le (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) {n : ι}
    (hτ_le : ∀ ω, τ ω ≤ n) : StronglyMeasurable[f n] (stoppedValue u τ) :=
  by
  have : stoppedValue u τ = (fun p : Set.Iic n × Ω => u (↑p.fst) p.snd) ∘ fun ω => (⟨τ ω, hτ_le ω⟩, ω) := by ext1 ω;
    simp only [stoppedValue, Function.comp_apply]
  rw [this]
  refine StronglyMeasurable.comp_measurable (h n) ?_
  exact (hτ.measurable_of_le hτ_le).subtype_mk.prodMk measurable_id

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