Proof of $\int_{[0,\infty)}pt^{p-1}\mu(\{x:|f(x)|\geq t\})d\mu(t)=\int_{[0,\infty)}\mu(\{x:|f(x)|^p\geq s\})d\mu(s)$ Let $({\Bbb R},{\mathcal A},\mu)$ be the measure space where ${\mu}$ is the Lebesgue measure.  Assume that $\int_{\Bbb R}|f|^pd\mu<\infty$ ($p\geq1$). There is an exercise for proving that  

$$\int_{[0,\infty)}pt^{p-1}\mu(\{x:|f(x)|\geq t\})d\mu(t)=\int_{[0,\infty)}\mu(\{x:|f(x)|^p\geq s\})d\mu(s).$$

If one formally let $s=t^p$, then $ds=pt^{p-1}dt$ and one would immediately get the equality above. However, how can I justify it rigorously in the sense of Lebesgue integration?

[Edited]
What puzzles me is that I have the "change of variable" theorem for Riemann integration, but all the integrations here are in the Lebesgue sense. Unless one has shown that the integrands are also Riemann integrable, how can I directly use "change of variable"?
 A: This follows from a pointwise identity, namely the fact that, for every nonnegative $u$,

$$
\int_0^{+\infty}pt^{p-1}\mathbf 1_{u\geqslant t}\,\mathrm dt=u^p=\int_0^{+\infty}\mathbf 1_{u^p\geqslant s}\,\mathrm ds.
$$

Applying this to each $u=|f(x)|$ and integrating the result with respect to $\mathrm d\mu(x)$, one gets the desired identity, since
$$
\int_0^{+\infty}pt^{p-1}\mu(\{x:|f(x)|\geqslant t\})\,\mathrm dt
=
\int|f(x)|^p\,\mathrm d\mu(x)
=
\int_0^{+\infty}\mu(\{x:|f(x)|^p\geqslant s\})\,\mathrm ds.
$$
Edit: The use of $\mathrm d\mu(t)$ and $\mathrm d\mu(s)$ in the question is a tad misleading, I think. While $\mu$ in $\mu(\{x:|f(x)|\geqslant t\})$ and $\mu(\{x:|f(x)|^p\geqslant s\})$ can be any measure, $\mathrm d\mu(t)$ and $\mathrm d\mu(s)$ must really refer to the Lebesgue measure for the identity to hold. Hence the slight notational difference between this post and the question.
A: Let me try to show this by using the change of variables formula given here. 
Let $\lambda$ be the Lebesgue measure on $[0,\infty)$. Then
$$
I=\int_0^\infty\mu(\{x:|f(x)|^p\geq s\})\,\lambda(\mathrm ds)=\int_0^\infty \mu(\{x:|f(x)|\geq s^{1/p}\})\,\lambda(\mathrm ds)
$$
Let $f(t)=\mu(\{x:|f(x)|\geq t\})$ and define $\varphi(t)=t^{1/p}$ for $t\geq 0$, because then
$$
I=\int_0^\infty (f\circ \varphi)(s)\,\mathrm \lambda(\mathrm ds)=\int_0^\infty f(s) \lambda_\varphi(\mathrm ds),
$$
where $\lambda_\varphi=\lambda\circ \varphi^{-1}$ is the image measure. Now, if we can show that $\lambda_\varphi$ has density $t\mapsto  pt^{p-1}$ with respect to $\lambda$, then we are done. Here it is of course enough to look at intervals: For $a>0$
$$
\lambda_\varphi([0,a))=\lambda(\{t\geq 0:t^{1/p}\leq a\})=\lambda([0,a^p))=a^p=\int_{[0,a)}pt^{p-1}\,\lambda(\mathrm dt)
$$
meaning that indeed
$$
\frac{\mathrm d\lambda_\varphi}{\mathrm d\lambda}(t)=pt^{p-1},\quad t\geq 0.
$$
A: Primarily for my own benefit, I'd like to work out the details here. 


*

