proposition: Lemma random_coding_good_code epsilon : 0 <= epsilon -> forall (r : CodeRateType), forall epsilon0, epsilon0_condition r epsilon epsilon0 -> forall n, n_condition r epsilon0 n -> exists M : finType, (0 < #|M|)%nat /\ #|M| = '| Int_part (exp2 (INR n * r)) | /\ let Jtdec := jtdec P W epsilon0 in \sum_(f : encT A M n) (Wght.d P f * echa(W , mkCode f (Jtdec f)))%R < epsilon.
proof: Proof. move=> Hepsilon r epsilon0 Hepsilon0 n Hn. have [k Hk] : exists k, (log (INR k.+1) / INR n = r)%R. case: Hn => ? [? [Hn2 ?]]. case/fp_nat : Hn2 => k Hn2. exists '| k |.-1. rewrite prednK; last first. apply/ltP/INR_lt. rewrite INR_Zabs_nat; [by rewrite -Hn2 | apply le_IZR; by rewrite -Hn2]. rewrite -(@eqR_mul2l (INR n)); last by rewrite INR_eq0; apply/eqP; rewrite -lt0n. rewrite mulRCA mulRV ?INR_eq0' -?lt0n // mulR1 -(exp2K (INR n * r)) Hn2 INR_Zabs_nat //. apply le_IZR; by rewrite -Hn2. set M := [finType of 'I_k.+1]. exists [finType of 'I_k.+1]. split; first by rewrite /= card_ord. split. have -> : (INR n * r)%R = log (INR k.+1). rewrite -Hk mulRCA mulRV ?INR_eq0' -?lt0n ?mulR1 //; by case: Hn. rewrite logK; last exact/ltR0n. by rewrite Int_part_INR Zabs_nat_Z_of_nat card_ord. move=> Jtdec. rewrite /CodeErrRate. rewrite [X in X < _](_ : _ = (1 / INR #|M| * \sum_(f : encT A M n) Wght.d P f * (\sum_(m in M) e(W, mkCode f (Jtdec f)) m))%R); last first. rewrite big_distrr /=. apply eq_bigr => f _. rewrite -!mulRA mulRC -!mulRA. do 2 f_equal. by rewrite mulRC. rewrite [X in X < _](_ : _ = (\sum_(f : encT A M n) Wght.d P f * (e(W, mkCode f (Jtdec f))) ord0)%R); last first. transitivity (1 / INR #|M| * \sum_(f : encT A M n) (\sum_(m in M) Wght.d P f * (e(W, mkCode f (Jtdec f))) m))%R. f_equal. apply eq_bigr => i _; by rewrite big_distrr. rewrite exchange_big /=. transitivity (1 / INR #|M| * \sum_(f : encT A M n) (\sum_( m_ in M ) Wght.d P f * (e(W, mkCode f (Jtdec f))) ord0))%R. congr (_ * _)%R. rewrite [in RHS]exchange_big /=. apply eq_bigr => m' _. apply error_rate_symmetry. by move: Hepsilon0; rewrite /epsilon0_condition; case => /ltRW. rewrite exchange_big /= big_const /= iter_addR div1R mulRA mulVR ?mul1R //. by rewrite INR_eq0' card_ord. set Cal_E := @cal_E M n epsilon0. apply/RltP. apply (@leR_ltR_trans (\sum_(f : encT A M n) Wght.d P f * Pr (W ``(| f ord0)) (~: Cal_E f ord0) + \sum_(i | i != ord0) \sum_(f : encT A M n) Wght.d P f * Pr (W ``(| f ord0)) (Cal_E f i))%R). rewrite exchange_big /= -big_split /=. apply leR_sumR => /= i _. rewrite -big_distrr /= -mulRDr. apply leR_wpmul2l; first exact/RleP/FDist.ge0. rewrite [X in (X <= _)%coqR](_ : _ = Pr (W ``(| i ord0)) (~: Cal_E i ord0 :|: \bigcup_(i0 : M | i0 != ord0) Cal_E i i0)); last first. congr Pr; apply/setP => /= tb. move: (preimC_Cal_E epsilon0 i tb); by rewrite inE. apply (@leR_trans (Pr (W ``(| i ord0)) (~: Cal_E i ord0) + Pr (W ``(| i ord0)) (\bigcup_(i0 | i0 != ord0) (Cal_E i i0)))%R). exact: Pr_union. exact/leR_add2l/Pr_bigcup. rewrite first_summand //. set lhs := (\sum_(_ < _ | _) _)%R. have -> : lhs = (#| M |.-1%:R * Pr ((P `^ n) `x ((`O(P , W)) `^ n)) [set x | prod_rV x \in `JTS P W n epsilon0])%R. rewrite {}/lhs. rewrite [RHS](_ : _ = \sum_(H0 < k.+1 | H0 != ord0) Pr ((P `^ n) `x ((`O( P , W )) `^ n)) [set x | prod_rV x \in `JTS P W n epsilon0])%R; last first. rewrite big_const /= iter_addR; congr (_%:R * _)%R. rewrite card_ord /=. transitivity (#| finset.setT :\ (@ord0 k)|). move: (cardsD1 (@ord0 k) finset.setT) => /=. rewrite !cardsT !card_ord inE /= add1n. case=> H1; by rewrite {1}H1. rewrite cardsE. apply eq_card => m_. by rewrite -!topredE /= !finset.in_set andbC. by apply eq_big => //; exact: second_summand. rewrite card_ord /=. apply (@leR_ltR_trans (epsilon0 + k%:R * Pr P `^ n `x (`O(P , W)) `^ n [set x | prod_rV x \in `JTS P W n epsilon0])%R). apply leR_add2r. rewrite Pr_of_cplt leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //. by case: Hepsilon0. by case: Hn => _ [_ []]. apply (@leR_ltR_trans (epsilon0 + #| M |%:R * exp2 (- n%:R * (`I(P, W ) - 3 * epsilon0)))). apply/leR_add2l/leR_pmul; [exact: leR0n|exact: Pr_ge0| |exact: non_typical_sequences]. by apply/le_INR/leP; rewrite card_ord. apply (@ltR_trans (epsilon0 + epsilon0)); last by case: Hepsilon0 => ? [? ?]; lra. apply ltR_add2l. have -> : INR #| M | = exp2 (log (INR #| M |)). rewrite logK // (_ : 0 = INR 0)%R //. by apply lt_INR; rewrite card_ord; exact/ltP. rewrite -ExpD. rewrite (_ : _ + _ = - n%:R * (`I(P, W) - log #| M |%:R / n%:R - 3 * epsilon0))%R; last first. field. by apply/eqP; rewrite INR_eq0' gtn_eqF //; case: Hn. rewrite (_ : _ / _ = r)%R; last by rewrite -Hk card_ord. apply (@ltR_trans (exp2 (- n%:R * epsilon0))). apply Exp_increasing => //. rewrite !mulNR ltR_oppr oppRK; apply/ltR_pmul2l. - apply ltR0n; by case: Hn. - case: Hepsilon0 => _ [_ Hepsilon0]. apply (@ltR_pmul2l 4) in Hepsilon0; last lra. rewrite mulRCA mulRV ?mulR1 in Hepsilon0; last exact/eqP. clear Hk; lra. apply (@ltR_leR_trans (exp2 (- (- (log epsilon0) / epsilon0) * epsilon0))). apply Exp_increasing => //; apply ltR_pmul2r. - rewrite /epsilon0_condition in Hepsilon0; tauto. - rewrite ltR_oppr oppRK; by case: Hn => _ [Hn2 _]. rewrite !mulNR -mulRA mulVR ?mulR1 ?oppRK; last first. by apply/gtR_eqF; case: Hepsilon0. rewrite logK; [| by case: Hepsilon0]. by apply/RleP; rewrite Order.POrderTheory.lexx. 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