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] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → X → E} [TopologicalSpace.IsCompletelyPseudoMetrizableSpace 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] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → X → E} [hE : Nonempty E] [TopologicalSpace.IsCompletelyMetrizableSpace E] (hf : ∀ (i : ι), StronglyMeasurable (f i)) : StronglyMeasurable fun (x : X) => l.limUnder fun (x_1 : ι) => f x_1 x

theorem MeasureTheory.StronglyMeasurable.tprod {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [CommMonoid E] [TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [ContinuousMul E] [Countable ι] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E} (h : ∀ (i : ι), StronglyMeasurable (f i)) : StronglyMeasurable fun (x : X) => ∏'[L] (i : ι), f i x

The product of strongly measurable functions is measurable.

theorem MeasureTheory.StronglyMeasurable.tsum {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [AddCommMonoid E] [TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [ContinuousAdd E] [Countable ι] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E} (h : ∀ (i : ι), StronglyMeasurable (f i)) : StronglyMeasurable fun (x : X) => ∑'[L] (i : ι), f i x

The sum of strongly measurable functions is measurable.

theorem MeasureTheory.AEStronglyMeasurable.tprod {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [CommMonoid E] [TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [ContinuousMul E] [Countable ι] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {μ : Measure X} {f : ι → X → E} (h : ∀ (i : ι), AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (fun (x : X) => ∏'[L] (i : ι), f i x) μ

The product of almost everywhere strongly measurable functions is measurable.

theorem MeasureTheory.AEStronglyMeasurable.tsum {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [AddCommMonoid E] [TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [ContinuousAdd E] [Countable ι] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {μ : Measure X} {f : ι → X → E} (h : ∀ (i : ι), AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (fun (x : X) => ∑'[L] (i : ι), f i x) μ

The sum of almost everywhere strongly measurable functions is measurable.

theorem MeasureTheory.StronglyMeasurable.tprod' {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [CommMonoid E] [TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousMul E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E} (h : ∀ (i : ι), StronglyMeasurable (f i)) : StronglyMeasurable (∏'[L] (i : ι), f i)

The product of strongly measurable functions is measurable.

theorem MeasureTheory.StronglyMeasurable.tsum' {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [AddCommMonoid E] [TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousAdd E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E} (h : ∀ (i : ι), StronglyMeasurable (f i)) : StronglyMeasurable (∑'[L] (i : ι), f i)

The sum of strongly measurable functions is measurable.

theorem MeasureTheory.AEStronglyMeasurable.tprod' {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [CommMonoid E] [TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousMul E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {μ : Measure X} {f : ι → X → E} (h : ∀ (i : ι), AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (∏'[L] (i : ι), f i) μ

The product of almost everywhere strongly measurable functions is measurable.

theorem MeasureTheory.AEStronglyMeasurable.tsum' {X : Type u_4} {E : Type u_5} {ι : Type u_6} [MeasurableSpace X] [AddCommMonoid E] [TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousAdd E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {μ : Measure X} {f : ι → X → E} (h : ∀ (i : ι), AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (∑'[L] (i : ι), f i) μ

The sum of almost everywhere strongly measurable functions is measurable.