Factorization of a map from measurability

Consider f : X → Y and g : X → Z and assume that g is measurable with respect to the pullback along f. Then g factors through f, which means that (if Z is nonempty) there exists h : Y → Z such that g = h ∘ f.

If Z is completely metrizable, the factorization map h can be taken to be measurable. This is the content of the Doob-Dynkin lemma: see exists_eq_measurable_comp.

theorem Measurable.factorsThrough {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [MeasurableSpace Z] [MeasurableSingletonClass Z] (hg : Measurable g) : Function.FactorsThrough g f

If a function g is measurable with respect to the pullback along some function f, then to prove g x = g y it is enough to prove f x = f y.

theorem MeasureTheory.StronglyMeasurable.factorsThrough {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] [T1Space Z] (hg : StronglyMeasurable g) : Function.FactorsThrough g f

If a function g is strongly measurable with respect to the pullback along some function f, then to prove g x = g y it is enough to prove f x = f y.

If Z is not empty there exists h : Y → Z such that g = h ∘ f. If Z is also completely metrizable, the factorization map h can be taken to be measurable (see exists_eq_measurable_comp).

theorem MeasureTheory.StronglyMeasurable.exists_eq_measurable_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [Nonempty Z] [TopologicalSpace Z] [TopologicalSpace.IsCompletelyMetrizableSpace Z] (hg : StronglyMeasurable g) : ∃ (h : Y → Z), StronglyMeasurable h ∧ g = h ∘ f

If a function g is strongly measurable with respect to the pullback along some function f, then there exists some strongly measurable function h : Y → Z such that g = h ∘ f.

theorem Measurable.exists_eq_measurable_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [Nonempty Z] [MeasurableSpace Z] [StandardBorelSpace Z] (hg : Measurable g) : ∃ (h : Y → Z), Measurable h ∧ g = h ∘ f

If a function g is measurable with respect to the pullback along some function f, then there exists some measurable function h : Y → Z such that g = h ∘ f.

theorem Measurable.dependsOn_of_piLE {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z} [Preorder ι] {i : ι} [MeasurableSpace Z] [MeasurableSingletonClass Z] (hf : Measurable f) : DependsOn f (Set.Iic i)

If a function is measurable with respect to the σ-algebra generated by the first coordinates, then it only depends on those first coordinates.

theorem MeasureTheory.StronglyMeasurable.dependsOn_of_piLE {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z} [Preorder ι] {i : ι} [TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] [T1Space Z] (hf : StronglyMeasurable f) : DependsOn f (Set.Iic i)

If a function is strongly measurable with respect to the σ-algebra generated by the first coordinates, then it only depends on those first coordinates.

theorem Measurable.dependsOn_of_piFinset {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z} {s : Finset ι} [MeasurableSpace Z] [MeasurableSingletonClass Z] (hf : Measurable f) : DependsOn f ↑s

If a function is measurable with respect to the σ-algebra generated by the first coordinates, then it only depends on those first coordinates.

theorem MeasureTheory.StronglyMeasurable.dependsOn_of_piFinset {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z} {s : Finset ι} [TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] [T1Space Z] (hf : StronglyMeasurable f) : DependsOn f ↑s

If a function is strongly measurable with respect to the σ-algebra generated by the first coordinates, then it only depends on those first coordinates.