measurableSet_tendsto — Mathlib

English

The set of points x where a sequence of measurable functions tends to a limit is measurable.

Русский

Множество точек x, для которых последовательность измеримых функций сходится к пределу, измеримо.

LaTeX

$$$\\\\text{measurableSet}_tendsto \\\\; : \\\\text{MeasurableSet} \\\\{ x \\\\;|\\\\; Tendsto(\\\\lambda n, f n x) l l' \\\\} $$$

Lean4

/-- The set of points for which a sequence of measurable functions converges to a given value
is measurable. -/
@[measurability]
theorem measurableSet_tendsto {_ : MeasurableSpace β} [MeasurableSpace γ] [Countable δ] {l : Filter δ}
    [l.IsCountablyGenerated] (l' : Filter γ) [l'.IsCountablyGenerated] [hl' : l'.IsMeasurablyGenerated] {f : δ → β → γ}
    (hf : ∀ i, Measurable (f i)) : MeasurableSet {x | Tendsto (fun n ↦ f n x) l l'} :=
  by
  rcases l.exists_antitone_basis with ⟨u, hu⟩
  rcases (Filter.hasBasis_self.mpr hl'.exists_measurable_subset).exists_antitone_subbasis with ⟨v, v_meas, hv⟩
  simp only [hu.tendsto_iff hv.toHasBasis, true_imp_iff, true_and, setOf_forall, setOf_exists]
  exact .iInter fun n ↦ .iUnion fun _ ↦ .biInter (to_countable _) fun i _ ↦ (v_meas n).2.preimage (hf i)

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