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.
theorem
measurable_of_tendsto_metrizable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β]
{f : ℕ → α → β}
{g : α → β}
(hf : ∀ (i : ℕ), measurable (f i))
(lim : filter.tendsto f filter.at_top (nhds g)) :
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))) :
ae_measurable g μ
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))) :
ae_measurable g μ
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) ≤ ε)) :
ae_measurable g μ
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))