Conull Image Probability Isomorphism

Abstract

A conull measurable injection pulls a probability law back to its domain.

Theorem 1.1 (A conull measurable injection is a probability isomorphism).

$$\begin{array}{c}\forall X,O:\mathrm{Type},\\ \mathrm{StandardBorel}\left(X\right),\mathrm{StandardBorel}\left(O\right),\\ q:X\to O,\mathrm{Measurable}\left(q\right),\mathrm{Injective}\left(q\right),\\ \nu :\mathrm{ProbabilityMeasure}\left(O\right),\nu (\mathrm{range}\left(q\right))=1\Rightarrow \\ e=\mathrm{equivRange}\left(q\right),rho=\mathrm{comap}\left(coe,\nu \right),\\ \exists \mu :\mathrm{ProbabilityMeasure}\left(X\right),\mathrm{map}\left(q,\mu \right)=\nu \wedge \\ \mathrm{MeasurePreserving}\left(e,\mu ,rho\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/ConullImageProbabilityIsomorphism.conull_measurable_injection_probability_isomorphism (✓ std3). ∎

Source. Repository-derived.

Commentary.

The standard Borel hypotheses turn the measurable injection q into a measurable embedding. Its canonical equivalence e identifies X directly with the measurable subtype range(q).

The measure rho is constructed by pulling nu back along subtype inclusion. Full mass of range(q) makes its pushforward exactly nu, and therefore makes rho a probability measure.

Mapping rho back through the measurable inverse of e constructs mu. The public conclusions state both map(q, mu) = nu and that e is measure-preserving from mu to rho, exposing the conull-space isomorphism rather than wrapping it in mere inhabitation.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/ConullImageProbabilityIsomorphism.conull_measurable_injection_probability_isomorphism