proposition: Lemma mut_info_dist_ub : `| `I(P, V) - `I(P, W) | <= / ln 2 * (#|B|%:R + #|A|%:R * #|B|%:R) * - xlnx (sqrt (2 * D(V || W | P))).
proof: Proof. rewrite /mutual_info_chan. rewrite (_ : _ - _ = `H(P `o V) - `H(P `o W) + (`H(P, W) - `H(P, V))); last by field. apply: leR_trans; first exact: Rabs_triang. rewrite -mulRA mulRDl mulRDr. apply leR_add. - by rewrite mulRA; apply out_entropy_dist_ub. - by rewrite distRC 2!mulRA; apply joint_entropy_dist_ub. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals Lra mathcomp(Rstruct reals) ssrR realType_ext Reals_ext Ranalysis_ext logb ln_facts fdist entropy channel_code channel divergence conditional_divergence variation_dist pinsker