proposition: Lemma success_factor_ub : success_factor tc V <= success_factor_bound.
proof: Proof. rewrite /success_factor_bound. apply Rmax_case. - rewrite mulR0 exp2_0; by apply success_factor_bound_part1. - apply (@leR_trans (exp2 (n%:R * `I(P, V)) / #|M|%:R)); last first. + apply/Req_le/esym. rewrite mulRDr mulRC. rewrite Rmult_opp_opp -mulRA mulRN mulVR ?INR_eq0' //. rewrite mulRN mulR1 /exp2 ExpD mulRC /Rdiv; f_equal. rewrite Exp_Ropp LogK //; exact/ltR0n. + exact/success_factor_bound_part2. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext logb fdist entropy ln_facts num_occ types jtypes divergence conditional_divergence entropy channel_code channel