diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v index 3198c51f..ccbb0a7f 100644 --- a/information_theory/channel_coding_direct.v +++ b/information_theory/channel_coding_direct.v @@ -1,10 +1,10 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum matrix perm. -Require Import Reals Lra Classical. -From mathcomp Require Import Rstruct classical_sets. -Require Import ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix perm. +From mathcomp Require Import Rstruct classical_sets reals boolp lra ring. +From mathcomp Require Import archimedean mathcomp_extra. +Require Import realType_ext realType_logb ssr_ext ssralg_ext bigop_ext. Require Import fdist proba entropy aep typ_seq joint_typ_seq channel. Require Import channel_code. @@ -28,25 +28,28 @@ Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. -Local Open Scope R_scope. +Local Open Scope ring_scope. Local Open Scope fdist_scope. Local Open Scope jtyp_seq_scope. Local Open Scope channel_code_scope. Local Open Scope channel_scope. Local Open Scope vec_ext_scope. +Import Order.Theory GRing.Theory Num.Theory. +#[local] Definition R := Rdefinitions.R. + Module Wght. Section wght. Variables (A M : finType) (P : {fdist A}) (n : nat). -Definition f := [ffun g : encT A M n => \prod_(m in M) P `^ n (g m)]. +Definition f := [ffun g : encT A M n => \prod_(m in M) (P `^ n) (g m)]. -Lemma f0 g : (0 <= f g)%mcR. Proof. rewrite ffunE; apply/RleP; exact: prodR_ge0. Qed. +Lemma f0 g : 0 <= f g. Proof. by rewrite ffunE prodr_ge0. Qed. Lemma f1 : \sum_(g in {ffun M -> 'rV[A]_n}) f g = 1. Proof. under eq_bigr do rewrite ffunE /=. -rewrite -(bigA_distr_bigA (fun _ v => P `^ n v)) /=. +rewrite -(bigA_distr_bigA (fun _ v => (P `^ n) v)) /=. rewrite [RHS](_ : _ = \prod_(m0 : M | xpredT m0) 1); last by rewrite big1. by apply eq_bigr => _ _; rewrite (FDist.f1 (P `^ n)). Qed. @@ -92,15 +95,15 @@ Lemma good_code_sufficient_condition P W epsilon exists f, echa(W , mkCode f (phi f)) < epsilon. Proof. move=> H. -apply not_all_not_ex => abs. +apply/not_existsP => abs. set x := \sum_(f <- _) _ in H. have : \sum_(f : encT A M n) Wght.d P f * epsilon <= x. - rewrite /x; apply leR_sumRl => //= f _. - - by apply leR_wpmul2l => //; exact/Rnot_lt_le/abs. - - by apply mulR_ge0 => //; exact/RleP/echa_ge0. -apply/Rlt_not_le/(@ltR_leR_trans epsilon) => //. -rewrite -big_distrl /= (FDist.f1 (Wght.d P)) mul1R. -by apply/RleP; rewrite Order.POrderTheory.lexx. + rewrite /x ler_suml => //= f _. + by rewrite ler_wpM2l // leNgt; exact/negP. +apply/negP. +rewrite -ltNge. +apply/(lt_le_trans H). +by rewrite -big_distrl /= (FDist.f1 (Wght.d P)) mul1r. Qed. Definition o_PI (m m' : M) := fun g : encT A M n => [ffun x => g (tperm m m' x)]. @@ -217,19 +220,11 @@ End joint_typicality_decoding. (* TODO: move? *) Section sum_rV_ffun. -Import Monoid.Theory. -Variable R : Type. -Variable times : Monoid.mul_law 0. -Local Notation "*%M" := times (at level 0). -Variable plus : Monoid.add_law 0 *%M. -Local Notation "+%M" := plus (at level 0). - -Lemma sum_rV_ffun (I J : finType) (F : {ffun I -> J} -> R) +Lemma sum_rV_ffun S (I J : finType) (F : {ffun I -> J} -> S) (G : _ -> _ -> _) (idef : I) (zero : 'I_ _) : O = zero -> - \big[+%M/0]_(j : 'rV[J]_#|I|) G (F [ffun x => j ord0 (enum_rank x)]) (j ord0 zero) = - \big[+%M/0]_(f : {ffun I -> J}) G (F f) (f (nth idef (enum I) 0)). + \sum_(j : 'rV[J]_#|I|) G (F [ffun x => j ord0 (enum_rank x)]) (j ord0 zero) = + \sum_(f : {ffun I -> J}) G (F f) (f (nth idef (enum I) 0)) :> R. Proof. -Local Open Scope ring_scope. move=> Hzero. rewrite (reindex_onto (fun y : {ffun _ -> J} => \row_(i < _) y (enum_val i)) (fun p => [ffun x => p ord0 (enum_rank x)])) //. @@ -245,7 +240,6 @@ rewrite (reindex_onto (fun y : {ffun _ -> J} => \row_(i < _) y (enum_val i)) move=> i _. apply/rowP => a; by rewrite mxE ffunE enum_valK. Qed. - End sum_rV_ffun. Section random_coding_good_code_existence. @@ -255,9 +249,11 @@ Variables (B A : finType) (W : `Ch(A, B)) (P : {fdist A}). Definition epsilon0_condition r epsilon epsilon0 := 0 < epsilon0 /\ epsilon0 < epsilon / 2 /\ epsilon0 < (`I(P, W) - r) / 4. +(* TODO move *) +Definition frac_part (x : R) := x - (Num.floor x)%:~R. Definition n_condition r epsilon0 n := - (O < n)%nat /\ - log epsilon0 / epsilon0 < INR n /\ - frac_part (exp2 (INR n * r)) = 0 /\ (JTS_1_bound P W epsilon0 <= n)%nat. + (O < n)%nat /\ - log epsilon0 / epsilon0 < n%:R /\ + frac_part (Exp 2 (r *+ n)) = 0 /\ (JTS_1_bound P W epsilon0 <= n)%nat. Definition cal_E M n epsilon (f : encT A M n) m := [set vb | prod_rV (f m, vb) \in `JTS P W n epsilon]. @@ -289,7 +285,7 @@ Qed. Lemma rsum_rmul_tuple_pmf_tnth {C : finType} n k (Q : {fdist C}) : \sum_(t : {:k.-tuple ('rV[C]_n)}) \prod_(m < k) (Q `^ n) t !_ m = 1. Proof. -transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) Q `^ _ (j m)). +transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) (Q `^ _) (j m)). rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)]) (fun x => fgraph x)) //=; last first. by move=> f _; apply/ffunP => /= i; rewrite ffunE tnth_fgraph enum_rankK. @@ -298,8 +294,8 @@ transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) Q `^ _ (j m)). - move=> i /=; apply/esym/eqP/eq_from_tnth => j. by rewrite tnth_fgraph ffunE enum_valK. - by move=> i _; apply eq_bigr => j _; rewrite ffunE /= tcastE -enum_rank_ord. -rewrite -(bigA_distr_bigA (fun m xn => Q `^ _ xn)) /= big_const. -by rewrite FDist.f1 iter_mulR exp1R. +rewrite -(bigA_distr_bigA (fun m xn => (Q `^ _) xn)) /= big_const. +by rewrite FDist.f1 iter_mulr mulr1 expr1n. Qed. (* TODO: move? *) @@ -331,13 +327,14 @@ rewrite {1}/cal_E. case/card_gt0P : (fdist_card_neq0 P) => a _. pose zero := @enum_rank M ord0. have : 0%N = zero :> nat by rewrite /zero enum_rank_ord. -move/(@sum_rV_ffun _ _ _ _ _ (Wght.d P) - (fun r v => r * Pr (W ``(| v )) (~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0])) - ord0 zero). +move/(sum_rV_ffun (Wght.d P) + (fun r v => + r * Pr (W ``(| v )) (~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0])) + ord0). rewrite (_ : nth ord0 (enum M) 0 = ord0); last by rewrite enum_ordSl. move=> <- /=. transitivity (\sum_(v : 'rV['rV[A]_n]_#|M|) ( - (\prod_(m : M) P `^ n ([ffun x => v ``_ x] (enum_rank m))) * + (\prod_(m : M) (P `^ n) ([ffun x => v ``_ x] (enum_rank m))) * \sum_(w | w \in ~: cal_E epsilon0 [ffun x => v ``_ x] zero) (W ``(| [ffun x => v ``_ x] zero)) w)). apply eq_bigr => v _; congr (_ * _). @@ -351,12 +348,14 @@ transitivity (\sum_(v : 'rV[A]_n) (\sum_(y in ~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0]) (W ``(| v)) y) * \sum_(j in {: #|M|.-1.-tuple ('rV[A]_n)}) - (\prod_(m : M) P `^ _ ((tcast M_prednK [tuple of v :: j]) !_ (enum_rank m)))). - rewrite (reindex_onto (fun y : {ffun _ -> 'rV__} => \row_(i < _) y (enum_val i)) + (\prod_(m : M) + (P `^ _) ((tcast M_prednK [tuple of v :: j]) !_ (enum_rank m)))). + rewrite (reindex_onto + (fun y : {ffun _ -> 'rV__} => \row_(i < _) y (enum_val i)) (fun p : 'rV_ _ => [ffun x => p ``_ (enum_rank x)])) //=; last first. move=> v _; by apply/rowP => i; rewrite mxE ffunE enum_valK. apply trans_eq with (\sum_(f : {ffun M -> 'rV__}) - ((\prod_(m < k.+1) P `^ n (f m)) * + ((\prod_(m < k.+1) (P `^ n) (f m)) * \sum_(y in ~: [set y0 | prod_rV (f ord0, y0) \in `JTS P W n epsilon0]) W ``(y | f ord0))). apply eq_big => //= f. @@ -367,12 +366,12 @@ transitivity (\sum_(v : 'rV[A]_n) move=> ?; by rewrite !inE -[in RHS]Hf !ffunE mxE. move=> ? _; by rewrite -[in RHS]Hf !ffunE mxE. rewrite (_ : ord0 = nth ord0 (enum M) 0); last by rewrite enum_ordSl. - rewrite -(big_tuple_ffun _ (fun f => \prod_(m : M) P `^ n (f m)) + rewrite -(big_tuple_ffun _ (fun f => \prod_(m : M) (P `^ n) (f m)) (fun r yn => r * (\sum_(y in ~: [set y0 | prod_rV (yn, y0) \in `JTS P W n epsilon0]) - W ``(y | yn))) (\row_(i < n) a) ord0)%R. + W ``(y | yn))) (\row_(i < n) a) ord0). transitivity (\sum_(j : _) - (\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) * + (\prod_(m : M) (P `^ n) ((tcast M_prednK j) !_ (enum_rank m))) * (\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in `JTS P W n epsilon0]) W ``(y | nth (\row_(i < n) a) j 0))). @@ -385,44 +384,43 @@ transitivity (\sum_(v : 'rV[A]_n) by rewrite tcastE /= cast_ord_id. apply eq_big => m; by rewrite !inE H. rewrite -(@big_tuple_cons_behead _ #|M|.-1 - (fun j => ((\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) * + (fun j => ((\prod_(m : M) (P `^ n) ((tcast M_prednK j) !_ (enum_rank m))) * (\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in `JTS P W n epsilon0]) W ``(y | nth (\row_(i < n) a) j 0)))) xpredT xpredT). - apply eq_bigr => ta _ /=; by rewrite -big_distrl /= mulRC. -transitivity ((\sum_(ta in 'rV[A]_n) P `^ _ ta * + apply eq_bigr => ta _ /=; by rewrite -big_distrl /= mulrC. +transitivity ((\sum_(ta in 'rV[A]_n) (P `^ _) ta * (\sum_(y in ~: [set y0 | prod_rV (ta, y0) \in `JTS P W n epsilon0]) (W ``(| ta ) ) y)) * - \sum_(j in {:k.-tuple ('rV[A]_n)}) \prod_(m < k) (P `^ _ (j !_ m)))%R. + \sum_(j in {:k.-tuple ('rV[A]_n)}) \prod_(m < k) ((P `^ _) (j !_ m))). rewrite big_distrl /=. apply eq_bigr => ta _. - rewrite -mulRA mulRCA; congr Rmult. + rewrite -mulrA mulrCA; congr (_ * _). transitivity (\sum_(j in {: #|'I_k|.-tuple ('rV[A]_n) }) - P `^ _ ta * \prod_(m < k) P `^ _ (j !_ (enum_rank m)))%R. + (P `^ _) ta * \prod_(m < k) (P `^ _) (j !_ (enum_rank m))). have k_prednK : #|'I_k.+1|.-1 = #|'I_k| by rewrite !card_ord. rewrite (big_tcast (esym k_prednK)) esymK. apply eq_bigr => i0 Hi0. rewrite big_ord_recl /=. - congr (P `^ _ _ * _)%R; first by rewrite tcastE // enum_rank_ord. - apply eq_bigr => i1 _; congr (P `^ _ _). + congr ((P `^ _) _ * _); first by rewrite tcastE // enum_rank_ord. + apply eq_bigr => i1 _; congr ((P `^ _) _). rewrite !tcastE {1}/tnth /=. rewrite (_ : enum_rank _ = (enum_rank i1).+1 :> nat) /=; last by rewrite !enum_rank_ord. apply set_nth_default; by rewrite size_tuple /= enum_rank_ord /= card_ord. - rewrite -big_distrr /=; congr (_ * _)%R. + rewrite -big_distrr /=; congr (_ * _). rewrite (big_tcast (esym (card_ord k))) esymK. apply eq_bigr => /= i0 _. apply eq_bigr => /= i1 _. by rewrite tcastE -enum_rank_ord. -rewrite rsum_rmul_tuple_pmf_tnth mulR1. +rewrite rsum_rmul_tuple_pmf_tnth mulr1. transitivity (\sum_(v in 'rV[A]_n) \sum_(y in ~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0]) - ((P `X W) `^ n (prod_rV (v, y))))%R. + (((P `X W) `^ n) (prod_rV (v, y)))). apply eq_bigr => /= v _. rewrite big_distrr /=. apply eq_bigr => // w _. rewrite DMCE 2!fdist_rVE -big_split /=. apply eq_bigr => /= i _. - rewrite fdist_prodE -fst_tnth_prod_rV -snd_tnth_prod_rV /= mulRC. - by rewrite RmultE GRing.mulrC. + by rewrite fdist_prodE -fst_tnth_prod_rV -snd_tnth_prod_rV /=. rewrite /Pr big_rV_prod pair_big_dep /=. by apply eq_bigl; case=> /= ? ?; rewrite !inE. Qed. @@ -430,11 +428,11 @@ Qed. (* TODO: move? *) Lemma big_cat_tuple {C : finType} m n (F : (m + n)%nat.-tuple C -> R) : (\sum_(i in {:m.-tuple C}) \sum_(j in {: n.-tuple C}) - F [tuple of (i ++ j)] = \sum_(p in {: (m + n)%nat.-tuple C}) (F p))%R. + F [tuple of (i ++ j)] = \sum_(p in {: (m + n)%nat.-tuple C}) (F p)). Proof. elim: m n F => [m2 F /=|m IH n F]. - transitivity (\sum_(i <- [tuple] :: [::]) - \sum_(j in {: m2.-tuple C}) F [tuple of i ++ j] )%R. + \sum_(j in {: m2.-tuple C}) F [tuple of i ++ j] ). apply congr_big => //=. apply (@eq_from_nth _ [tuple]); rewrite /index_enum -enumT /= (eqP (enum_tupleP _)) card_tuple expn0 //. @@ -442,11 +440,12 @@ elim: m n F => [m2 F /=|m IH n F]. rewrite tupleE /=. case: (enum _) => //= t. by rewrite (tuple0 t). - rewrite big_cons /= big_nil /= addR0. + rewrite big_cons /= big_nil /= addr0. apply eq_bigr => // i _; congr F. exact/val_inj. - symmetry. - transitivity (\sum_(p in [the finType of (m + n).+1.-tuple C]) F p)%R; first by apply congr_big. + transitivity (\sum_(p in [the finType of (m + n).+1.-tuple C]) F p); + first by apply congr_big. rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT). rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT). apply eq_bigr => i _. @@ -457,11 +456,11 @@ Qed. (* TODO: move? *) Lemma big_cat_tuple_seq {C : finType} m n (F : seq C -> R) : - (\sum_(i in {:m.-tuple C} ) \sum_(j in {: n.-tuple C}) (F (i ++ j)) = - \sum_(p in {: (m + n)%nat.-tuple C}) (F p))%R. + \sum_(i in {:m.-tuple C} ) \sum_(j in {: n.-tuple C}) (F (i ++ j)) = + \sum_(p in {: (m + n)%nat.-tuple C}) (F p). Proof. -move: (@big_cat_tuple _ m n (fun l => if size l == (m + n)%nat then F l else R0)). -set lhs := (\sum_(i in _) _)%R => H. +move: (@big_cat_tuple _ m n (fun l => if size l == (m + n)%nat then F l else 0)). +set lhs := (\sum_(i in _) _) => H. apply trans_eq with lhs. apply eq_bigr => /= t _; apply eq_bigr => /= t' _. case: ifP => //; by rewrite size_tuple eqxx. @@ -472,7 +471,7 @@ Lemma second_summand n k epsilon0 : let M := 'I_k.+1 in forall i, i != ord0 -> (\sum_(f : encT A M n) Wght.d P f * - Pr (W ``(| f ord0)) (cal_E epsilon0 f i))%R = + Pr (W ``(| f ord0)) (cal_E epsilon0 f i)) = Pr ((P `^ n) `x `O( P , W ) `^ n) [set x | prod_rV x \in `JTS P W n epsilon0]. Proof. move=> M. @@ -489,7 +488,7 @@ transitivity ( \sum_(ji in 'rV[A]_n) Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] * \sum_(y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0]) - (W ``(| j0)) y)%R. + (W ``(| j0)) y). transitivity ( \sum_(j0 in 'rV[A]_n) \sum_(j1 in {: i.-1.-tuple ('rV[A]_n)}) @@ -497,12 +496,12 @@ transitivity ( \sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)}) Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] * \sum_( y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0]) - (W ``(| j0) ) y)%R. + (W ``(| j0) ) y). rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)]) (fun y => fgraph y)) /=; last first. move=> f _; apply/ffunP => m; by rewrite ffunE tnth_fgraph enum_rankK. transitivity ( \sum_(j : _) (Wght.d P [ffun x => j!_(enum_rank x)] * - Pr (W ``(| [ffun x => j!_(enum_rank x)] ord0)) (E_F_N [ffun x => j!_(enum_rank x)] i)))%R. + Pr (W ``(| [ffun x => j!_(enum_rank x)] ord0)) (E_F_N [ffun x => j!_(enum_rank x)] i))). apply eq_big => //= x; apply/eqP/eq_from_tnth => j. by rewrite tnth_fgraph ffunE enum_valK. rewrite (big_tcast (card_ord k.+1)). @@ -520,11 +519,11 @@ transitivity ( rewrite (big_tcast Hs) -(big_tuple_cons_behead _ xpredT xpredT). apply eq_bigr => i2 _. have Ht : (#|'I_k.+1| - i.+1 = k - i)%nat by rewrite card_ord /= subSS. - rewrite (big_tcast Ht) //; apply eq_bigr => /= i3 _; congr (_ * _)%R. + rewrite (big_tcast Ht) //; apply eq_bigr => /= i3 _; congr (_ * _). - rewrite 2!Wght.dE /Wght.f 2!ffunE /=. rewrite (reindex_onto enum_rank enum_val); last by move=> *; rewrite enum_valK. apply eq_big => /=; first by move=> x; rewrite enum_rankK eqxx inE. - move=> i4 _; congr (P `^ _ _). + move=> i4 _; congr ((P `^ _) _). rewrite !ffunE; congr (_ !_ _). apply/val_inj => /=. rewrite [LHS]eq_tcast /= !eq_tcast /= [RHS]eq_tcast eq_tcast /=; congr (_ :: _ ++ _ :: _). @@ -556,7 +555,7 @@ transitivity ( ((P `^ n) j0) * ((P `^ n) ji) * (\sum_( y | y \in [set y0 | prod_rV (ji , y0) \in `JTS P W n epsilon0]) - (W ``(| j0) ) y)))%R. + (W ``(| j0) ) y))). rewrite !big_distrl /=. apply eq_bigr => j1 _. rewrite !big_distrl /=. @@ -565,59 +564,59 @@ transitivity ( apply eq_bigr => j0 _. rewrite !big_distrr /=. apply eq_bigr => j3 _. - rewrite !mulRA Wght.dE /Wght.f /=; congr (_ * _)%R. - transitivity (\prod_( i <- j0 :: j1 ++ j3 :: j2) P `^ _ i)%R; last first. - rewrite big_cons -mulRA mulRCA; congr (_ * _)%R. - rewrite big_cat /= big_cons [in RHS]mulRC mulRCA; congr (_ * _)%R. - by rewrite big_cat /= mulRC. + rewrite !mulrA Wght.dE /Wght.f /=; congr (_ * _). + transitivity (\prod_( i <- j0 :: j1 ++ j3 :: j2) (P `^ _) i); last first. + rewrite big_cons -mulrA mulrCA; congr (_ * _). + rewrite big_cat /= big_cons [in RHS]mulrC mulrCA; congr (_ * _). + by rewrite big_cat /= mulrC. rewrite [in RHS](big_nth j0) /= big_mkord. transitivity (\prod_(j < #|@predT M|) - P `^ _ ([ffun x => (tcast Hcast [tuple of j0 :: j1 ++ j3 :: j2])!_(enum_rank x)] (enum_val j)))%R. + (P `^ _) ([ffun x => (tcast Hcast [tuple of j0 :: j1 ++ j3 :: j2])!_(enum_rank x)] (enum_val j))). rewrite ffunE; apply eq_big => ? //= _. by rewrite !ffunE enum_valK. have j_M : (size (j1 ++ j3 :: j2)).+1 = #|M|. rewrite size_cat (size_tuple j1) /= (size_tuple j2) card_ord. by rewrite -[RHS](card_ord k.+1) -Hcast card_ord. rewrite j_M. - apply eq_bigr => i0 _; congr (P `^ n _). + apply eq_bigr => i0 _; congr ((P `^ n) _). rewrite ffunE /= enum_valK tcastE /tnth /=. apply set_nth_default; by rewrite /= j_M ltn_ord. transitivity (\sum_(j0 : 'rV[A]_n) \sum_(ji : 'rV[A]_n) ((P `^ n) j0) * ((P `^ n) ji) * (\sum_( y | y \in [set y0 in 'rV[B]_n | prod_rV (ji , y0) \in `JTS P W n epsilon0]) - (W ``(| j0)) y))%R. - set lhs := (\sum_(_ <- _) _)%R. - suff : lhs = 1%R by move=> ->; rewrite mul1R. + (W ``(| j0)) y)). + set lhs := (\sum_(_ <- _) _). + suff : lhs = 1 by move=> ->; rewrite mul1r. rewrite /lhs {lhs}. - rewrite (@big_cat_tuple_seq _ i.-1 (#|M| - i.+1) (fun x => \prod_(i0 <- x) (P `^ n) i0))%R. + rewrite (@big_cat_tuple_seq _ i.-1 (#|M| - i.+1) (fun x => \prod_(i0 <- x) (P `^ n) i0)). by rewrite rsum_rmul_tuple_pmf. transitivity (\sum_(ji : 'rV[A]_n) ((P `^ n) ji) * (\sum_(y | y \in [set y0 | prod_rV (ji , y0) \in `JTS P W n epsilon0]) - \sum_(j0 : 'rV[A]_n) ((W ``(| j0) ) y) * ((P `^ n) j0)))%R. + \sum_(j0 : 'rV[A]_n) ((W ``(| j0) ) y) * ((P `^ n) j0))). rewrite exchange_big /=. apply eq_bigr => ta _. - transitivity (\sum_(i1 : 'rV[A]_n) P `^ _ ta * P `^ _ i1 * + transitivity (\sum_(i1 : 'rV[A]_n) (P `^ _) ta * (P `^ _) i1 * (\sum_(y in [set y0 | prod_rV (ta, y0) \in `JTS P W n epsilon0]) - W ``(y | i1)))%R. + W ``(y | i1))). apply eq_bigr => i1 _. - by rewrite -mulRA mulRCA mulRA. + by rewrite -mulrA mulrCA mulrA. rewrite exchange_big /= big_distrr /=. apply eq_bigr => ta' _. - rewrite -[in X in _ = (_ * X)%R]big_distrl /= -mulRA; congr Rmult. - by rewrite mulRC. + rewrite -[in X in _ = (_ * X)]big_distrl /= -mulrA; congr (_ * _). + by rewrite mulrC. transitivity (\sum_(ji : 'rV[A]_n) ((P `^ n) ji) * \sum_( y | y \in [set y0 | prod_rV (ji , y0) \in `JTS P W n epsilon0]) - ((`O(P , W)) `^ n) y)%R. - apply eq_bigr => ta _; congr (_ * _)%R; apply eq_bigr => /= tb _. + ((`O(P , W)) `^ n) y). + apply eq_bigr => ta _; congr (_ * _); apply eq_bigr => /= tb _. by rewrite fdist_rV_out; apply eq_bigr => i0 _; by rewrite DMCE. transitivity (\sum_(v : 'rV[A]_n) (\sum_(y | y \in [set y0 | prod_rV (v , y0) \in `JTS P W n epsilon0]) - ((P `^ n) `x ((`O(P , W)) `^ n)) (v, y)))%R. + ((P `^ n) `x ((`O(P , W)) `^ n)) (v, y))). apply eq_bigr => // v _. rewrite big_distrr /=; apply eq_bigr => w _; by rewrite fdist_prodE. transitivity (\sum_( jiy | prod_rV jiy \in `JTS P W n epsilon0) - ((P `^ n) `x ((`O(P , W)) `^ n)) jiy)%R. + ((P `^ n) `x ((`O(P , W)) `^ n)) jiy). rewrite [in LHS]pair_big_dep /=. by apply eq_big => -[? ?] /=; rewrite !inE ?fdist_prodE. by apply eq_bigl => ?; rewrite !inE. @@ -665,84 +664,91 @@ apply/idP/idP. case/andP : Hm2 => _ /forallP /(_ m); by rewrite !inE m_tb m20 Hm implyTb. Qed. -Local Open Scope zarith_ext_scope. +Lemma ExpK (R' : realType) n x : (1 < n)%N -> Log n (Exp n%:R x) = x :> R'. +Proof. Import exp. +move=> n1; rewrite /Exp /Log prednK// 1?ltnW// ln_powR mulrK //. +by apply/unitf_gt0/ln_gt0; rewrite ltr1n. +Qed. 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)) | /\ + exists M : finType, (0 < #|M|)%nat /\ #|M| = `| Num.floor (Exp 2 (rate r *+ n)) |%N /\ 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. + (\sum_(f : encT A M n) Wght.d P f * echa(W , mkCode f (Jtdec f))) < epsilon. Proof. move=> Hepsilon r epsilon0 Hepsilon0 n Hn. -have [k Hk] : exists k, (log (INR k.+1) / INR n = r)%R. +have [k Hk] : exists k, log k.+1%:R / n%:R = r :> R. case: Hn => ? [? [Hn2 ?]]. - case/fp_nat : Hn2 => k Hn2. - exists '| k |.-1. + exists `| Num.floor (Exp 2 (rate r *+ n)) |.-1. rewrite prednK; last first. - apply/ltP/INR_lt. (* TODO: ssrZ? *) - 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. + rewrite absz_gt0; apply/eqP => Habs. + rewrite /frac_part Habs subr0 in Hn2. + suff : false => //. + have := @Exp_gt0 R 2 (rate r *+ n). + by rewrite Hn2 ltxx; apply. + rewrite eqr_divr_mulr; last by rewrite (eqr_nat R n 0) -lt0n. + rewrite -[in LHS]mulrz_nat natz gez0_abs. + move/subr0_eq: Hn2 => <-. + by rewrite /log ExpK // mulr_natr. + by rewrite floor_ge0 Exp_ge0. set M : finType := 'I_k.+1. exists M. 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. + have -> : rate r *+ n = log k.+1%:R. + rewrite -Hk -[LHS]mulr_natr -mulrA mulVr ?mulr1 //. + by case: Hn; rewrite -(ltr_nat R) => /unitf_gt0. + rewrite LogK // card_ord (floor_def (m:=k.+1)) // -{1}natz mulrz_nat lexx. + by rewrite addrC -intS -natz mulrz_nat ltr_nat leqnn. 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 [X in X < _](_ : _ = (1 / #|M|%:R * + \sum_(f : encT A M n) Wght.d P f * (\sum_(m in M) e(W, mkCode f (Jtdec f)) m))); 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. + by rewrite -!mulrA mulrC mul1r -!mulrA [Wght.d _ _ * _]mulrC. +rewrite [X in X < _](_ : _ = (\sum_(f : encT A M n) Wght.d P f * (e(W, mkCode f (Jtdec f))) ord0)); last first. + transitivity (1 / #|M|%:R * + \sum_(f : encT A M n) (\sum_(m in M) Wght.d P f * (e(W, mkCode f (Jtdec f))) m)). 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. + transitivity (1 / #|M|%:R * \sum_(f : encT A M n) + (\sum_( m_ in M ) Wght.d P f * (e(W, mkCode f (Jtdec f))) ord0)). + congr (_ * _). 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. + by move: Hepsilon0; rewrite /epsilon0_condition; case => /ltW. + rewrite exchange_big /= big_const /= iter_addr addr0 div1r. + by rewrite -(mulr_natl (\sum__ _)) mulrA mulVr (mul1r,unitf_gt0) // card_ord. set Cal_E := @cal_E M n epsilon0. -apply/RltP. -apply (@leR_ltR_trans +apply (@le_lt_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). + \sum_(f : encT A M n) Wght.d P f * Pr (W ``(| f ord0)) (Cal_E f i))). 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)) + apply ler_sum => /= i _. + rewrite -big_distrr /= -mulrDr. + apply ler_wpM2l; first by rewrite FDist.ge0. + rewrite [X in (X <= _)](_ : _ = 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). + apply (@le_trans _ _ (Pr (W ``(| i ord0)) (~: Cal_E i ord0) + + Pr (W ``(| i ord0)) (\bigcup_(i0 | i0 != ord0) (Cal_E i i0)))). exact: le_Pr_setU. - exact/leR_add2l/Pr_bigcup. + by rewrite lerD2l 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. +set lhs := (\sum_(_ < _ | _) _). +have -> : lhs = (#| M |.-1%:R * Pr ((P `^ n) `x ((`O(P , W)) `^ n)) [set x | prod_rV x \in `JTS P W n epsilon0])%fdist. 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. + Pr ((P `^ n) `x ((`O( P , W )) `^ n))%fdist [set x | prod_rV x \in `JTS P W n epsilon0]); last first. + rewrite big_const /= iter_addr addr0 -[in RHS]mulr_natl. + congr (_%:R * _). rewrite card_ord /=. transitivity (#| finset.setT :\ (@ord0 k)|). move: (cardsD1 (@ord0 k) finset.setT) => /=. @@ -753,135 +759,142 @@ have -> : lhs = (#| M |.-1%:R * Pr ((P `^ n) `x ((`O(P , W)) `^ n)) [set x | pro by rewrite -!topredE /= !finset.in_set andbC/= inE. 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_setC leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //. +apply (@le_lt_trans _ _ (epsilon0 + k%:R * + Pr (P `^ n) `x (`O(P , W) `^ n) [set x | prod_rV x \in `JTS P W n epsilon0])%fdist). + rewrite lerD2r. + rewrite Pr_setC lerBlDr addrC -lerBlDr; 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. +apply (@le_lt_trans _ _ (epsilon0 + + #| M |%:R * Exp 2 (- n%:R * (`I(P, W ) - 3 * epsilon0)))). + rewrite lerD2l ler_pM //. by rewrite card_ord ler_nat. + exact: non_typical_sequences. +apply (@lt_trans _ _ (epsilon0 + epsilon0)); last by case: Hepsilon0 => ? [? ?]; lra. +rewrite ltrD2l. +have -> : #| M |%:R = Exp 2 (log #| M |%:R) :> R by rewrite LogK // card_ord. +rewrite -powRD; last by rewrite (eqr_nat R 2 0) implybT. +rewrite (_ : _ + _ = - n%:R * (`I(P, W) - log #| M |%:R / n%:R - 3 * epsilon0)); 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. + by case: Hn; rewrite -(ltr_nat R) => /lt0r_neq0. +rewrite (_ : _ / _ = rate r); last by rewrite -Hk card_ord. +apply (@lt_trans _ _ (Exp 2 (- n%:R * epsilon0))). + apply Exp_increasing; first by rewrite (ltr_nat R 1 2). + rewrite -mulr_natr -mulNr. + rewrite -2!mulrA ltr_nM2l ?oppr_lt0 //. + rewrite ltr_pM2l; last by case: Hn; rewrite (ltr_nat R 0 n). + case: Hepsilon0 => _ [_ Hepsilon0]. + rewrite -(@ltr_pM2l R 4) in Hepsilon0; last lra. + rewrite mulrCA mulrV ?mulR1 in Hepsilon0; last first. + by rewrite unitfE (eqr_nat R 4 0). + lra. +apply (@lt_le_trans _ _ (Exp 2 (- (- (log epsilon0) / epsilon0) * epsilon0))). + rewrite /Exp /powR (eqr_nat R 2 0) /=. + rewrite ltr_expR ltr_pM2r; last by apply/ln_gt0; rewrite (ltr_nat R 1 2). + rewrite ltr_pM2r; first last. + - by case: Hepsilon0. + - rewrite -mulr_natr ltrN2 mul1r. + by case: Hn => _ []. +rewrite !mulNr opprK -mulrA mulVr; last first. + by case: Hepsilon0 => /lt0r_neq0; rewrite unitfE. +by rewrite mulr1 LogK ?lexx //; case: Hepsilon0. Qed. End random_coding_good_code_existence. +(* TODO: move to realType_logb *) +Lemma exists_frac_part (P : nat -> Prop) : (exists n, P n) -> + forall num den, (0 < num)%nat -> (0 < den)%nat -> + (forall n m, (n <= m)%nat -> P n -> P m) -> + exists n, P n /\ + frac_part (Exp 2 (n%:R * (log num%:R / den%:R))) = 0. +Proof. +case=> n Pn num den Hden HP. +exists (n * den)%nat. +split. + apply H with n => //. + by rewrite -{1}(muln1 n) leq_mul2l HP orbC. +rewrite natrM -mulrA (mulrCA den%:R) mulrV // ?mulr1; last first. + by rewrite unitfE lt0r_neq0 // (ltr_nat R 0). +rewrite /frac_part /Exp mulrC exp.powRrM -/(Exp 2 _). +rewrite (LogK (n:=2)) // ?ltr0n // exp.powR_mulrn ?ler0n // -natrX. +by rewrite floorK ?subrr // intr_nat. +Qed. + Section channel_coding_theorem. Variables (A B : finType) (W : `Ch(A, B)). Hypothesis set_of_I_nonempty : classical_sets.nonempty (fun y => exists P, `I(P, W) = y). -Local Open Scope zarith_ext_scope. - -Theorem channel_coding (r : CodeRateType) : r < capacity W -> +Theorem channel_coding (r : CodeRateType) : rate r < capacity W -> forall epsilon, 0 < epsilon -> exists n M (c : code A B M n), CodeRate c = r /\ echa(W, c) < epsilon. Proof. move=> r_I epsilon Hepsilon. -have [P HP] : exists P : {fdist A}, r < `I(P, W). - apply NNPP => abs. +have [P HP] : exists P : {fdist A}, rate r < `I(P, W). + apply/not_existsP => 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. + by move=> P; rewrite leNgt; apply/negP. 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. + by exists (rate r) => _ [Q _ <-]. move=> /(@Rsup_isLub 0 [set `I(P, W) | P in [set: {fdist A}]])[_]. apply. - by move=> x [P _ <-{x}]; exact/RleP/abs. + by move=> x [P _ <-{x}]. 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 ]. + 0 < epsilon0 /\ epsilon0 < epsilon / 2 /\ epsilon0 < (`I(P, W) - rate r) / 4. + exists ((Order.min (epsilon/2) ((`I(P, W) - rate r) / 4))/2). + have H0 : 0 < Order.min (epsilon / 2) ((`I(P, W) - rate r) / 4). + rewrite lt_min; lra. + split; first by apply mulr_gt0 => //; lra. + split; apply/(@lt_le_trans _ _ (Num.min (epsilon / 2) ((`I(P, W) - rate r) / 4))); try by rewrite ltr_pdivrMr // mulr_natr mulr2n ltr_pwDr. + by rewrite ge_min lexx. + by rewrite ge_min lexx orbT. 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. + - log epsilon0 / epsilon0 < n%:R /\ + (maxn (Nup (aep_bound P (epsilon0 / 3))) + (maxn (Nup (aep_bound (`O(P , W)) (epsilon0 / 3))) + (Nup (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)) |))). + (maxn (Nup (- log epsilon0 / epsilon0)) + (maxn (Nup (aep_bound P (epsilon0 / 3))) + (maxn (Nup (aep_bound (`O(P , W)) (epsilon0 / 3))) + (Nup (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. + apply (@lt_le_trans _ R (Num.floor (- log epsilon0 / epsilon0) + 1)%:~R). + exact: lt_succ_floor. + apply (@le_trans _ R (Nup (- log epsilon0 / epsilon0))%:R). + by rewrite /Nup -addn1 -mulrz_nat natz PoszD ler_int lerD // lez_abs. + by rewrite ler_nat /supermax 2!leq_max leqnn orbT. by rewrite [X in (_ <= X)%nat]maxnA leq_maxr. + rewrite /n_condition. 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. + by rewrite -Hr mulr_natl in Hn2. split. by apply/(@leq_trans n1) => //; tauto. split. - by apply (@ltR_leR_trans (INR n1)); [tauto | exact/le_INR/leP]. + by apply: (@lt_le_trans _ _ n1%:R); [tauto | rewrite ler_nat]. by apply leq_trans with n1 => //; tauto. -have He : (0 <= epsilon)%mcR. - apply/RleP. - by apply/ltRW. +have He : (0 <= epsilon) by apply ltW. 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. +case: (good_code_sufficient_condition 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 => _ [_ []]. +rewrite /CodeRate M_k -mulrz_nat natz gez0_abs; last first. + by rewrite floor_ge0 Exp_ge0. +case: Hn => Hn [_] []. +rewrite /frac_part => /subr0_eq <- _. +rewrite /log ExpK // -(mulr_natr (rate r)) mulrK //. +by apply/unitf_gt0; rewrite ltr0n. Qed. End channel_coding_theorem. diff --git a/lib/realType_ext.v b/lib/realType_ext.v index cae3399e..ca2a1a5d 100644 --- a/lib/realType_ext.v +++ b/lib/realType_ext.v @@ -56,6 +56,7 @@ move=> z0; split => [<-|->]; first by rewrite -mulrA mulVf // mulr1. by rewrite -mulrA mulfV // mulr1. Qed. +(* TODO: rename as prodr_gt0 *) Lemma prodR_gt0 (R : numDomainType) (A : finType) (F : A -> R) : (forall a, 0 < F a)%mcR -> (0 < \prod_(a : A) F a)%mcR. Proof. by move=> F0; elim/big_ind : _ => // x y ? ?; exact: mulr_gt0. Qed.