Let $X$ be a compact metric space, and let $\mathcal P(X)$ be the (compact, metrisable) space of Borel probability measures on $X$. Similarly, $\mathcal P (\mathcal P (X))$ is the space of Borel probability measures on $\mathcal P (X)$. I want to make sense of the integral $$ \int_{\mathcal P(X)} \mu \,\mathrm d \mathcal \tau (\mu) \tag{INT}\label{INT} $$ where $\tau \in \mathcal P (\mathcal P (X))$. Is there an elementary definition of this integral? (See the end of the question for an elaboration of what I mean by "elementary".)
It seems one way to interpret \eqref{INT} is to view it as a Bochner integral, by considering $\mathcal P(X)$ as a (compact, convex) subset of the Banach space of finite signed Borel measures on $X$ with the total variation norm. One property of the Bochner integral is that, for any bounded operator $T\colon \mathcal P(X) \to Y$ where $Y$ is another Banach space, we have that $$ \int_{\mathcal P (X)} T\mu\,\mathrm d\tau (\mu) = T \left( \int_{\mathcal P(X)} \mu \,\mathrm d \mathcal \tau (\mu) \right). \tag{*}\label{*} $$
In particular, suppose that $Y = L(C(X),\mathbb R)$, the space of bounded linear functionals on $C(X)$, and $T$ is the operator given by $$ \mu \mapsto \left(\begin{align*} C(X) &\to \mathbb R \\ f &\mapsto \int_X f(x) \,\mathrm d \mu(x) \end{align*}\right). $$ Then, we can parse \eqref{*} as $$ \int_X f(x) \, \mathrm d \mu_0 (x) = \int_{\mathcal P(X)} \int_X f(x) \,\mathrm d \mu(x) \,\mathrm d \tau (\mu) \tag{+} \label{+} $$ for each $f \in C(X)$, where $\mu_0$ is just the value of \eqref{INT}.
Hopefully, everything I've said so far is correct. (Please do point out mistakes if there are any.) If so, can I take \eqref{+} as the definition of \eqref{INT}? That is, I would like to define \eqref{INT} as the $\mu_0 \in \mathcal P(X)$ that satisfies \eqref{+} for each $f \in C(X)$. Do I lose any important properties of the integral by using this definition?
I am looking for a definition of \eqref{INT} without too much additional machinery, beyond what you would see in a typical introductory measure theory or functional analysis course. I was hoping \eqref{+} would do, but I am also open to alternative suggestions.
Additionally, if anyone can recommend a nice, readable reference for this material, I'd appreciate that as well. An ideal reference would be one that's accessible to someone who only knows a little measure theory and functional analysis, but I'll take what I can get.
Best Answer
This is a really interesting question! I think $(+)$ is the only sensible definition of $\mu_0$. As you correctly observed, this follows once we've decided to define $\mu_0$ using Bochner integration.
But the Bochner integral is the unique linear map satisfying a few "obvious" criteria, like the $L^1$ triangle inequality and dominated convergence. See Bochner Integral: Axioms. If you want to define $\mu_0$ in any way that is vaguely useful, it had better satisfy those axioms.
Per the discussion in the comments, let me outline how one could express the Bochner integral in terms of the Lebesgue integral. Let $X$ be a measure space, $B$ a Banach space, $B^*$ its dual, and $L^1(X \to B)$ the space of Bochner-integrable functions $X \to B$.
By the Hanh-Banach theorem, for every $x,y \in B$, $x=y$ if and only if for every $\varphi \in B^*$, $\varphi(x) = \varphi(y)$. In other words, to specify a point $x \in B$, it suffices to specify $\varphi(x)$ for every linear functional $\varphi$ (though there is no guarantee that $x$ will exist, and this seems unfixable due to Enflo's theorem that there are Banach spaces which do not admit a Schauder basis, if $x$ exists this uniquely defines it; maybe $\mathcal P(X)$ actually has a Schauder basis, and then you can just use the Schauder basis rather than fiddle around with linear functionals like this).
As you observe, the Bochner integral commutes with bounded linear maps. In particular it commutes with bounded linear functionals, i.e. elements of $B^*$. So if $f \in L^1(X \to B)$, we have $$\varphi\left(\int_X f(x)~dx\right) = \int_X \varphi(f(x)) ~dx.$$ Here the integral $\int_X \varphi(f(x))~dx$ is just the plain jane Lebesgue integral. We have specified $\varphi\int_Xf$ for every $\varphi$, so we have specified $\int_Xf$, provided that $\int_Xf$ actually exists. (It does, by the usual construction of the Bochner integral in terms of ISF, but the point of this outline was to give a cheap definition that averts this modulo technical details.)