proposition: Lemma chain_rule_relative_entropy : Pj `<< Qj -> D(Pj || Qj) = D(P1 || Q1) + cond_relative_entropy P Q.
proof: Proof. move=> PQ. rewrite {2}/div /cond_relative_entropy -big_split /= {1}/div /=. rewrite (eq_bigr (fun a => Pj (a.1, a.2) * (log (Pj (a.1, a.2) / (Qj (a.1, a.2)))))); last by case. rewrite -(pair_bigA _ (fun a1 a2 => Pj (a1, a2) * (log (Pj (a1, a2) / (Qj (a1, a2)))))) /=. rewrite exchange_big; apply eq_bigr => a _ /=. rewrite [in X in _ = X * _ + _](_ : P1 a = Pj`2 a); last first. by rewrite /P fdistX2 fdist_prod1. rewrite fdist_sndE big_distrl /= big_distrr /= -big_split /=; apply eq_bigr => b _. rewrite mulRA (_ : P1 a * _ = Pj (b, a)); last first. rewrite /jcPr Pr_set1 -/P1 mulRCA setX1 Pr_set1 {1}/Pj fdistX2 fdist_prod1. have [P2a0|P2a0] := eqVneq (P1 a) 0. have Pba0 : Pj (b, a) = 0. by rewrite /P fdistXE fdist_prodE P2a0 -RmultE mul0R. by rewrite Pba0 mul0R. by rewrite mulRV // ?mulR1. rewrite -mulRDr. have [->|H0] := eqVneq (Pj (b, a)) 0; first by rewrite !mul0R. congr (_ * _). have P1a0 : P1 a != 0. apply: contra H0 => /eqP. by rewrite /P fdistXE fdist_prodE => ->; rewrite -RmultE mul0R. have Qba0 := dominatesEN PQ H0. have Q2a0 : Q1 a != 0. apply: contra Qba0; rewrite /Q fdistXE fdist_prodE => /eqP ->; by rewrite -RmultE mul0R. rewrite -logM; last 2 first. by apply/divR_gt0; apply/RltP; rewrite -fdist_gt0. by apply/divR_gt0; by rewrite -Pr_jcPr_gt0 setX1 Pr_set1; apply/RltP; rewrite -fdist_gt0. congr (log _). rewrite /jcPr !setX1 !Pr_set1. rewrite !fdistXE !fdistX2 !fdist_prod1 !fdist_prodE /=. rewrite -/P1 -/Q1; field. split; first exact/eqP. split; first exact/eqP. apply/eqP. by apply: contra Qba0; rewrite /Qj fdistXE fdist_prodE /= => /eqP ->. 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