Virtual-surplus revenue identity (source code)

= Virtual-surplus revenue identity
{title2=$\mathbb E\sum_i P_i(V_i)=\mathbb E\sum_i\phi_i(V_i)X_i(V_i)-\sum_i U_i(\underline v_i)$}

For an <independent private values model>, let $X_i(v)$ and $P_i(v)$ be interim allocation and payment. The <interim payment identity> gives $P_i(v)=vX_i(v)-U_i(\underline v_i)-\int_{\underline v_i}^vX_i(t)dt$. Applying <Fubini's theorem> to reverse the order of integration yields $\mathbb E\int_{\underline v_i}^{V_i}X_i(t)dt=\int X_i(t)(1-F_i(t))dt$. Subtracting this term from $\int vX_i(v)f_i(v)dv$ proves the identity. <Interim individual rationality> bounds the lowest-type utilities below by zero.