Darth Vader Rule: what is the reason for its name, and a formal proof?
A basic proof uses Lebesgue Integration.
Let $S(x)$ be a survival function on $x\in [0,\infty]$, then $S(x)$ is a monotonically decreasing function starting at $S(0)=1$ and $\lim\limits_{x\rightarrow \infty} S(x)= 0$.
Now, lets calculate the area under the curve using a Lebesgue Sum, of $S(x)$.
$L_S:= \sum\limits_{\eta_i\in \chi_S} \Delta(\eta_i)\mu(S^{-1}(\eta_i))$
Where:
- $\chi_S$ is a partition of the range of $S(x)$ into a set of intervals.
- $\Delta(\eta_i)$ is the length of interval $\eta_i \in \chi_S$
- $\mu(S^{-1}(\eta_i))$ is the Lebesgue measure $\mu$ (i.e., total length) of the interval on the x-axis where $S(x)\geq \inf \eta_i$
Such an integral can be hard to interpret. However, since $S(x)$ is monotonic-decreasing, we know that the set of $x$ values in each term of the summation will have a special property: $\mu(S^{-1}(\eta_i))=x_i:S(x)=\inf \eta_i$, which means we can dispense with the Lebesgue measure and just use the actual function inverse:
$L_S := \sum\limits_{\eta_i\in \chi_S} \Delta(\eta_i)S^{-1}(\eta_i)$
Now, lets take the limit of the Lebesgue sum to get a Lebesgue Integral:
$\lim\limits_{\Delta(\eta_i)\rightarrow 0} \sum\limits_{\eta_i\in\chi_S} \eta_i\mu(S^{-1}(\eta_i)) = \int_0^1 S^{-1}(z)dz$ [This can be envisioned as the limit of a series of stacked rectangles (i.e. a Riemann sum on the inverse of S)].
However, note that $dz = dS = dP$; thus, an interval on the y-axis represents a probability, and the limit of this interval represents a density, so we can re-write the integral using the fact that $\int f(x) dx = \int f^{-1}(y) dy$:
$\int_0^1 S^{-1}(z)dz = \int_0^{\infty} xdS=\int_0^{\infty} xdP = E[X]\;\;\text{ where } F_X(x)=1-S(x)$
On the naming question:
This expectation result has been around for a long time (e.g., you can find it in old probability books by Feller), and it appears to have been designated as the "Darth Vader rule" only quite recently. The earliest reference I can find to this name in the literature is in Muldowney, Ostaszewski and Wojdows (2012), who appear to be the ones who coined the name. They give an explanation for the name in a footnote, saying that the "...designation may capture the somewhat counterintuitive—if not slightly unsettling and surreal—impression which the result can evoke on first encounter" (p. 53, Footnote 1).
Honestly, that seems like an extremely tenuous reason for the name to me, firstly because almost every mathematical theorem seems unsettling and mysterious when you are not familiar with it, and secondly because there are plenty of other movie villains that are more unsettling and surreal than Darth Vader (the "Blair Witch rule" perhaps?). So, I think the correct answer is: there is no sensible reason why the rule is called by this name --- some maths guys just thought it would be a cool name because they are Star Wars nerds.
Notwithstanding the fact that there does not appear to be any sensible logical basis for the name, that does not really matter too much in mathematics. The main purpose of naming mathematical rules is so that we have a shared language to refer to them easily, and a silly name is just as good for this as a sensible name. For that reason, I have no problem referring to the rule by that name, and I hope it catches on widely enough that it adds to the shared language of mathematics.