proposition: Lemma shannon_fano_average_entropy : is_shannon_fano P f -> average P f < `H P + 1.
proof: Proof. move=> H; rewrite /average. apply (@ltR_leR_trans (\sum_(x in A) P x * (- Log #|T|%:R (P x) + 1))). apply: ltR_sumR. apply: fdist_card_neq0. exact: P. move=> i. apply ltR_pmul2l; first by apply/RltP; rewrite lt0r Pr_pos /=. rewrite H. rewrite (_ : #|T|%:R = 2) // ?card_ord // -!/(log _). set x := log _; case: (ceilP x) => _ Hx. have Pi0 : 0 < P i by apply/RltP; rewrite lt0r Pr_pos /=. rewrite INR_Zabs_nat; last first. apply/leR0ceil. rewrite /x div1R /log LogV //. apply oppR_ge0. by rewrite -(Log_1 2); apply Log_increasing_le. case: (ceilP x) => _. by rewrite -LogV // -/(log _) -(div1R _) /x. under eq_bigr do rewrite mulRDr mulR1 mulRN. rewrite big_split /= FDist.f1 leR_add2r. apply Req_le. rewrite /entropy big_morph_oppR; apply eq_bigr => i _. by rewrite card_ord (_ : 2%:R = 2). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrZ ssrR logb Reals_ext realType_ext ssr_ext fdist entropy kraft