Channel action on probability measures

For arbitrary types $X$ and $Y$, each equipped with a measurable-space structure, a kernel $K$ from $X$ to $Y$ (a measurable assignment to each $x \in X$ of a measure $K(x)$ on $Y$), an assumption that $K$ is a Markov kernel, meaning that $K(x)(Y)=1$ for every $x \in X$, and a probability measure $\mu$ on $X$, meaning a measure with $\mu(X)=1$, the definition $\operatorname{DuchiSIT.channel}(K,\mu)$ returns a probability measure on $Y$. Its underlying measure is the measure obtained by binding $\mu$ with $K$: for every measurable set $A \subseteq Y$,

where this is the nonnegative extended-real integral. The returned value packages this measure together with the fact that its total mass is one; it does not perform any additional normalization. The spaces and their measurable structures are arbitrary, with no finiteness, countability, topology, or standard-Borel assumption. The requirement that $K(x)$ have mass one holds at every $x$, including points in sets of $\mu$-measure zero. If $X$ is empty there is no admissible probability measure $\mu$; if $Y$ is empty and $X$ is nonempty there is no admissible Markov kernel $K$, so no inputs satisfy all requirements in either empty-space case. The displayed evaluation formula is stated for measurable sets; the returned object itself is a measure, defined on all subsets with the usual measure-theoretic convention.