measurable_of_tendsto_metrizable
theorem measurable_of_tendsto_metrizable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [inst_4 : BorelSpace β]
{f : ℕ → α → β} {g : α → β},
(∀ (i : ℕ), Measurable (f i)) → Filter.Tendsto f Filter.atTop (nhds g) → Measurable g
The theorem `measurable_of_tendsto_metrizable` states that if we have a sequence of measurable functions `f : ℕ → α → β` converging to a function `g : α → β`, in a pseudo-metrizable topological space `β`, then the limit function `g` is also measurable. Here, convergence is defined in terms of the `Filter.Tendsto` function, which states that for every neighborhood of `g`, the pre-image of this neighborhood under the function `f` is eventually in the filter `Filter.atTop`, signifying that as we go to the limit (in this case as `ℕ` goes to infinity), `f` gets arbitrarily close to `g`. The `Measurable` property of a function is defined as the preimage of every measurable set being measurable. Thus, in effect, the theorem guarantees that the limit of measurable functions in a pseudo-metrizable space retains the measurability property.
More concisely: If `f : ℕ → α → β` is a sequence of measurable functions converging to a measurable function `g : α → β` in a pseudo-metrizable topological space `β`, then `g` is also measurable.
|
measurable_of_tendsto_metrizable'
theorem measurable_of_tendsto_metrizable' :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [inst_4 : BorelSpace β]
{ι : Type u_3} {f : ι → α → β} {g : α → β} (u : Filter ι) [inst_5 : u.NeBot] [inst_6 : u.IsCountablyGenerated],
(∀ (i : ι), Measurable (f i)) → Filter.Tendsto f u (nhds g) → Measurable g
The theorem `measurable_of_tendsto_metrizable'` states that if we have a sequence of measurable functions defined on a measurable space, valued in a pseudometrizable space, and this sequence tends to a limit function with respect to a certain filter, then that limit function is measurable. This is under the condition that the filter is neither empty (i.e., it is not the bottom filter) nor uncountably generated, and the target space is equipped with the Borel sigma algebra induced by its topology.
More concisely: If $(X, \mathcal{B}, \mu)$ is a measurable space, $(Y, d)$ is a pseudometrizable space, $f_n : X \to Y$ is a sequence of measurable functions, and $f : X \to Y$ is the limit of $f_n$ with respect to a non-empty and countably generated filter, then $f$ is measurable.
|
measurableSet_of_tendsto_indicator
theorem measurableSet_of_tendsto_indicator :
∀ {α : Type u_3} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_4} (L : Filter ι)
[inst_1 : L.IsCountablyGenerated] {As : ι → Set α} [inst_2 : L.NeBot],
(∀ (i : ι), MeasurableSet (As i)) → (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → MeasurableSet A
The theorem `measurableSet_of_tendsto_indicator` states that for any measurable space `α`, any set `A` of type `α`, any type `ι`, and any filter `L` on `ι` that is countably generated and nontrivial (i.e., not the bottom filter), if the indicator functions of measurable sets `As i` (for any `i` in `ι`) converge to the indicator function of `A` along the filter `L`, then the set `A` is also measurable. In other words, if a sequence of measurable sets `As i` converges in the sense that for every `x` in `α`, the membership of `x` in the `As i` eventually coincides with its membership in `A` along the filter `L`, then `A` is measurable.
More concisely: If a sequence of measurable sets converges pointwise to a set along a countably generated and nontrivial filter, then the limit set is measurable.
|
nullMeasurableSet_of_tendsto_indicator
theorem nullMeasurableSet_of_tendsto_indicator :
∀ {α : Type u_3} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_4} (L : Filter ι)
[inst_1 : L.IsCountablyGenerated] {As : ι → Set α} [inst_2 : L.NeBot] {μ : MeasureTheory.Measure α},
(∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
(∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → MeasureTheory.NullMeasurableSet A μ
This theorem states that if we have a sequence of almost everywhere measurable sets `Aᵢ`, indexed by `ι`, and the indicator functions of these sets converge almost everywhere to the indicator function of another set `A` along a nonempty countably generated filter `L`, then the set `A` is also almost everywhere measurable. The almost everywhere measurability of a set means that it can be approximated by a measurable set up to a set of null measure. The countably generated filter `L` is used to describe a certain kind of convergence (almost everywhere convergence) of the sequence of indicator functions of the sets `Aᵢ` to the indicator function of the set `A`.
More concisely: If `{Aι} (ι ∈ I)` is a sequence of almost everywhere measurable sets and `ι₁, ι₂, ...` is a sequence in `I` such that `∥F.indicator Aι i - F.indicator A∥_1 ∈ L` for all `i`, then `A` is almost everywhere measurable, where `F` is the complete and separable measurable structure on the underlying measurable space and `L` is a nonempty countably generated filter.
|
aemeasurable_of_tendsto_metrizable_ae
theorem aemeasurable_of_tendsto_metrizable_ae :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [inst_4 : BorelSpace β]
{ι : Type u_3} {μ : MeasureTheory.Measure α} {f : ι → α → β} {g : α → β} (u : Filter ι) [hu : u.NeBot]
[inst_5 : u.IsCountablyGenerated],
(∀ (n : ι), AEMeasurable (f n) μ) →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) → AEMeasurable g μ
This theorem states that for any types `α`, `β` and `ι` where `α` is a measurable space, `β` is a topological space which is also a pseudo metrizable space, a measurable space, and a Borel space, and a measure `μ` is defined on `α`, if we have a sequence of functions `f : ι → α → β` and another function `g : α → β`, with a filter `u` on `ι` that is countably generated and not bottom, such that each function `f n` is almost everywhere measurable with respect to measure `μ`, and for almost all `x` in `α`, the function values `f n x` tend to `g x` as `n` goes to `u` (in the sense that the pre-image of any neighborhood of `g x` under `f n` is a neighborhood in `u`), then the function `g` is also almost everywhere measurable. Here, being almost everywhere measurable means that `g` coincides almost everywhere with a measurable function.
More concisely: If `α` is a measurable space, `β` is a Borel space, a pseudo-metric space, and a topological space with a measure `μ`, `f : ι → α → β` is a sequence of almost everywhere measurable functions, `g : α → β` is a function, and `u` is a countably generated non-bottom filter on `ι`, such that for almost all `x` in `α`, `f n x` converges to `g x` as `n` goes to `u`, then `g` is almost everywhere measurable.
|