Results about strongly measurable functions #
In measure theory it is often assumed that some space is a PolishSpace, i.e. a separable and
completely metrizable topological space, because it ensures a nice interaction between the topology
and the measurable space structure. Moreover a strongly measurable function whose codomain is a
metric space is measurable and has a separable range
(see stronglyMeasurable_iff_measurable_separable). Therefore if the codomain is also complete,
by corestricting the function to the closure of its range, some results about measurable functions
can be extended to strongly measurable functions without assuming separability on the codomain.
The purpose of this file is to collect those results.
theorem
MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace E]
[TopologicalSpace.IsCompletelyMetrizableSpace E]
[Countable ι]
{l : Filter ι}
[l.IsCountablyGenerated]
{f : ι → X → E}
(hf : ∀ (i : ι), StronglyMeasurable (f i))
:
MeasurableSet {x : X | ∃ (c : E), Filter.Tendsto (fun (x_1 : ι) => f x_1 x) l (nhds c)}
theorem
MeasureTheory.StronglyMeasurable.limUnder
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[MeasurableSpace X]
[TopologicalSpace E]
[TopologicalSpace.IsCompletelyMetrizableSpace E]
[Countable ι]
{l : Filter ι}
[l.IsCountablyGenerated]
{f : ι → X → E}
[hE : Nonempty E]
(hf : ∀ (i : ι), StronglyMeasurable (f i))
:
StronglyMeasurable fun (x : X) => _root_.limUnder l fun (x_1 : ι) => f x_1 x