# Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

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

theorem measurable_of_tendsto_ennreal' {α : Type u_1} [] {ι : Type u_3} {f : ιαENNReal} {g : αENNReal} (u : ) [] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

A limit (over a general filter) of measurable ℝ≥0∞ valued functions is measurable.

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

A sequential limit of measurable ℝ≥0∞ valued functions is measurable.

theorem measurable_of_tendsto_nnreal' {α : Type u_1} [] {ι : Type u_3} {f : ιαNNReal} {g : αNNReal} (u : ) [] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

A limit (over a general filter) of measurable ℝ≥0 valued functions is measurable.

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

A sequential limit of measurable ℝ≥0 valued functions is measurable.

theorem measurable_of_tendsto_metrizable' {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} {f : ιαβ} {g : αβ} (u : ) [] (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 : ] (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 : ∀ (ε : ), ε > 0f, ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ε) :
theorem measurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [] [] [] [] {μ : } {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 : } (hf : ∀ (n : ι), AEMeasurable (f n)) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, l, Filter.Tendsto (fun n => f n x) L (nhds l)) :
f_lim hf_lim_meas, ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) L (nhds (f_lim x))
theorem measurableSet_of_tendsto_indicator {α : Type u_4} [] {A : Set α} {ι : Type u_3} (L : ) {As : ιSet α} [] (As_mble : ∀ (i : ι), MeasurableSet (As i)) (h_lim : Filter.Tendsto (fun i => Set.indicator (As i) 1) L (nhds ())) :

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_4} [] {A : Set α} {ι : Type u_3} (L : ) {As : ιSet α} [] {μ : } (As_mble : ∀ (i : ι), ) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => Set.indicator (As i) 1 x) L (nhds ())) :

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.