proposition: Lemma mi_bound : PQR`1 = P `x Q -> mutual_info (fdist_proj13 PQR) + mutual_info (fdist_proj23 PQR) <= mutual_info PQR.
proof: Proof. move=> PQ; rewrite chain_rule_mutual_info leR_add2l /cond_mutual_info. rewrite [X in _ <= X - _](_ : _ = `H Q); last first. rewrite condentropy_indep; last first. rewrite fdist_proj13_fst fdistA1 fdistX1 fdistA21 -/Q. rewrite fdist_proj13_snd fdistX2 -/P. rewrite -[RHS]fdistXI fdistX_prod -PQ. apply/fdist_ext => -[b a]. rewrite fdist_proj13E fdistXE fdist_fstE; apply eq_bigr => c _. by rewrite fdistXE fdistAE. by rewrite /fdist_proj13 fdistA21 fdistC12_fst fdistX1 fdistX2 fdistA21 -/Q. rewrite mutual_infoE. rewrite fdist_proj23_fst -/Q. rewrite -oppRB leR_oppl oppRB -!addR_opp leR_add2r. rewrite -subR_ge0. move: (cond_mutual_info_ge0 (fdistC12 PQR)); rewrite /cond_mutual_info. rewrite /fdist_proj13 fdistC12I -/(fdist_proj23 _). by rewrite cond_entropy_fdistA /fdistAC fdistC12I. 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