*We show that $
\int_{[0,\infty)}\mu(\{x\in\Bbb{R}\mid |f(x)|^p\geq s\}) \ d\mu(s)<\infty
$ by showing that $$
\int_{[0,\infty)}\mu(\{x\in\Bbb{R}\mid |f(x)|^p\geq s\}) \ d\mu(s)=\int_\Bbb{R}|f(x)|^p
\ d\mu(x).
$$
First of all, we claim that for a nonnegative measurable function $g:\Bbb{R}\to[0,\infty)$,
$$
\int_\Bbb{R}g(x)\ d\mu(x)=\int_{[0,\infty)}\mu(\{x\in\Bbb{R}\mid g(x)\geq s\}) \ d\mu(s).
$$
This is a good example of applications of the Fubini-Tonelli's Theorem. 
Let $\nu:=g_*\mu$ be the pushforward of $\mu$, i.e., $\nu=\mu\circ g^{-1}$. Then
$$
\int_\Bbb{R}g(x)\ d\mu(x)=\int_{[0,\infty)}x\ d\nu(x).
$$
Note that
$$
\begin{align*}
\int_{[0,\infty)}x\ d\nu(x)&=\int_{[0,\infty)}\left(\int_{[0,\infty)}1_{[0,x]}(y)\ d\mu(y)\right)\ d\nu(x)\\
&=\int_{[0,\infty)} \left(\int_{[0,\infty)}1_{[y,\infty]}(x)\ d\nu(x)\right)\ d\mu(y)\\
&=\int_{[0,\infty)} \nu([y,\infty))\ d\mu(y)\\
&=\int_{[0,\infty)} \mu\circ g^{-1}([y,\infty))\ d\mu(y)\\
&=\int_{[0,\infty)}\mu(\{x\in\Bbb{R}\mid g(x)\geq y\}) \ d\mu(y).
\end{align*}
$$
Replacing $g(x)$ with $|f(x)|^p$ one can see that
$$
\int_{[0,\infty)}\mu(\{x\in\Bbb{R}\mid |f(x)|^p\geq s\}) \ d\mu(s)=\int_\Bbb{R}|f(x)|^p
\ d\mu(x)<\infty
$$

*In the second part, we show the identity in the title. Define $\phi(s)=s^{1/p}$ and let
$$
F(t):=\mu(\{x:|f(x)|\geq t\}).
$$
Then 
$$
\begin{align*}
\int_{[0,\infty)}\mu(\{x:|f(x)|^p\geq s\})d\mu(s)=
\int_{[0,\infty)}\mu(\{x:|f(x)|\geq s^{1/p}\})d\mu(s)
=\int_XF(\phi(s))\ d\mu(s)
\end{align*}$$
where $X:=(0,\infty)$. Let $\lambda=\phi_*\mu$. Then, by the change of variables formula,
$$
\int_YF(t)\ d\lambda(t)=\int_XF(\phi(s))\ d\mu(s)
$$
where $Y=X=(0,\infty)$. It thus suffices to show that
$$
d\lambda(t)=pt^{p-1}d\mu(t).
$$
But $$
(\phi^{-1}(t))'=pt^{p-1}.
$$
It follows from Theorem 2.47 in Folland's Real Analysis that
$$
\lambda(E)=\mu\circ\phi^{-1}(E)=\int_{\phi^{-1}(E)}d\mu(t)=\int_Ept^{-1}d\mu(t).
$$

A: This ugly stated homework exercise (as @Did pointed out in his answer regarding the misleading notations) could be restated as follows. 

Consider a measure space $(X,\mathcal{A},\mu)$ with $\mu$ being $\sigma$-finite. Suppose $f\in L^p$ for some $1\leq p<\infty$. Then we have
  $$
\int_0^\infty pt^{p-1}\mu(|f|\geq t )\ dt=\int_0^\infty\mu ( |f|^p\geq s)\ ds.\tag{*}
$$

I was so obsessed with the change of variable formula in the setting of abstract measure spaces (see for instance Exercise 36 in this real analysis note by Tao) that I wanted to calculate the pushforward directly, which is not needed for this problem. 
The following is essentially elaborating @Did's answer, in which I didn't understand how to get the second formula. 
Note that the identity $(*)$ is equivalent to
$$
\int_0^\infty\left(\int_Xpt^{p-1}1_{|f|\geq t}\ d\mu\right)\ dt
=\int_0^\infty\left(\int_X1_{|f|^p\geq s}\ d\mu\right)\ ds.
$$
By Tonelli's theorem for non-negative functions, it suffices to show that
$$
\int_X\left(\int_0^\infty pt^{p-1}1_{|f|\geq t}\ dt\right)\ d\mu
=\int_X\left(\int_0^\infty 1_{|f|^p\geq s}\ ds\right)\ d\mu.
$$
But
$$
\int_0^\infty pt^{p-1}1_{|f|\geq t}\ dt=\int_0^{|f|}pt^{p-t}\ dt,\quad
\int_0^\infty 1_{|f|^p\geq s}\ ds=\int_0^{|f|^p}\ ds
$$
By the fundamental theorem of calculus, both are equal to $|f|^p$. QED.

One should note that the function $\mu(f>t):=\mu\{x\in X:f(x)>t\}$ is called the distribution function of $f$, which is clearly a monotonic (nonincreasing) function of $t$ and is therefore Borel measurable. See Rudin's Real and Complex Analysis (8.15) for a generalization of $(*)$ and also a related trick for controlling integrals at http://www.tricki.org/article/Control_level_sets.
