Frequency_Moments and Expander_Graphs: Change the dependency between the entries.

The dependency of Expander_Graphs to Frequency_Moments was due to the use of some auxiliary
results (in particular those about HOL-Probability.Product_PMF).
This change moves those to Universal_Hash_Families, so that the dependency
can be avoided.

Note: I added aliases and abbreviations to minimize the risk of merge-conflicts.

This change will enable the introduction of further additional examples, that
show how Expander Graphs can be used to further improve the space complexity
of the verified algorithms in Frequency_Moments.