Measurable functions in (pseudo-)metrizable Borel spaces #
theorem
measurable_of_tendsto_ennreal'
{α : Type u_1}
[MeasurableSpace α]
{ι : Type u_3}
{f : ι → α → ENNReal}
{g : α → ENNReal}
(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 ℝ≥0∞ valued functions is measurable.
theorem
measurable_of_tendsto_ennreal
{α : Type u_1}
[MeasurableSpace α]
{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}
[MeasurableSpace α]
{ι : Type u_3}
{f : ι → α → NNReal}
{g : α → NNReal}
(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 ℝ≥0 valued functions is measurable.
theorem
measurable_of_tendsto_nnreal
{α : Type u_1}
[MeasurableSpace α]
{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}
[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.