proposition: Lemma typed_success_bound : scha(W, tc) <= n.+1%:R ^ (#|A| * #|B|) * exp_cdiv_bound Vmax.
proof: Proof. rewrite (typed_success W Mnot0 tc). apply (@leR_trans ( \sum_(V|V \in \nu^{B}(P)) exp_cdiv P V W * exp2 (- n%:R * +| log #|M|%:R * / n%:R - `I(P, V) |))). apply: leR_sumR => V Vnu. rewrite -mulRA; apply leR_wpmul2l. by rewrite /exp_cdiv; case : ifP. by rewrite /success_factor mulRA; exact: success_factor_ub. apply (@leR_trans (\sum_(V | V \in \nu^{B}(P)) exp_cdiv P Vmax W * exp2 (- n%:R * +| log #|M|%:R * / n%:R - `I(P, Vmax)|))). apply leR_sumR => V HV. by move/RleP: (@arg_rmax2 [finType of (P_ n (A, B))] V0 (fun V => exp_cdiv P V W * success_factor_bound M V P) V). rewrite big_const iter_addR /success_factor_bound; apply leR_wpmul2r. - apply mulR_ge0; last exact/exp2_ge0. by rewrite /exp_cdiv; case: ifP. - by rewrite natRexp; exact/le_INR/leP/card_nu. 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