Entropy lower bound for prefix codes

Every binary prefix code has expected length at least its source entropy; Shannon lengths achieve expected length strictly below $H+1$.