Measurability of functions with multiple parameters

Question

For a formalisation of the Giry monad in a theorem prover, I think I require some notion of measurability of “curried” functions. I.e. I have measure spaces $A$, $B$, and $C$ and a function $f: A \rightarrow (B \rightarrow C)$ and want it to be “measurable”, but for that I would, of course, require some way of constructing a measure space “$B \rightarrow C$”, and I don't know how to do that.

What I definitely need is that all projections of $f$, i.e. one parameter is fixed, yielding functions $A \rightarrow C$ and $B\rightarrow C$, respectively, must be measurable.

My approach of tackling this is by using the isomorphism between $A \rightarrow (B \rightarrow C)$ and $A \times B \rightarrow C$ and demanding that the equivalent function $g: A\times B \rightarrow C$ with $g(a,b) = f(a)(b)$ be measurable w.r.t. $A\otimes B$ and $C$. This would probably work.

However, since I operate within Higher Order Logic, where functions are traditionally curried, not tupled, a formulation of measurability that directly works for a function in $A \rightarrow (B\rightarrow C)$ would be more natural and easier to use, so I would like to know if there is such a concept of measurability, i.e. a “measure space $B \rightarrow C$ of measurable functions.”

Intuitively, I would think there should be, seeing as tupled and curried functions are isomorphic.

EDIT: I just found this interesting answer that seems to be related, but am not quite sure if it helps me here: https://mathoverflow.net/a/120736/32355

Answer 1

My advisor, Johannes Hölzl, apparently found a solution to this (and proved it formally, in Isabelle/HOL): there is no solution, since measurable spaces are not a cartesian-closed category, as, e.g.:

Let $\mathcal M_1 = \mathfrak P(\mathbb R)$, $\mathcal M_2 = \{\{x\}\,|\,x\in\mathbb R\}$, and $\mathcal N = \mathfrak P(\mathbb B)$.

It can be shown that there is no measurable space $\mathcal N'$ such that $$f\ \,\mathsf{is}\ \,\mathcal M_1\mathsf{-}\mathcal N'\hskip-0.7mm\mathsf{-measurable}\ \longleftrightarrow\ (\lambda x\,y.\;f(x,y))\ \,\mathsf{is}\ \,\mathcal M_1\hskip-1mm\otimes\hskip-0.7mm\mathcal M_2\mathsf{-}\mathcal N\hskip-0.5mm\mathsf{-measurable}\;.$$