proposition: Lemma shannon_fano_is_kraft : is_shannon_fano P f -> kraft_condR T sizes.
proof: Proof. move=> H. rewrite /kraft_condR. rewrite (_ : 1 = 1%mcR)//. rewrite -(FDist.f1 P) /sizes size_map. rewrite (eq_bigr (fun i:'I_(size(enum A)) => #|'I_t|%:R ^- size (f (nth a (enum A) i)))); last first. move=> i _; by rewrite /= (nth_map a). rewrite -(big_mkord xpredT (fun i => #|T|%:R ^- size (f (nth a (enum A) i)))). rewrite -(big_nth a xpredT (fun i => #|'I_t|%:R ^- size (f i))). rewrite enumT. apply leR_sumR => i _. rewrite H. have Pi0 : 0 < P i by apply/RltP; rewrite lt0r Pr0/=. apply (@leR_trans (Exp #|T|%:R (- Log #|T|%:R (1 / P i)))); last first. rewrite div1R LogV// oppRK LogK //; first by apply/RleP; rewrite lexx. by rewrite (_ : 1 = 1%:R) // ltR_nat card_ord. rewrite pow_Exp; last by apply ltR0n; rewrite card_ord. rewrite Exp_Ropp. apply/leR_inv/Exp_le_increasing => //. by rewrite (_ : 1 = 1%:R) // ltR_nat card_ord. rewrite INR_Zabs_nat; last first. case/boolP : (P i == 1) => [/eqP ->|Pj1]. by rewrite divR1 Log_1 /ceil fp_R0 eqxx /=; apply/Int_part_ge0. apply/leR0ceil/ltRW/ltR0Log. by rewrite (_ : 1 = 1%:R) // ltR_nat card_ord. rewrite div1R invR_gt1 // ltR_neqAle; split => //; exact/eqP. by set x := Log _ _; case: (ceilP x). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrZ ssrR logb Reals_ext realType_ext ssr_ext fdist entropy kraft