When comparing random-variable sequences generated from probability distributions, what's a formal proof that a distribution with higher entropy produces a sequence that's "harder" to compress?
In background reading, I haven't come across this analysis for a general, abstract probability distribution. The information theory texts I've looked at, rather, tend to focus their analysis on comparing compression algorithms rather than comparing the distributions producing the data.