Invariance of an information slot under a re-encoding of one of its variables #

An information slot depends on the variable filling it only through the information that variable carries, so replacing the variable by its image under a map that has a left inverse leaves the slot unchanged: the data processing inequality bounds the slot in one direction along the map and in the other along the left inverse. The same holds for a variable replaced by one equal to it almost everywhere, since the two induce the same joint law. For a re-encoding of the conditioning variable the chain rule turns the statement about a pair back into one about the conditional mutual information.

None of the statements mentions a channel or a code: they are properties of mutualInfo and condMutualInfo under a substitution of one of their variables.

Main statements #

• mutualInfo_eq_of_leftInverse — re-encoding a variable by a map that has a left inverse leaves the mutual information it carries about another variable unchanged.
• mutualInfo_congr_ae — two variables that agree almost everywhere carry the same mutual information about a third.
• condMutualInfo_eq_of_leftInverse_cond — the same re-encoding applied to the conditioning variable of a conditional mutual information, obtained from the chain rule by cancelling the tag term on both sides.

Implementation notes #

A variable relabeled by a MeasurableEquiv is the special case g := e.symm, so mutualInfo_map_left_measurableEquiv is an instance of mutualInfo_eq_of_leftInverse; it is stated separately because it is proved directly from klDiv_map_measurableEquiv, without the data processing inequality. Its conditioner analogue condMutualInfo_map_cond_measurableEquiv is not subsumed the same way: cancelling the conditioning variable's own term of the chain rule, which is how condMutualInfo_eq_of_leftInverse_cond is proved, needs that term to be finite, whereas a relabel needs no side condition at all.