Take a distribution function $F$. If $Q_F : [0, 1] \rightarrow \mathbb{R}$ is defined by $Q(p) = \inf\{x | p \leq F(x)\}$, is it true that
$$E_F[X] = \int_0^1 Q_F d\mu$$
where $\mu$ is the Lebesgue measure. I've seen this result a thousand times for ``well-behaved'' distribution functions, but is it true in general? My conjecture is yes, via some carefully-defined-but-ex-post-obvious pushforward-measure argument/change of variables. Can anyone help fill in the blanks?
My conjecture: We can simultaneously consider F as both a measure (as in a Lebesgue-Stieltjes integral) and a measurable mapping from supp(F) to [0,1]. I think that then the pushforward measure of F (using function F) is then equivalent to the Lebesgue measure on [0,1], and the standard change-of-variable formula applies, so
$$ \int_0^1 Q_F \ d(F_{*}F) = \int_{supp(F)} Q_F \circ F \ dF$$
But $F_{*}F = \mu$ (the standard Lebesgue measure) and $Q_F \circ F$ is simply the identity function, so we would have:
$$ \int_0^1 Q_F \ d\mu = \int_{supp(F)} \mu \ dF =: E_F[X].$$
But I am relatively untrained in all of this and have just tried to learn by Googling, so don't have much confidence that any of the above is rigorously correct.