proposition: Lemma data_processing_inequality : markov_chain -> mutual_info PR <= mutual_info PQ.
proof: Proof. move=> H. have H1 : mutual_info (fdistA PQR) = mutual_info PR + cond_mutual_info PQR. rewrite /cond_mutual_info !mutual_infoE addRA; congr (_ - _). by rewrite -/PR subRK /PR fdist_proj13_fst. have H2 : mutual_info (fdistA PQR) = mutual_info PQ + cond_mutual_info PRQ. transitivity (mutual_info (fdistA PRQ)). by rewrite !mutual_infoE fdistA_AC_fst cond_entropy_fdistA. rewrite /cond_mutual_info !mutual_infoE addRA; congr (_ - _). by rewrite fdistA1 {1}/PRQ fdist_proj13_AC -/PQ subRK /PQ fdistAC_fst_fst. have H3 : cond_mutual_info PRQ = 0 by rewrite markov_cond_mutual_info. have H4 : 0 <= cond_mutual_info PQR by exact: cond_mutual_info_ge0. move: H2; rewrite {}H3 addR0 => <-. by rewrite {}H1 addRC -leR_subl_addr subRR. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence