All these properties should be evident from the construction.
\defn{The redundancy of a mixer is $$r(f) :=\underbrace{M +\log S}_{\hbox{output entropy}}-\quad\underbrace{(\log X +\log Y)}_{\hbox{input entropy}}.$$}
\defn{The redundancy of a mixer is $$r(f) :=\underbrace{M +\log S}_{\hbox{output entropy}}-\quad\underbrace{(\log X +\log Y)}_{\hbox{input entropy}}.$$
In general, the redundancy of a mapping (with possibly multiple inputs and multiple outputs) is the sum of the logs of the
output alphabet size, minus the sum of the logs of the input alphabet sizes. Note that there is no rounding (because the inputs and
outputs can be from arbitrary alphabets, not necessarily binary) and the redundancy can be non-integer. Compare this to the concept
of redundancy for space-efficient datastructures defined above.}
\subsection{On the existence of certain kinds of mixers}