proposition: Lemma markov_cond_mutual_info : markov_chain -> cond_mutual_info (PRQ : {fdist A * C * B}) = 0.
proof: Proof. rewrite /markov_chain => mc. rewrite cond_mutual_infoE (eq_bigr (fun=> 0)) ?big_const ?iter_addR ?mulR0 //= => x _. case/boolP : (PRQ x == 0) => [/eqP ->|H0]; first by rewrite mul0R. rewrite (_ : _ / _ = 1); first by rewrite /log Log_1 mulR0. rewrite eqR_divr_mulr ?mul1R; last first. rewrite mulR_neq0'; apply/andP; split. rewrite /jcPr divR_neq0' //. rewrite setX1 Pr_set1. case: x => [[x11 x12] x2] in H0 *. exact: fdist_proj13_dominN H0. rewrite Pr_set1 fdist_proj13_snd. case: x => [x1 x2] in H0 *. exact: dom_by_fdist_sndN H0. rewrite /jcPr divR_neq0' //. rewrite setX1 Pr_set1. case: x => [[x11 x12] x2] in H0 *. exact: fdist_proj23_dominN H0. rewrite Pr_set1 fdist_proj23_snd. case: x => [x1 x2] in H0 *. exact: dom_by_fdist_sndN H0. transitivity (Pr PRQ [set x] / Pr Q [set x.2]). rewrite /jcPr setX1 {2}/PRQ fdistAC2 -/Q; by case: x H0. transitivity (Pr PQ [set (x.1.1,x.2)] * \Pr_RQ[[set x.1.2]|[set x.2]] / Pr Q [set x.2]). congr (_ / _). case: x H0 => [[a c] b] H0 /=. rewrite /PRQ Pr_set1 fdistACE /= mc; congr (_ * _). rewrite /jcPr {2}/QP fdistX2 -/P Pr_set1 mulRCA mulRV ?mulR1; last first. apply dom_by_fdist_fstN with b. apply dom_by_fdist_fstN with c. by rewrite fdistACE in H0. by rewrite /QP Pr_fdistX setX1. rewrite {1}/Rdiv -mulRA mulRCA mulRC; congr (_ * _). rewrite /jcPr fdist_proj13_snd -/Q {2}/PRQ fdistAC2 -/Q -/(Rdiv _ _); congr (_ / _). by rewrite /PRQ /PQ setX1 fdist_proj13_AC. rewrite /jcPr fdist_proj23_snd; congr (_ / _). - by rewrite /RQ /PRQ /fdist_proj23 fdistA_AC_snd. - by rewrite /RQ fdistX2 fdistA21 /PRQ fdistAC2. 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