measurableSet_lt_of_isLUB — Mathlib

English

Let hτ be a stopping time and i an index. If IsLUB(Iio(i), i) holds, then {ω ∈ Ω : τ(ω) < i} is measurable in F_i.

Русский

Пусть hτ — остановочное время, и i — индекс. Если выполняется IsLUB(Iio(i), i), то {ω ∈ Ω : τ(ω) < i} измеримо в F_i.

LaTeX

$$$\forall i,\, (IsLUB(\mathrm{Iio}(i), i) \rightarrow \{\omega \in \Omega \mid \tau(\omega) < i\} \in \mathcal{F}_i) $$$

Lean4

/-- Auxiliary lemma for `MeasureTheory.IsStoppingTime.measurableSet_lt`. -/
theorem measurableSet_lt_of_isLUB (hτ : IsStoppingTime f τ) (i : ι) (h_lub : IsLUB (Set.Iio i) i) :
    MeasurableSet[f i] {ω | τ ω < i} := by
  by_cases hi_min : IsMin i
  · suffices {ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
    ext1 ω
    simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
    exact isMin_iff_forall_not_lt.mp hi_min (τ ω)
  obtain ⟨seq, -, -, h_tendsto, h_bound⟩ :
    ∃ seq : ℕ → ι, Monotone seq ∧ (∀ j, seq j ≤ i) ∧ Tendsto seq atTop (𝓝 i) ∧ ∀ j, seq j < i :=
    h_lub.exists_seq_monotone_tendsto (not_isMin_iff.mp hi_min)
  have h_Ioi_eq_Union : Set.Iio i = ⋃ j, {k | k ≤ seq j} :=
    by
    ext1 k
    simp only [Set.mem_Iio, Set.mem_iUnion, Set.mem_setOf_eq]
    refine ⟨fun hk_lt_i => ?_, fun h_exists_k_le_seq => ?_⟩
    · rw [tendsto_atTop'] at h_tendsto
      have h_nhds : Set.Ici k ∈ 𝓝 i := mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_i⟩
      obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds
      exact ⟨a, ha a le_rfl⟩
    · obtain ⟨j, hk_seq_j⟩ := h_exists_k_le_seq
      exact hk_seq_j.trans_lt (h_bound j)
  have h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i := by ext1 ω;
    simp only [Set.mem_setOf_eq, Set.mem_preimage, Set.mem_Iio]
  rw [h_lt_eq_preimage, h_Ioi_eq_Union]
  simp only [Set.preimage_iUnion, Set.preimage_setOf_eq]
  exact MeasurableSet.iUnion fun n => f.mono (h_bound n).le _ (hτ.measurableSet_le (seq n))

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