proposition: Lemma channel_coding_converse_gen : exists Delta, 0 < Delta /\ forall n', let n := n'.+1 in forall (M : finType) (c : code A B M n), (0 < #|M|)%nat -> minRate <= CodeRate c -> scha(W, c) <= n.+1%:R ^ (#|A| + #|A| * #|B|) * exp2 (- n%:R * Delta).
proof: Proof. move: error_exponent_bound => /(_ _ _ Bnot0 W _ HminRate set_of_I_has_ubound). case => Delta [Delta_pos HDelta]. exists Delta; split => // n' n M c Mnot0 H. apply: (leR_trans (success_bound W Mnot0 c)). set Pmax := [arg max_(P > _) _]%O. set tc := _.-typed_code _. rewrite pow_add -mulRA. apply leR_wpmul2l; first exact/pow_le/leR0n. apply: (leR_trans (typed_success_bound W Mnot0 (Pmax.-typed_code c))). apply leR_wpmul2l; first exact/pow_le/leR0n. set Vmax := [arg max_(V > _) _]%O. rewrite /success_factor_bound /exp_cdiv. case : ifP => Hcase; last by rewrite mul0R. rewrite -ExpD. apply Exp_le_increasing => //. rewrite -mulRDr 2!mulNR. rewrite leR_oppr oppRK; apply/leR_wpmul2l; first exact/leR0n. have {}Hcase : Pmax |- Vmax << W. move=> a Hp; apply/dominatesP => b /eqP Hw. move/forallP : Hcase. by move/(_ a)/implyP/(_ Hp)/forallP/(_ b)/implyP/(_ Hw)/eqP. apply (leR_trans (HDelta Pmax Vmax Hcase)) => /=. exact/leR_add2l/Rle_max_compat_l/leR_add2r. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext logb ln_facts num_occ fdist entropy types jtypes divergence conditional_divergence error_exponent channel_code channel success_decode_bound