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 though f, which means that there exists h : Y → Z such that g = h ∘ f.

TODO

• Under certain assumptions, the factorization map h is measurable. This is the content of the Doob-Dynkin lemma.

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.

TODO: under certain assumptions, the factorization map h is measurable. This is the content of the Doob-Dynkin lemma.

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.