proposition: Theorem channel_coding_converse : exists n0, forall n M (c : code A B M n), (0 < #|M|)%nat -> n0 < n%:R -> minRate <= CodeRate c -> scha(W, c) < epsilon.
proof: Proof. case: (channel_coding_converse_gen minRate_cap set_of_I_has_ubound) => Delta [Delta_pos HDelta]. pose K := (#|A| + #|A| * #|B|)%nat. pose n0 := 2 ^ K * K.+1`!%:R / ((Delta * ln 2) ^ K.+1) / epsilon. exists n0 => n M c HM n0_n HminRate. have Rlt0n : 0 < n%:R. apply: (ltR_trans _ n0_n). rewrite /n0. apply mulR_gt0; last exact/invR_gt0. rewrite /Rdiv -mulRA. apply mulR_gt0; first exact/expR_gt0/Rlt_0_2. apply mulR_gt0; [exact/ltR0n/fact_gt0 | exact/invR_gt0/expR_gt0/mulR_gt0]. destruct n as [|n']. by apply ltRR in Rlt0n. set n := n'.+1. apply: (@leR_ltR_trans (n.+1%:R ^ K * exp2 (- n%:R * Delta))). exact: HDelta. move: (n0_n) => /(@ltR_pmul2l (/ n%:R) _) => /(_ (invR_gt0 n%:R Rlt0n)). rewrite mulVR ?INR_eq0' //. move/(@ltR_pmul2l epsilon) => /(_ eps_gt0); rewrite mulR1 => H1'. apply: (leR_ltR_trans _ H1') => {H1'}. rewrite /n0 [in X in _ <= X]mulRC -2![in X in _ <= X]mulRA. rewrite mulVR ?mulR1 ?gtR_eqF //. apply Rge_le; rewrite mulRC -2!mulRA; apply Rle_ge. set aux := _%:R * (_ * _). have aux_gt0 : 0 < aux. apply mulR_gt0; first exact/ltR0n/fact_gt0. apply mulR_gt0; [exact/invR_gt0/expR_gt0/mulR_gt0 | exact/invR_gt0]. apply (@leR_trans ((n.+1%:R / n%:R) ^ K * aux)); last first. apply leR_pmul => //. - apply/expR_ge0/divR_ge0 => //; exact: leR0n. - exact: ltRW. - apply pow_incr; split. + apply divR_ge0 => //; exact: leR0n. + apply (@leR_pmul2r n%:R) => //. rewrite -mulRA mulVR // ?mulR1 ?INR_eq0' ?gtn_eqF // (_ : 2 = 2%:R) //. rewrite -natRM; apply/le_INR/leP; by rewrite -{1}(mul1n n) ltn_pmul2r. - by apply/RleP; rewrite Order.POrderTheory.lexx. rewrite expRM -mulRA; apply leR_pmul => //. - exact/expR_ge0/ltRW/ltR0n. - by apply/RleP; rewrite Order.POrderTheory.lexx. - apply invR_le => //. + apply mulR_gt0; last exact aux_gt0. rewrite expRV ?INR_eq0' //; exact/invR_gt0/expR_gt0. + rewrite -exp2_Ropp mulNR oppRK /exp2. have nDeltaln2 : 0 <= n%:R * Delta * ln 2. apply mulR_ge0; last exact/ltRW. apply mulR_ge0; [exact/leR0n | exact/ltRW]. apply: (leR_trans _ (exp_lb (K.+1) nDeltaln2)) => {nDeltaln2}. apply Req_le. rewrite invRM; last 2 first. exact/gtR_eqF/expR_gt0/invR_gt0. exact/gtR_eqF. rewrite -/(Rdiv _ _) divRM; last 2 first. by rewrite INR_eq0' gtn_eqF // fact_gt0. rewrite gtR_eqF //; apply/mulR_gt0; last exact/invR_gt0. exact/invR_gt0/expR_gt0/mulR_gt0. rewrite -mulRA mulRC invRM; last 2 first. - by apply/eqP/invR_neq0/eqP; rewrite expR_eq0 mulR_neq0' ln2_neq0 andbT; exact/gtR_eqF. - by apply/eqP/invR_neq0/eqP; by rewrite INR_eq0'. - rewrite 2!invRK (_ : / (/ n%:R) ^ K = n%:R ^ K); last first. rewrite expRV ?INR_eq0' // invRK //; apply/expR_neq0; by rewrite INR_eq0'. rewrite -mulRA {1}/Rdiv (mulRA n%:R) -expRS mulRA -expRM. by rewrite -/(Rdiv _ _) mulRCA -mulRA (mulRC (ln 2)). 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