proposition: Lemma han_helper (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 (fdist_perm P (put_front_perm i))) <= cond_entropy (fdistX (fdist_belast_last_of_rV (fdist_take P (lift ord0 i)))).
proof: Proof. rewrite (_ : fdistX _ = fdist_prod_of_rV (fdist_perm (fdist_take P (lift ord0 i)) (put_front_perm (inord i)))); last first. apply/fdist_ext => /= -[a v]. rewrite fdistXE fdist_belast_last_of_rVE fdist_prod_of_rVE /= fdist_permE. rewrite !(fdist_takeE _ (lift ord0 i)); apply eq_bigr => /= w _; congr (P _); apply/rowP => k. rewrite !castmxE /= cast_ord_id. case/boolP : (k < i.+1)%nat => ki. have @k1 : 'I_i.+1 := Ordinal ki. rewrite (_ : cast_ord _ k = lshift (n - bump 0 i) k1); last exact/val_inj. rewrite 2!row_mxEl castmxE /= cast_ord_id [in RHS]mxE. case/boolP : (k < i)%nat => [ki'|]. rewrite (_ : cast_ord _ _ = lshift 1%nat (Ordinal ki')) /=; last exact/val_inj. rewrite row_mxEl /put_front_perm permE /put_front ifF; last first. apply/negbTE/eqP => /(congr1 val) /=. by rewrite inordK // => /eqP; rewrite ltn_eqF. rewrite inordK //= ki' (_ : inord k.+1 = rshift 1%nat (Ordinal ki')); last first. by apply/val_inj => /=; rewrite inordK. by rewrite (@row_mxEr _ 1%nat 1%nat). rewrite permE /put_front. rewrite -leqNgt leq_eqVlt => /orP[|] ik. rewrite ifT; last first. apply/eqP/val_inj => /=; rewrite inordK //; exact/esym/eqP. rewrite row_mx_row_ord0 (_ : cast_ord _ _ = rshift i ord0); last first. by apply val_inj => /=; rewrite addn0; apply/esym/eqP. by rewrite row_mxEr mxE. move: (leq_ltn_trans ik ki); by rewrite ltnn. rewrite -ltnNge ltnS in ki. move=> [:Hk1]. have @k1 : 'I_(n - bump 0 i). apply: (@Ordinal _ (k - i.+1)). abstract: Hk1. by rewrite /bump leq0n add1n ltn_sub2r // (leq_ltn_trans _ (ltn_ord k)). rewrite (_ : cast_ord _ _ = rshift i.+1 k1); last by apply val_inj => /=; rewrite subnKC. by rewrite 2!row_mxEr. rewrite (_ : fdist_perm (fdist_take _ _) _ = fdist_take (fdist_perm P (put_front_perm i)) (lift ord0 i)); last first. apply/fdist_ext => /= w. rewrite fdist_permE 2!(fdist_takeE _ (lift ord0 i)); apply eq_bigr => /= v _. rewrite fdist_permE; congr (P _); apply/rowP => /= k. rewrite /col_perm mxE !castmxE /= !cast_ord_id /=. case/boolP : (k < bump 0 i)%nat => ki. rewrite (_ : cast_ord _ _ = lshift (n - bump 0 i) (Ordinal ki)); last exact/val_inj. rewrite row_mxEl mxE /put_front_perm !permE /= /put_front /=. case/boolP : (k == i) => ik. rewrite ifT; last first. apply/eqP/val_inj => /=; rewrite inordK //; exact/eqP. rewrite (_ : cast_ord _ _ = lshift (n - bump 0 i) ord0); last exact/val_inj. by rewrite row_mxEl. rewrite ifF; last first. apply/negbTE/eqP => /(congr1 val) /=. apply/eqP; by rewrite inordK. case/boolP : (k < i)%nat => {}ik. rewrite inordK // ik. move=> [:Hk1]. have @k1 : 'I_(bump 0 i). apply: (@Ordinal _ k.+1). abstract: Hk1. by rewrite /bump leq0n add1n. rewrite (_ : cast_ord _ _ = lshift (n - bump 0 i) k1); last first. apply/val_inj => /=; rewrite inordK // ltnS. by rewrite (leq_trans ik) // -ltnS. rewrite row_mxEl; congr (w _ _). by apply val_inj => /=; rewrite inordK. rewrite -ltnNge in ik. rewrite ifF; last first. apply/negbTE. by rewrite -leqNgt -ltnS inordK. rewrite (_ : cast_ord _ _ = lshift (n - bump 0 i) (Ordinal ki)); last exact/val_inj. by rewrite row_mxEl. rewrite -ltnNge /bump leq0n add1n ltnS in ki. move=> [:Hk1]. have @k1 : 'I_(n - bump 0 i). apply: (@Ordinal _ (k - i.+1)). abstract: Hk1. by rewrite /bump leq0n add1n ltn_sub2r // (leq_trans _ (ltn_ord k)). rewrite (_ : cast_ord _ _ = rshift i.+1 k1); last by apply/val_inj => /=; rewrite subnKC. rewrite row_mxEr permE /put_front /= ifF; last first. by move: ki; rewrite ltnNge; apply: contraNF => /eqP ->. rewrite ltnNge (ltnW ki) /=. move=> [:Hk2]. have @k2 : 'I_(n - bump 0 i). apply: (@Ordinal _ (k - i.+1)). abstract: Hk2. by rewrite /bump leq0n add1n ltn_sub2r // (leq_trans _ (ltn_ord k)). rewrite (_ : cast_ord _ _ = rshift (bump 0 i) k2); last first. by apply/val_inj => /=; rewrite /bump leq0n add1n subnKC. rewrite row_mxEr; congr (v _ _); exact/val_inj. exact/information_cant_hurt_cond. 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