proposition: Lemma success_bound : let Pmax := [arg max_(P > P0) scha(W, P.-typed_code c)]%O in scha(W, c) <= n.+1%:R ^ #|A| * scha(W, Pmax.-typed_code c).
proof: Proof. move=> Pmax. apply (@leR_trans (#| P_ n ( A ) |%:R * scha W (Pmax.-typed_code c))); last first. apply leR_wpmul2r; first exact/RleP/scha_pos. rewrite natRexp; exact/le_INR/leP/(type_counting A n). apply (@leR_trans (\sum_(P : P_ n ( A )) scha W (P.-typed_code c))); last first. rewrite (_ : #| P_ n ( A ) |%:R * scha W (Pmax.-typed_code c) = \sum_(P : P_ n ( A )) scha W (Pmax.-typed_code c)); last first. by rewrite big_const iter_addR. apply leR_sumR => P _. by move/RleP : (arg_rmax2 P0 (fun P1 : P_ n (A) => scha(W, P1.-typed_code c)) P). rewrite schaE // -(sum_messages_types c). rewrite div1R (big_morph _ (morph_mulRDr _) (mulR0 _)). apply leR_sumR => P _. rewrite mulRC leR_pdivr_mulr; last exact/ltR0n. rewrite schaE // div1R -mulRA mulRCA mulVR ?INR_eq0' -?lt0n // mulR1. apply/(@leR_trans (\sum_(m | m \in enc_pre_img c P) \sum_(y | (dec (P.-typed_code c)) y == Some m) (W ``(|(enc (P.-typed_code c)) m)) y)). apply: leR_sumR => m Hm. apply/Req_le/eq_big => tb // _. rewrite inE in Hm. by rewrite /tcode /= ffunE Hm. - apply leR_sumRl => //= i ?; [| exact/RleP/sumr_ge0]. by apply/RleP; rewrite lexx. 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