Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Measurable functions in (pseudo-)metrizable Borel spaces #

theorem measurable_of_tendsto_metrizable' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {ι : Type u_3} {f : ιαβ} {g : αβ} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated 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} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {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} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {ι : Type u_3} {μ : MeasureTheory.Measure α} {f : ιαβ} {g : αβ} (u : Filter ι) [hu : Filter.NeBot u] [Filter.IsCountablyGenerated u] (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} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α} {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} [MeasurableSpace α] {β : Type u_3} [MeasurableSpace β] [PseudoMetricSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α} {g : αβ} (hf : ε > 0, ∃ (f : αβ), AEMeasurable f μ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ε) :
theorem measurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.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} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {ι : Type u_3} [Countable ι] [Nonempty ι] {μ : MeasureTheory.Measure α} {f : ιαβ} {L : Filter ι} [Filter.IsCountablyGenerated L] (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} [MeasurableSpace α] {A : Set α} {ι : Type u_4} (L : Filter ι) [Filter.IsCountablyGenerated L] {As : ιSet α} [Filter.NeBot L] (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} [MeasurableSpace α] {A : Set α} {ι : Type u_4} (L : Filter ι) [Filter.IsCountablyGenerated L] {As : ιSet α} [Filter.NeBot L] {μ : MeasureTheory.Measure α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As 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.