proposition: Lemma information_cant_hurt_cond (A : finType) (n' : nat) (n := n'.+1 : nat) (P : {fdist 'rV[A]_n}) (i : 'I_n) (i0 : i != O :> nat) : cond_entropy (fdist_prod_of_rV P) <= cond_entropy (fdist_prod_of_rV (fdist_take P (lift ord0 i))).
proof: Proof. apply/RleP. rewrite -subR_ge0. set Q : {fdist A * 'rV[A]_i * 'rV[A]_(n' - i)} := fdist_take_drop P i. have H1 : fdist_proj13 (fdistAC Q) = fdist_prod_of_rV (fdist_take P (lift ord0 i)). rewrite /fdist_proj13 /fdistAC /fdist_prod_of_rV /fdist_take /fdist_snd /fdistA. rewrite /fdistC12 /fdistX /fdist_take_drop !fdistmap_comp; congr (fdistmap _ P). rewrite boolp.funeqE => /= v /=. congr (_, _). - rewrite mxE castmxE /= cast_ord_id; congr (v ord0 _); exact: val_inj. - apply/rowP => j. rewrite !mxE !castmxE /= !cast_ord_id !esymK mxE; congr (v ord0 _). exact: val_inj. have H2 : cond_entropy (fdistA (fdistAC Q)) = cond_entropy (fdist_prod_of_rV P). rewrite -cond_entropy_fdistA /cond_entropy /=. rewrite (partition_big (@row_take A _ i) xpredT) //=. rewrite (eq_bigr (fun a => (fdistA Q)`2 (a.1, a.2) * cond_entropy1 (fdistA Q) (a.1, a.2))%R); last by case. rewrite -(pair_bigA _ (fun a1 a2 => (fdistA Q)`2 (a1, a2) * cond_entropy1 (fdistA Q) (a1, a2))%R) /=. apply eq_bigr => v _. rewrite (@reindex_onto _ _ _ [finType of 'rV[A]_n'] [finType of 'rV[A]_(n' - i)] (fun w => (castmx (erefl 1%nat, subnKC (ltnS' (ltn_ord i))) (row_mx v w))) (@row_drop A _ i)) /=; last first. move=> w wv; apply/rowP => j. rewrite castmxE /= cast_ord_id /row_drop mxE; case: splitP => [j0 /= jj0|k /= jik]. - rewrite -(eqP wv) mxE castmxE /= cast_ord_id; congr (w _ _); exact: val_inj. - rewrite mxE /= castmxE /= cast_ord_id; congr (w _ _); exact: val_inj. apply eq_big => /= w. apply/esym/andP; split; apply/eqP/rowP => j. by rewrite !mxE !castmxE /= !cast_ord_id esymK cast_ordK row_mxEl. by rewrite !mxE !castmxE /= cast_ord_id esymK cast_ordK cast_ord_id row_mxEr. move=> _; congr (_ * _)%R. - rewrite !fdist_sndE; apply eq_bigr => a _. by rewrite fdistAE /= fdist_prod_of_rVE /= /Q fdist_take_dropE. - rewrite /cond_entropy1; congr (- _)%R; apply eq_bigr => a _. congr (_ * log _)%R. + rewrite /jcPr !(Pr_set1,setX1) fdistAE /= /Q fdist_take_dropE /= fdist_prod_of_rVE /=. congr (_ / _)%R. rewrite !fdist_sndE; apply eq_bigr => a0 _. by rewrite fdistAE fdist_take_dropE fdist_prod_of_rVE. + rewrite /jcPr !(Pr_set1,setX1) fdistAE /= /Q fdist_take_dropE /= fdist_prod_of_rVE /=. congr (_ / _)%R. rewrite !fdist_sndE; apply eq_bigr => a0 _. by rewrite fdistAE fdist_take_dropE fdist_prod_of_rVE. rewrite (_ : _ - _ = cond_mutual_info (fdistAC Q))%R; last by rewrite /cond_mutual_info H1 H2. exact/cond_mutual_info_ge0. 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