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 ι)
[u.NeBot]
[u.IsCountablyGenerated]
(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 : Nat → α → β}
{g : α → β}
(hf : ∀ (i : Nat), 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 : u.NeBot]
[u.IsCountablyGenerated]
(hf : ∀ (n : ι), AEMeasurable (f n) μ)
(h_tendsto :
Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (n : ι) => f n x) u (nhds (g x))) (MeasureTheory.ae μ))
:
AEMeasurable g μ
theorem
aemeasurable_of_tendsto_metrizable_ae'
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{μ : MeasureTheory.Measure α}
{f : Nat → α → β}
{g : α → β}
(hf : ∀ (n : Nat), AEMeasurable (f n) μ)
(h_ae_tendsto :
Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (n : Nat) => f n x) Filter.atTop (nhds (g x)))
(MeasureTheory.ae μ))
:
AEMeasurable g μ
theorem
aemeasurable_of_unif_approx
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_3}
[MeasurableSpace β]
[PseudoMetricSpace β]
[BorelSpace β]
{μ : MeasureTheory.Measure α}
{g : α → β}
(hf :
∀ (ε : Real),
GT.gt ε 0 →
Exists fun (f : α → β) =>
And (AEMeasurable f μ)
(Filter.Eventually (fun (x : α) => LE.le (Dist.dist (f x) (g x)) ε) (MeasureTheory.ae μ)))
:
AEMeasurable g μ
theorem
measurable_of_tendsto_metrizable_ae
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{μ : MeasureTheory.Measure α}
[μ.IsComplete]
{f : Nat → α → β}
{g : α → β}
(hf : ∀ (n : Nat), Measurable (f n))
(h_ae_tendsto :
Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (n : Nat) => f n x) Filter.atTop (nhds (g x)))
(MeasureTheory.ae μ))
:
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 ι}
[L.IsCountablyGenerated]
(hf : ∀ (n : ι), AEMeasurable (f n) μ)
(h_ae_tendsto :
Filter.Eventually (fun (x : α) => Exists fun (l : β) => Filter.Tendsto (fun (n : ι) => f n x) L (nhds l))
(MeasureTheory.ae μ))
:
Exists fun (f_lim : α → β) =>
And (Measurable f_lim)
(Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (n : ι) => f n x) L (nhds (f_lim x))) (MeasureTheory.ae μ))
theorem
measurableSet_of_tendsto_indicator
{α : Type u_3}
[MeasurableSpace α]
{A : Set α}
{ι : Type u_4}
(L : Filter ι)
[L.IsCountablyGenerated]
{As : ι → Set α}
[L.NeBot]
(As_mble : ∀ (i : ι), MeasurableSet (As i))
(h_lim : ∀ (x : α), Filter.Eventually (fun (i : ι) => Iff (Membership.mem (As i) x) (Membership.mem A x)) L)
:
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 ι)
[L.IsCountablyGenerated]
{As : ι → Set α}
[L.NeBot]
{μ : MeasureTheory.Measure α}
(As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ)
(h_lim :
Filter.Eventually
(fun (x : α) => Filter.Eventually (fun (i : ι) => Iff (Membership.mem (As i) x) (Membership.mem A x)) L)
(MeasureTheory.ae μ))
:
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.