intuitively obvious integration identity Let $\mu$ denote the Lebesgue measure on $[-\infty,\infty]$.
For each measurable subset $E\subset(0,\infty)$, define the nondecreasing function $m_E:(0,\mu(E))\to(0,\infty)$ by the rule
$$m_E(t)=\inf\left\{s\in(0,\infty):\mu\left(E\cap(0,s)\right)=t\right\}.$$
Question 1.  I would like to show the following:  If $f:(0,\infty)\to[0,\infty]$ is a (nonnegative) measurable function, then
$$\int_Ef(t)\;dt=\int_0^{\mu(E)}(f\circ m_E)(t)\;dt.$$
Discussion.
My intuition tells me it should work, but I'm too rusty on my measure theory to prove it.
The analogy here is to the $\ell_1$ norm of subsequences.  For example, if $B\subset\mathbb{N}$, then let
$$i_B(n)=\left\{i\in B:\#\left(B\cap[0,i]\right)\leq n\right\}.$$
It follows that, for any sequence of nonnegative scalars $(a_n)_{n=1}^\infty$, we have
$$\sum_{n\in B}a_n=\sum_{n=1}^{\#B}a_{i_B(n)}.$$
In other words, we have "pushed" $(a_n)_{n\in B}$ down to $(a_{i_B(n)})_{n=1}^{\#B}$ so that their $\#$-integrals are the same.
I would like to construct an analogous transformation to work with nonnegative functions on $(0,\infty)$.
Thanks!
 A: Let $\lambda$ denote Lebesgue measure.  For any finite measure $\nu$ on $[0,\infty)$, let $m_{\nu}(t)=\inf{\!(\{s:\nu([0,s))=t\})}$.
Lemma. $m_{\nu}:([0,\infty);\nu)\to([0,\infty);\lambda)$ is a measure-preserving transformation for Borel sets.
Proof.  The Borel $\sigma$-algebra is generated by sets of the form $[0,t)$, and it is elementary that $m_{\nu}$ is measure-preserving on those sets.  QED.
Corollary. For any Borel-measurable $f$ and finite measure $\nu$, $$\int{f\,d\nu}=\int{(f\circ m_{\nu})\cdot 1_{[0,\nu([0,\infty)))}\,d\lambda}$$
Proof. Elementary application of layer-cake decomposition.  QED.
Lemma. The same holds for any $\nu\ll\lambda$.
Proof.  By linearity, we may suppose $f\geq0$ w/oLoG.  Let $\nu_N(S)=\nu(S\cap[0,N))$; note that $\nu_N$ is a finite measure and so $$\int{f\,d\nu_N}=\int{(f\circ m_{\nu_N})\cdot 1_{[0,\nu_N([0,\infty)))}\,d\lambda}$$   Now take $N\to\infty$; both sides converge to $$\int{f\,d\nu}=\int{f\circ m_{\nu}\,d\lambda}$$ by the monotone convergence theorem.  QED.
Corollary. Your claim holds for Borel-measurable functions.
Proof. Let $\nu(S)=\lambda(E\cap S)$ and apply the previous lemma.  QED.
Corollary. Your claim holds for any Lebesgue-measurable function.
Proof. Every Lebesgue-measurable function is a.e. equal to a Borel-measurable one.  QED.
