proposition: Lemma chain_rule_information : mutual_info PY = \sum_(i < n.+1) if i == O :> nat then mutual_info (fdist_prod_nth PY ord0) else cond_mutual_info (fAC i).
proof: Proof. rewrite mutual_infoE chain_rule_rV. have -> : cond_entropy PY = \sum_(j < n.+1) if j == O :> nat then cond_entropy (fdist_prod_nth PY ord0) else cond_entropy (fA j). have := chain_rule (fdistX PY). rewrite fdistXI addRC -subR_eq fdistX1 -/Y => <-. rewrite /joint_entropy. set YP : {fdist 'rV[A]_n.+2} := fdist_rV_of_prod (fdistX PY). transitivity (`H YP - `H Y); first by rewrite /YP entropy_fdist_rV_of_prod. rewrite (chain_rule_rV YP). rewrite [in LHS]big_ord_recl /=. rewrite (_ : `H (head_of_fdist_rV YP) = `H Y); last first. by rewrite /YP /head_of_fdist_rV (fdist_prod_of_rVK (fdistX PY)) fdistX1. rewrite addRC addRK. apply eq_bigr => j _. case: ifPn => j0. - have {}j0 : j = ord0 by move: j0 => /eqP j0; exact/val_inj. subst j. rewrite /cond_entropy /=. apply big_rV_1 => // a1. have H1 a : (fdistX (fdist_belast_last_of_rV (fdist_take YP (lift ord0 (lift ord0 ord0))))) (a, a1) = (fdist_prod_nth PY ord0) (a, a1 ``_ ord0). rewrite fdistXE fdist_belast_last_of_rVE. rewrite (fdist_takeE _ (lift ord0 (lift ord0 ord0))) fdist_prod_nthE /=. have H1 : (n.+2 - bump 0 (bump 0 0) = n)%nat. by rewrite /bump !leq0n !add1n subn2. rewrite (big_cast_rV H1). rewrite (eq_bigr (fun x => PY (x.1, x.2))); last by case. rewrite -(pair_big (fun i : 'rV_n.+1 => i ``_ ord0 == a) (fun i => i == a1 ``_ ord0) (fun i1 i2 => PY (i1, i2))) /=. rewrite [in RHS](eq_bigl (fun i : 'rV_n.+1 => (xpred1 a (i ``_ ord0)) && (xpredT i))); last first. move=> i; by rewrite andbT. rewrite -(big_rV_cons_behead (fun i => \sum_(j | j == a1 ``_ ord0) PY (i, j)) (fun i => i == a) xpredT). rewrite exchange_big /=. apply eq_bigr => v _. rewrite big_pred1_eq. rewrite big_pred1_eq. rewrite /YP. rewrite fdist_rV_of_prodE fdistXE /=; congr (PY (_, _)). apply/rowP => i. rewrite mxE castmxE /=. move: (leq0n i); rewrite leq_eqVlt => /orP[/eqP|] i0. move=> [:Hi1]. have @i1 : 'I_(bump 0 0).+1. apply: (@Ordinal _ i.+1); abstract: Hi1. by rewrite /bump leq0n add1n -i0. rewrite (_ : cast_ord _ _ = lshift (n.+2 - bump 0 (bump 0 0)) i1); last exact/val_inj. rewrite row_mxEl castmxE /= 2!cast_ord_id. rewrite (_ : cast_ord _ _ = rshift 1 (Ordinal (ltn_ord ord0))); last first. by apply val_inj => /=; rewrite add1n -i0. rewrite row_mxEr mxE. set i2 : 'I_1 := Ordinal (ltn_ord ord0). rewrite (_ : i = lshift n i2); last exact/val_inj. by rewrite (@row_mxEl _ _ 1) mxE. move=> [:Hi1]. have @i1 : 'I_(n.+2 - bump 0 (bump 0 0)). apply: (@Ordinal _ i.-1); abstract: Hi1. by rewrite /bump !leq0n !add1n subn2 prednK //= -ltnS. rewrite (_ : cast_ord _ _ = rshift (bump 0 0).+1 i1); last first. by apply/val_inj => /=; rewrite /bump !leq0n !add1n add2n prednK. rewrite row_mxEr castmxE /= !cast_ord_id. have @i2 : 'I_n by apply: (@Ordinal _ i.-1); rewrite prednK // -ltnS. rewrite (_ : i = rshift 1 i2); last first. by apply/val_inj => /=; rewrite add1n prednK. rewrite (@row_mxEr _ _ 1) //; congr (v _ _); exact/val_inj. rewrite castmxE /=. rewrite (_ : cast_ord _ _ = lshift (n.+2 - bump 0 (bump 0 0)) (Ordinal (ltn_ord ord0))); last exact/val_inj. rewrite row_mxEl castmxE /= 2!cast_ord_id. rewrite (_ : cast_ord _ _ = lshift 1 (Ordinal (ltn_ord ord0))); last exact/val_inj. rewrite row_mxEl /=; congr (a1 ``_ _); exact/val_inj. congr (_ * _). rewrite 2!fdist_sndE; apply eq_bigr => a _; by rewrite H1. rewrite /cond_entropy1; congr (- _). apply eq_bigr => a _; congr (_ * log _). + rewrite /jcPr /Pr !big_setX /= !big_set1. rewrite H1; congr (_ / _). rewrite !fdist_sndE; apply eq_bigr => a0 _. by rewrite H1. + rewrite /jcPr /Pr !big_setX /= !big_set1. rewrite H1; congr (_ / _). rewrite !fdist_sndE; apply eq_bigr => a0 _. by rewrite H1. - rewrite /fA /f. rewrite /cond_entropy /=. have H1 : bump 0 j = j.+1 by rewrite /bump leq0n. rewrite (big_cast_rV H1) /=. rewrite -(big_rV_cons_behead _ xpredT xpredT) /= exchange_big /= pair_bigA. have H2 (v : 'rV_j) (b : B) (a : A) (H1' : (1 + j)%nat = lift ord0 j) : (fdistX (fdist_belast_last_of_rV (fdist_take YP (lift ord0 (lift ord0 j))))) (a, (castmx (erefl 1%nat, H1') (row_mx (\row__ b) v))) = (fdistA (fdistC12 (fdist_prod_take PY j))) (a, (v, b)). rewrite /YP /fdistX /fdist_belast_last_of_rV /fdist_take /fdist_rV_of_prod. rewrite /fdistA /fdistC12 /fdist_prod_take !fdistmap_comp !fdistmapE /=. apply eq_bigl => -[w b0]; rewrite /= /swap /= !inE /=. rewrite (_ : rlast _ = w ``_ j); last first. rewrite /rlast !mxE !castmxE /= cast_ord_id. rewrite (_ : cast_ord _ _ = rshift 1%nat j); last exact/val_inj. by rewrite (@row_mxEr _ 1%nat 1%nat n.+1). rewrite !xpair_eqE; congr (_ && _). rewrite (_ : rbelast _ = row_take (lift ord0 j) (rbelast (row_mx (\row_(k<1) b0) w))); last first. apply/rowP => i; rewrite !mxE !castmxE /= esymK !cast_ord_id. by rewrite /rbelast mxE; congr (row_mx _ _ _ _); exact: val_inj. rewrite (_ : rbelast _ = row_mx (\row_(k<1) b0) (rbelast w)); last first. apply/rowP => i; rewrite mxE /rbelast. have [i0|i0] := eqVneq (i : nat) O. rewrite (_ : widen_ord _ _ = ord0); last exact: val_inj. rewrite (_ : i = ord0); last exact: val_inj. by rewrite 2!row_mx_row_ord0. have @k : 'I_n.+1. apply: (@Ordinal _ i.-1). by rewrite prednK // ?lt0n // -ltnS (leq_trans (ltn_ord i)). rewrite (_ : widen_ord _ _ = rshift 1%nat k); last first. by apply val_inj => /=; rewrite -subn1 subnKC // lt0n. rewrite (@row_mxEr _ 1%nat 1%nat n.+1). have @k' : 'I_n. apply: (@Ordinal _ i.-1). by rewrite prednK // ?lt0n // -ltnS (leq_trans (ltn_ord i)). rewrite (_ : i = rshift 1%nat k'); last first. by apply val_inj => /=; rewrite -subn1 subnKC // lt0n. rewrite (@row_mxEr _ 1%nat 1%nat n) mxE; congr (w ord0 _); exact: val_inj. apply/idP/idP; last first. move/andP => /= [/eqP <- /eqP ->]. apply/eqP/rowP => k. rewrite !mxE !castmxE /= esymK !cast_ord_id. case/boolP : (k == O :> nat) => [/eqP | ] k0. rewrite (_ : cast_ord _ _ = ord0); last exact: val_inj. rewrite (_ : k = ord0); last exact: val_inj. by rewrite 2!row_mx_row_ord0. have @l : 'I_n. apply: (@Ordinal _ k.-1). by rewrite prednK // ?lt0n // -ltnS (leq_trans (ltn_ord k)). rewrite (_ : cast_ord _ _ = rshift 1%nat l); last first. by apply val_inj => /=; rewrite add1n prednK // lt0n. rewrite (@row_mxEr _ 1%nat 1%nat n) //. have @l0 : 'I_(widen_ord (leqnSn n.+1) j). apply: (@Ordinal _ k.-1). by rewrite prednK // ?lt0n // -ltnS (leq_trans (ltn_ord k)). rewrite (_ : k = rshift 1%nat l0); last first. by apply val_inj => /=; rewrite add1n prednK // lt0n. rewrite (@row_mxEr _ 1%nat 1%nat) //. rewrite !mxE !castmxE /= cast_ord_id; congr (w _ _). exact: val_inj. move/eqP/rowP => H. move: (H ord0). rewrite !mxE !castmxE /= 2!cast_ord_id esymK. rewrite (_ : cast_ord _ _ = ord0); last exact: val_inj. rewrite 2!row_mx_row_ord0 => ->; rewrite eqxx andbT. apply/eqP/rowP => k. have @k1 : 'I_(bump 0 j). apply: (@Ordinal _ k.+1). by rewrite /bump leq0n add1n ltnS. move: (H k1). rewrite !mxE !castmxE /= esymK !cast_ord_id. have @k2 : 'I_n. apply: (@Ordinal _ k). by rewrite (leq_trans (ltn_ord k)) // -ltnS (leq_trans (ltn_ord j)). rewrite (_ : cast_ord _ _ = rshift 1%nat k2); last first. by apply val_inj => /=; rewrite add1n. rewrite (@row_mxEr _ 1%nat 1%nat) mxE. rewrite (_ : cast_ord _ _ = widen_ord (leqnSn n) k2); last exact: val_inj. move=> ->. rewrite (_ : k1 = rshift 1%nat k); last by apply val_inj => /=; rewrite add1n. by rewrite row_mxEr. apply eq_bigr => -[v b] _ /=. rewrite 2!fdist_sndE; congr (_ * _). apply eq_bigr => a _. rewrite -H2. congr (fdistX _ (a, castmx (_, _) _)). exact: eq_irrelevance. rewrite /cond_entropy1; congr (- _). apply eq_bigr => a _. rewrite /jcPr /Pr !big_setX /= !big_set1. rewrite !H2 //=. congr (_ / _ * log (_ / _)). + rewrite 2!fdist_sndE; apply eq_bigr => a' _; by rewrite H2. + rewrite 2!fdist_sndE; apply eq_bigr => a' _; by rewrite H2. rewrite -addR_opp big_morph_oppR -big_split /=; apply eq_bigr => j _ /=. case: ifPn => j0. - rewrite mutual_infoE addR_opp; congr (`H _ - _). rewrite /head_of_fdist_rV /fdist_fst /fdist_rV_of_prod. by rewrite /fdist_prod_nth !fdistmap_comp. - rewrite /cond_mutual_info /fA -/P; congr (_ - _). + congr cond_entropy. by rewrite /fAC /f fdist_proj13_AC fdistC12_fst belast_last_take. + rewrite /fAC /f /fdistAC fdistC12I /cond_entropy /=. rewrite (eq_bigr (fun a => (fdistA (fdistC12 (fdist_prod_take PY j)))`2 (a.1, a.2) * cond_entropy1 (fdistA (fdistC12 (fdist_prod_take PY j))) (a.1, a.2))); last by case. rewrite -(pair_bigA _ (fun a1 a2 => (fdistA (fdistC12 (fdist_prod_take PY j)))`2 (a1, a2) * cond_entropy1 (fdistA (fdistC12 (fdist_prod_take PY j))) (a1, a2))) /=. rewrite exchange_big pair_bigA /=; apply eq_bigr => -[b v] _ /=. congr (_ * _). * rewrite !fdist_sndE; apply eq_bigr=> a _. by rewrite !fdistAE /= fdistXE fdistC12E /= fdistAE. * rewrite /cond_entropy1; congr (- _); apply eq_bigr => a _. by rewrite -!setX1 -jcPr_fdistA_AC /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