Measurable Factor Information Inclusion

Abstract

A measurable factorization includes the generated information space.

Theorem 1.1 (Measurable factorization implies generated-information inclusion).

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

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

Source. Repository-derived.

Commentary.

The information generated by a readout is its codomain measurable space pulled back to the state carrier. The displayed factorization and measurability conditions are the complete hypotheses.

Pullback along a composite equals iterated pullback. Measurability of p then makes the pullback along C no larger than the pullback along D, which is exactly the displayed event inclusion.

References

• Truth anchor: D5/S3/ConceptDynamics/MeasurableRefinement/MeasurableFactorInformationInclusion.measurable_factorization_generated_information_inclusion
• Dependency: D5/S3/ConceptDynamics/MeasurableRefinement/DoobDynkinFactorization