Doob-Dynkin Factorization

Abstract

Standard-Borel measurable refinement is generated-information inclusion.

Theorem 1.1 (Measurable refinement is information inclusion).

$$\begin{array}{c}\forall X,BC,BD:\mathrm{Type},\\ [\mathrm{MeasurableSpace}\left(BC\right)],[\mathrm{MeasurableSpace}\left(BD\right)],\\ [\mathrm{Nonempty}\left(BC\right)],[\mathrm{StandardBorelSpace}\left(BC\right)],\\ C:X\to BC,D:X\to BD,\\ (\mathrm{Measurable}\left(C,\mathrm{generated}\left(D\right)\right)\Rightarrow \exists p:BD\to BC,\mathrm{Measurable}\left(p\right)\wedge C=\mathrm{compose}\left(p,D\right))\wedge \\ (\exists p:BD\to BC,\mathrm{Measurable}\left(p\right)\wedge C=\mathrm{compose}\left(p,D\right)⟺\mathrm{generated}\left(C\right)\subseteq \mathrm{generated}\left(D\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/MeasurableRefinement/DoobDynkinFactorization.measurable_refinement_iff_generated_information_inclusion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The information generated by a concept is the pullback measurable space along its readout. Measurability of C for the pullback along D therefore means that C observes no more events than D.

For a nonempty standard-Borel codomain, the pinned Mathlib Doob-Dynkin theorem supplies a measurable map p with C equal to p composed with D.

Conversely, composing a measurable p with the canonical measurable map into D’s pullback space proves inclusion of the generated measurable spaces. The two directions give the stated equivalence.

References

• Truth anchor: D5/S3/ConceptDynamics/MeasurableRefinement/DoobDynkinFactorization.measurable_refinement_iff_generated_information_inclusion
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition