# Measurable functions in (pseudo-)metrizable Borel spaces #

theorem measurable_of_tendsto_metrizable' {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} {f : ιαβ} {g : αβ} (u : ) [u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is measurable.

theorem measurable_of_tendsto_metrizable {α : Type u_1} {β : Type u_2} [] [] [] [] {f : αβ} {g : αβ} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

A sequential limit of measurable functions valued in a (pseudo) metrizable space is measurable.

theorem aemeasurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} {μ : } {f : ιαβ} {g : αβ} (u : ) [hu : u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (n : ι), AEMeasurable (f n) μ) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) u (nhds (g x))) :
theorem aemeasurable_of_tendsto_metrizable_ae' {α : Type u_1} {β : Type u_2} [] [] [] [] {μ : } {f : αβ} {g : αβ} (hf : ∀ (n : ), AEMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (g x))) :
theorem aemeasurable_of_unif_approx {α : Type u_1} [] {β : Type u_3} [] [] {μ : } {g : αβ} (hf : ε > 0, ∃ (f : αβ), ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ε) :
theorem measurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [] [] [] [] {μ : } [μ.IsComplete] {f : αβ} {g : αβ} (hf : ∀ (n : ), Measurable (f n)) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (g x))) :
theorem measurable_limit_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} [] [] {μ : } {f : ιαβ} {L : } [L.IsCountablyGenerated] (hf : ∀ (n : ι), AEMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Filter.Tendsto (fun (n : ι) => f n x) L (nhds l)) :
∃ (f_lim : αβ), Measurable f_lim ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) L (nhds (f_lim x))
theorem measurableSet_of_tendsto_indicator {α : Type u_3} [] {A : Set α} {ι : Type u_4} (L : ) [L.IsCountablyGenerated] {As : ιSet α} [L.NeBot] (As_mble : ∀ (i : ι), MeasurableSet (As i)) (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x As i x A) :

If the indicator functions of measurable sets Aᵢ converge to the indicator function of a set A along a nontrivial countably generated filter, then A is also measurable.

theorem nullMeasurableSet_of_tendsto_indicator {α : Type u_3} [] {A : Set α} {ι : Type u_4} (L : ) [L.IsCountablyGenerated] {As : ιSet α} [L.NeBot] {μ : } (As_mble : ∀ (i : ι), ) (h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x As i x A) :

If the indicator functions of a.e.-measurable sets Aᵢ converge a.e. to the indicator function of a set A along a nontrivial countably generated filter, then A is also a.e.-measurable.