Proof high-entropy sequences are hard to compress 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.
You are looking for Shannon's source coding theorem.