proposition: Lemma success_factor_bound_part2 : success_factor tc V <= exp2(n%:R * `I(P, V)) / #|M|%:R.
proof: Proof. rewrite /success_factor -mulRA (mulRC (/ #|M|%:R)) !mulRA. apply leR_wpmul2r; first exact/invR_ge0/ltR0n. rewrite /mutual_info_chan -addR_opp addRC addRA. rewrite (_ : - `H(type.d P , V) + `H P = - `H( V | P )); last first. rewrite /cond_entropy_chan. by rewrite oppRD oppRK. rewrite mulRDr mulRN -mulNR /exp2 ExpD; apply leR_wpmul2l => //. rewrite -big_morph_natRD; apply (@leR_trans #| T_{`tO( V )} |%:R); last first. by rewrite -output_type_out_entropy //; exact: card_typed_tuples. apply/le_INR/leP. apply: (@leq_trans (\sum_m #| T_{`tO( V )} :&: (@tuple_of_row B n @: (dec tc @^-1: [set Some m]))|)). - apply leq_sum => m _. by apply subset_leq_card, setSI, shell_subset_output_type. - set lhs := (\sum__ _)%nat. rewrite (_ : lhs = #|\bigcup_(i : M) (T_{`tO( V )} :&: (@tuple_of_row B n @: (dec tc @^-1: [set Some i]))) | ); last first. subst lhs. rewrite -cover_pre_image. move: trivIset_pre_image ; rewrite /trivIset => /eqP => <-. rewrite big_imset /= ; last first. move=> m l _. rewrite in_set; case/existsP => tb Htb. move/setP/(_ tb); rewrite Htb; move: Htb. rewrite in_set => /andP [_ Hl]. rewrite in_set => /andP [_ Hm]. suff : Some m = Some l by case. move: Hl Hm. case/imsetP => v1 Hv1 ->. case/imsetP => v2 Hv2. move/tuple_of_row_inj => ?; subst v2. rewrite !inE in Hv1, Hv2. by rewrite -(eqP Hv1) -(eqP Hv2). symmetry; rewrite big_mkcond /=. apply eq_bigr => m _. case : ifP => //; rewrite in_set => /negbT H. symmetry; apply/eqP/negPn/negP => abs ; move: H. apply/negP/negPn/existsP/card_gt0P; by rewrite lt0n. apply subset_leq_card; apply/subsetP => tb. case/bigcupP => m _. by rewrite in_set => /andP [H _]. 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