mathlib3 documentation

measure_theory.constructions.borel_space.metrizable

Measurable functions in (pseudo-)metrizable Borel spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem measurable_of_tendsto_ennreal' {α : Type u_1} [measurable_space α] {ι : Type u_2} {f : ι α ennreal} {g : α ennreal} (u : filter ι) [u.ne_bot] [u.is_countably_generated] (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} [measurable_space α] {f : α ennreal} {g : α ennreal} (hf : (i : ), measurable (f i)) (lim : filter.tendsto f filter.at_top (nhds g)) :

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

theorem measurable_of_tendsto_nnreal' {α : Type u_1} [measurable_space α] {ι : Type u_2} {f : ι α nnreal} {g : α nnreal} (u : filter ι) [u.ne_bot] [u.is_countably_generated] (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} [measurable_space α] {f : α nnreal} {g : α nnreal} (hf : (i : ), measurable (f i)) (lim : filter.tendsto f filter.at_top (nhds g)) :

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

theorem measurable_of_tendsto_metrizable' {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] [topological_space.pseudo_metrizable_space β] [measurable_space β] [borel_space β] {ι : Type u_3} {f : ι α β} {g : α β} (u : filter ι) [u.ne_bot] [u.is_countably_generated] (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.

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

theorem ae_measurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] [topological_space.pseudo_metrizable_space β] [measurable_space β] [borel_space β] {ι : Type u_3} {μ : measure_theory.measure α} {f : ι α β} {g : α β} (u : filter ι) [hu : u.ne_bot] [u.is_countably_generated] (hf : (n : ι), ae_measurable (f n) μ) (h_tendsto : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ι), f n x) u (nhds (g x))) :
theorem ae_measurable_of_tendsto_metrizable_ae' {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] [topological_space.pseudo_metrizable_space β] [measurable_space β] [borel_space β] {μ : measure_theory.measure α} {f : α β} {g : α β} (hf : (n : ), ae_measurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :
theorem ae_measurable_of_unif_approx {α : Type u_1} [measurable_space α] {β : Type u_2} [measurable_space β] [pseudo_metric_space β] [borel_space β] {μ : measure_theory.measure α} {g : α β} (hf : (ε : ), ε > 0 ( (f : α β), ae_measurable f μ ∀ᵐ (x : α) μ, has_dist.dist (f x) (g x) ε)) :
theorem measurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] [topological_space.pseudo_metrizable_space β] [measurable_space β] [borel_space β] {μ : measure_theory.measure α} [μ.is_complete] {f : α β} {g : α β} (hf : (n : ), measurable (f n)) (h_ae_tendsto : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :
theorem measurable_limit_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] [topological_space.pseudo_metrizable_space β] [measurable_space β] [borel_space β] {ι : Type u_3} [countable ι] [nonempty ι] {μ : measure_theory.measure α} {f : ι α β} {L : filter ι} [L.is_countably_generated] (hf : (n : ι), ae_measurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) μ, (l : β), filter.tendsto (λ (n : ι), f n x) L (nhds l)) :
(f_lim : α β) (hf_lim_meas : measurable f_lim), ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ι), f n x) L (nhds (f_lim x))