proposition: Theorem channel_coding (r : CodeRateType) : r < capacity W -> forall epsilon, 0 < epsilon -> exists n M (c : code A B M n), CodeRate c = r /\ echa(W, c) < epsilon.
proof: Proof. move=> r_I epsilon Hepsilon. have [P HP] : exists P : {fdist A}, r < `I(P, W). apply NNPP => abs. have {}abs : forall P : {fdist A}, `I(P, W) <= r. move/not_ex_all_not in abs. move=> P; exact/Rnot_lt_le/abs. have ? : capacity W <= r. apply/RleP. have : has_sup [set `I(P, W) | P in [set: {fdist A}]]. case: set_of_I_nonempty => [x [P H1]]; split; first by exists x, P. by exists (rate r) => _ [Q _ <-]; exact/Rstruct.RleP/abs. move=> /(@Rsup_isLub 0 [set `I(P, W) | P in [set: {fdist A}]])[_]. apply. by move=> x [P _ <-{x}]; exact/RleP/abs. lra. have [epsilon0 Hepsilon0] : exists epsilon0, 0 < epsilon0 /\ epsilon0 < epsilon / 2 /\ epsilon0 < (`I(P, W) - r) / 4. exists ((Rmin (epsilon/2) ((`I(P, W) - r) / 4))/2). have H0 : 0 < Rmin (epsilon / 2) ((`I(P, W) - r) / 4). apply Rmin_pos; apply mulR_gt0 => //; lra. split; first by apply mulR_gt0 => //; lra. split; [exact/(ltR_leR_trans (Rlt_eps2_eps _ H0))/geR_minl | exact/(ltR_leR_trans (Rlt_eps2_eps _ H0))/geR_minr ]. have [n Hn] : exists n, n_condition W P r epsilon0 n. destruct r as [r [num [den [Hnum [Hden Hr]]]]]. have Hn : exists n, (0 < n)%nat /\ - log epsilon0 / epsilon0 < INR n /\ (maxn '| up (aep_bound P (epsilon0 / 3)) | (maxn '| up (aep_bound (`O(P , W)) (epsilon0 / 3)) | '| up (aep_bound ((P `X W)) (epsilon0 / 3)) |) <= n)%nat. set supermax := maxn 1 (maxn '| up (- log epsilon0 / epsilon0) | (maxn '| up (aep_bound P (epsilon0 / 3)) | (maxn '| up (aep_bound (`O(P , W)) (epsilon0 / 3)) | '| up (aep_bound ((P `X W)) (epsilon0 / 3)) |))). exists supermax. split; first by rewrite leq_max. split. apply (@ltR_leR_trans (IZR (up (- log epsilon0 / epsilon0)))). rewrite up_Int_part. case: (base_Int_part (- log epsilon0 / epsilon0)) => H1 H2. rewrite plus_IZR //. move: H2. set eps := - log epsilon0 / epsilon0. move=> ?; lra. apply (@leR_trans (INR '| up (- log epsilon0 / epsilon0) |)). case: (Z_lt_le_dec (up (- log epsilon0 / epsilon0)) 0) => H1. by apply (@leR_trans 0); [exact/IZR_le/ltZW | exact: leR0n]. rewrite INR_Zabs_nat //. by apply/RleP; rewrite Order.POrderTheory.lexx. apply le_INR. rewrite /supermax maxnA. apply/leP. by rewrite leq_max leq_max leqnn orbT. by rewrite [X in (_ <= X)%nat]maxnA leq_maxr. lapply (exists_frac_part Hn Hnum Hden); last move=> n1 n2 n1_n2 Pn1. case=> n [[Hn1 [Hn3 Hn4]] Hn2]. exists n => /=. rewrite /n_condition. split => //; split => //; split => //. by rewrite -Hr in Hn2. split. by apply/(@leq_trans n1) => //; tauto. split. by apply (@ltR_leR_trans (INR n1)); [tauto | exact/le_INR/leP]. by apply leq_trans with n1 => //; tauto. have He : (0 <= epsilon)%mcR. apply/RleP. by apply/ltRW. case: (random_coding_good_code He Hepsilon0 Hn) => M [HM [M_k H]]. move/RltP in H. case: (good_code_sufficient_condition HM H) => f Hf. exists n, M, (mkCode f (jtdec P W epsilon0 f)); split => //. rewrite /CodeRate M_k INR_Zabs_nat; last exact/Int_part_ge0. suff -> : IZR (Int_part (exp2 (INR n * r))) = exp2 (INR n * r). rewrite exp2K /Rdiv -mulRA mulRCA mulRV ?INR_eq0' -?lt0n ?mulR1 //; by case: Hn. by apply frac_Int_part; case: Hn => _ [_ []]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix perm) Reals Lra Classical mathcomp(Rstruct classical_sets) ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq joint_typ_seq channel channel_code