Nested sampling: Bayesian evidence integral transformation proof I am trying to work out how the Bayesian evidence integral ($\equiv Z$) is transformed to a one-dimensional integral as presented in John Skilling's nested sampling paper (page 2): https://projecteuclid.org/download/pdf_1/euclid.ba/1340370944
I'll quote his steps here:
We want to evaluate
\begin{equation}
\label{one} \tag{1}
Z = \int_{\hat{y}} L(y) \pi(y) \mathrm{d}y,
\end{equation}
where $y$ is a parameter (possibly a vector of parameters) $L(y)$ is the likelihood function and $\pi(y)$ is the prior function. $\hat{y}$ is the support of $\pi(y)$. 
Skilling then defines an infinitesimal unit of `prior mass' $\mathrm{d}X$ to be 
\begin{equation}
\label{two}\tag{2}
\mathrm{d}X = \pi(y) \mathrm{d}y
\end{equation}
and
\begin{equation}
\label{three}\tag{3}
X(\lambda) = \int_{L(y) > \lambda} \pi(y) \mathrm{d}y.
\end{equation}
i.e. $X(\lambda) $ is the integral over the prior at all points for which $L(y) > \lambda$ is satisfied, which means $X \in [0, 1]$.
The method makes sense up to this point, but then he sets $L(X)$ equal to the inverse of equation \ref{three} ($L(X) \equiv \lambda(X)$) and from that deduces
\begin{equation}
\label{four}\tag{4}
Z = \int_{0}^{1} L(X) \mathrm{d}X.
\end{equation}
Intuitively I can see how equation \ref{four} arises, but I cannot see how it is mathematically derived from inverting equation \ref{three}. Could anyone provide a proof for this relation? 
I have tried interpreting the integral on the RHS of equation \ref{three} as $P(y | L(Y) > \lambda)$ where $P(\cdot|\cdot)$ is the conditional CDF of the prior,
and applying the inverse function theorem $(L'(X) = 1 / \pi(y | L(Y) > \lambda)$ but I feel like I am going nowhere fast.
Is it possible to show this mathematically without a knowledge of measure theory? If not, could you describe the relevant theory to look up to understand the problem more.
Thanks
EDIT: Response to Bridgeburner's answer
If $L(y) = \lambda$ for more than
one value of $y$ (which is generally the case for likelihood
functions), can you still swap the order of integration between $y$
and $\lambda$? 
My guess is you can swap the order, since if you split up the integration over $y$ into $n$ separate regions where in each region you get one occurrence of $L(y) = \lambda$, then: 
\begin{equation}
\label{five}\tag{5}
\int_{\hat y} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y = \int_{\hat y_1} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y~+~ ...~+~\int_{\hat y_n} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y,
\end{equation}
then the double integral becomes
\begin{equation}
\label{six}\tag{6}
-\int \lambda \int_{\hat y} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y  \mathrm{d}\lambda = -\int \lambda \left[ \int_{\hat y_1} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y 
\quad+ ~... ~+ \int_{\hat y_n} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y \right] \mathrm{d} \lambda,
\end{equation}
and the order of each integral can be re-arranged (I think)
\begin{equation}
\label{seven}\tag{7}
 -\int_{\hat y_1} \pi(y) \left[ \int \lambda \delta(L(y) - \lambda) \mathrm{d}\lambda \right] \mathrm{d}y~+ ~...~+~\int_{\hat y_n} \pi(y) \left[ \int \lambda \delta(L(y) - \lambda)  \mathrm{d} \lambda \right] \mathrm{d}y,
\end{equation} 
which would also lead to the desired result.
I am trying to relate this to Fubini's theorem, but I am unsure how it is affected by the fact that we are integrating over a delta function.
I guess a more general question I have following Bridgeburner's answer is, how does integrating over a delta function affect the applicability of Fubini's theorem?
 A: Edit: made assumptions explicit.
Edit 2: added a method with less assumptions.
I know that this question is 3 years old, but I found myself trying to understand this method and found this question in the process. I'll try to give a more probabilistic proof of Eq 4. Let us establish first that Eq 3 means simply
$$
X(\lambda) = \int_{\theta:L(\theta)>\lambda} \pi(d\theta) = \int_{\Theta} \boldsymbol{1}\{L(\theta)>\lambda\}\pi(d\theta) = \pi(L(\theta)>\lambda)
$$
where the notation $\pi(A)$ is the probability under the prior of the set $A$. Going back to the definition of $Z$, using the formula for the expectation of a non-negative random variable gives
$$
Z = \mathbb{E}_{\theta\sim\pi}[L(\theta)] = \int_0^\infty \pi(L(\theta)>L)dL = \int_0^\infty X(L)dL
$$
Method 1
Note that the integral can be trivially expressed as integration over a subset of $\mathbb{R}^2$
$$
Z = \int_0^\infty X(L)dL = \int_0^\infty\left[\int_0^{X(L)} 1 dX\right]dL
$$
But the same set can be reparametrized using the inverse function $L(x) = X^{-1}(x)$, so that the integral can be written as
$$
Z = \int_0^1\left[\int_0^{L(X)} 1dL\right]dX = \int_0^1 L(X)dX.
$$
This is Eq. 4.
To understand the intuition of the re-parametrization, consider Fig. 1 in the paper. The original integral corresponds to integrating "Area Z" with horizontal bars (as in Riemannian integration), whereas the re-parametrization computes the same area with vertical bars.
Method 2
To get Eq. 4, we do integration by parts. To do this, we impose a differentiability assumption.
Assumption: $X(L)$ is differentiable.
Then,
$$
\frac{d}{dL}[LX(L)] = X(L) + LX'(L)
$$
Integrating both sides w.r.t. $\int_0^\infty [...]dL$ gives
$$
\lim_{L\to\infty}LX(L) - 0\cdot X(0) = \int_0^\infty X(L)dL + \int_0^\infty LX'(L)dL
$$
To deal with the limit we require an additional assumption.
Assumption: Let $\pi_L$ be the push-forward of the prior $\pi$ under the Likelihood function $L(\theta)$. Overloading notation, let us call $\pi_L(L)$ its density (note that this density exists because of the previous assumption). Then we assume that the tails of $\pi_L$ decay faster than $L^{-2}$
$$
\lim_{L\to\infty} L^2\pi_L(L) = 0
$$
Now, using L'Hôpital's rule
$$
\lim_{L\to\infty}\frac{X(L)}{L^{-1}} = \lim_{L\to\infty}\frac{\pi_L(L)}{L^{-2}} = 0
$$
Thus
$$
Z = \int_0^\infty X(L)dL = - \int_0^\infty LX'(L)dL
$$
Now we do a change of variables $L \to L(X)$, so that
$$
dL = L'(X)dX = [X'(L(X))]^{-1} dX
$$
where we used the formula for the derivative of the inverse of a function. Moreover, note that when $L=0$ we have $X=1$ and when $L=\infty$ we get $X=0$. Putting everything together yields
$$
Z = - \int_0^\infty LX'(L)dL = - \int_1^0 L(X) X'(L(X)) [X'(L(X))]^{-1} dX = \int_0^1 L(X) dX
$$
which completes the proof.
A: The expression for $X$ can be rewritten:
$$
X(\lambda) = \int_\hat{y} \pi(y) \Theta(L(y) - \lambda) \mathrm{d}y,
$$
where $\Theta(x)$ is the Heaviside step function, which satisfies $\frac{\mathrm{d}}{\mathrm{d}x} \Theta(x) = \delta(x),$ the Dirac delta function. So,
$$
\frac{\mathrm{d}X}{\mathrm{d}\lambda} = -\int_\hat{y} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y.  
$$
Now the final form of the integral, as you expressed it, can be re-expressed as an integral over $\lambda$ by making a change of variables from $X$ to $\lambda$,
$$
\begin{split}
Z &= \int_0^1 \lambda(X) \mathrm{d}X \\
&= \int \lambda \cdot \left( \frac{\mathrm{d}X}{\mathrm{d}\lambda} \right) \mathrm{d}\lambda \\
&= -\int \lambda \int_{\hat y} \pi(y) \delta(L(y) - \lambda) \mathrm{d}y \mathrm{d}\lambda.
\end{split}
$$
Because the outer integral is over all possible values of $\lambda,$ and the inner integral is over all $\hat y,$ there is no dependence of the bounds on each others' variable, so the order of integration can simply be switched.
$$
\begin{split}
Z &= \int_{\hat y} \pi(y) \left( -\int \lambda \delta(L(y) - \lambda) \mathrm{d} \lambda \right) \mathrm{d}y \\
&= \int_{\hat y} \pi(y) L(y) \mathrm{d}y.
\end{split}
$$
A: There is a 36-page paper by Doris Schneider and Philipp Wacker posted on the arXiv (https://arxiv.org/abs/2005.08602) entirely dedicated to this proof. It turns out the original nested sampling paper by Skilling glossed over an idea that ended up being much more complicated in some cases. The theorem still holds, but for example, Skilling says that L is the inverse of X, while Schneider and Wacker show that's not true (page 8).
It's impossible to condense such a paper into a single answer, but the rough idea is that if your likelihood has a flat spot of nonzero prior probability, things start to fall apart.
