Library Infotheo.channel_coding_direct

Require Import Reals Fourier Classical.
Require Import Reals_ext ssr_ext Rssr log2 Rbigop tuple_prod.
Require Import proba entropy aep typ_seq joint_typ_seq channel channel_code.

Set Implicit Arguments.
Import Prenex Implicits.

Local Open Scope proba_scope.
Local Open Scope jtyp_seq_scope.
Local Open Scope channel_code_scope.
Local Open Scope channel_scope.

Module Wght.

Section Wght_sect.

Variables A M : finType.
Variable P : dist A.
Variable n : nat.

Definition pmf := fun f : encT A M n\rmul_(m in M) P `^ n (f m).

Lemma pmf0 (f : {ffun M 'rV[A]_n}) : 0 pmf f.

Lemma pmf1 : \rsum_(f | f \in {ffun M 'rV[A]_n}) pmf f = 1.

Definition d : dist [finType of encT A M n] := makeDist pmf0 pmf1.

End Wght_sect.

End Wght.


Section joint_typicality_decoding.

Variables A B M : finType.
Variable n : nat.

Definition not_preimg (phi : decT B M n) m := [set tb | phi tb != Some m].

Lemma e_m_Pr_not_preimg (W : `Ch_1(A, B)) (c : code A B M n) m :
  e( W , c ) m = Pr (W ``^ n (| enc c m )) (not_preimg (dec c) m).

Joint typicality decoding

Definition jtdec P W epsilon (f : encT A M n) : decT B M n :=
  [ffun tb [pick m |
    (prod_tuple (f m, tb) \in `JTS P W n epsilon) &&
    [ m', (m' != m) ==> (prod_tuple (f m', tb) \notin `JTS P W n epsilon)]]].

Lemma jtdec_map epsilon (P : dist A) (W : `Ch_1(A, B)) (f : encT A M n) tb m0 m1 :
  (prod_tuple (f m0, tb) \in `JTS P W n epsilon) &&
  [ m', (m' != m0) ==> (prod_tuple (f m', tb) \notin `JTS P W n epsilon)]
  (prod_tuple (f m1, tb) \in `JTS P W n epsilon) &&
  [ m', (m' != m1) ==> (prod_tuple (f m', tb) \notin `JTS P W n epsilon)]
  m0 = m1.

Hypothesis HM : (0 < #|M|)%nat.

Lemma good_code_sufficient_condition P W epsilon
  (phi : encT A M n decT B M n) :
  \rsum_(f : encT A M n) (Wght.d P f × echa(W , mkCode f (phi f))) < epsilon
   f, echa(W , mkCode f (phi f)) < epsilon.

Definition o_PI (m m' : M) := fun g : encT A M n[ffun x g (tperm m m' x)].

Lemma o_PI_2 (g : encT A M n) (m m' m_ : M) : (o_PI m m' (o_PI m m' g)) m_ = g m_.

Lemma wght_o_PI m m' P (h : encT A M n) : Wght.d P (o_PI m m' h) = Wght.d P h.

Lemma error_rate_symmetry (P : dist A) (W : `Ch_1(A, B)) epsilon :
  0 epsilon let Jtdec := jtdec P W epsilon in
     m m',
      \rsum_(f : encT A M n) (Wght.d P f × e(W, mkCode f (Jtdec f)) m) =
      \rsum_(f : encT A M n) (Wght.d P f × e(W, mkCode f (Jtdec f)) m').

End joint_typicality_decoding.

Section sum_rV_ffun.

Import Monoid.Theory.

Variable R : Type.
Variable times : Monoid.mul_law 0.
Notation Local "*%M" := times (at level 0).
Variable plus : Monoid.add_law 0 *%M.
Notation Local "+%M" := plus (at level 0).

Lemma sum_rV_ffun (I J : finType) (F : {ffun I J} R)
  (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)).
Local Open Scope ring_scope.

End sum_rV_ffun.

Section random_coding_good_code_existence.

Variables B A : finType.
Variable W : `Ch_1(A, B).
Variable P : dist A.

Definition epsilon0_condition r epsilon epsilon0 :=
  0 < epsilon0 epsilon0 < epsilon / 2 epsilon0 < (`I(P ; W) - r) / 4.

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.

the set of output tb such that (f m, tb) is jointly typical:

Definition cal_E M n epsilon (f : encT A M n) m :=
  [set tb | prod_tuple (f m, tb) \in `JTS P W n epsilon].

Local Open Scope tuple_ext_scope.

Lemma first_summand k n epsilon0 :
  let M := [finType of 'I_k.+1] in
  \rsum_(f : encT A M n) Wght.d P f ×
    Pr (W ``^ n (| f ord0)) (~: cal_E epsilon0 f ord0) =
  Pr (`J(P , W) `^ n) (~: `JTS P W n epsilon0).
Local Open Scope ring_scope.
Lemma big_head_behead_P_tuple {C:finType} n (F : n.+1.-tuple C R) (P1 : pred C) (P2 : pred ({: n.-tuple C})) :
  \rsum_(i in C | P1 i) \rsum_(j in {: n.-tuple C} | P2 j) (F [tuple of (i :: j)])
  =
  \rsum_(p in {: n.+1.-tuple C} | (P1 (thead p)) && (P2 (tbehead p)) ) (F p).


Lemma rsum_rmul_tuple_pmf_tnth {C:finType} n k (Q : dist C) :
  \rsum_(t : {:k.-tuple ('rV[C]_n)}) \rmul_(m < k) (Q `^ n) t \_ m = 1%R.

Qed.

Lemma second_summand n k epsilon0 :
  let M := [finType of 'I_k.+1] in
     i, i != ord0
      (\rsum_(f : encT A M n) Wght.d P f ×
        Pr (W ``^n (| f ord0)) (cal_E epsilon0 f i))%R =
   Pr ((P `^ n) `x ((`O( P , W )) `^ n)) [set x | prod_tuple x \in `JTS P W n epsilon0].
Lemma big_head_behead_tuple {C:finType} n (F : n.+1.-tuple C R) :
  \rsum_(i in C) \rsum_(j in {: n.-tuple C}) (F [tuple of (i :: j)]) =
  \rsum_(p in {: n.+1.-tuple C}) (F p).


Lemma big_cat_tuple {C:finType} m n (F : (m + n)%nat.-tuple C R) :
  \rsum_(i in {:m.-tuple C} ) \rsum_(j in {: n.-tuple C})
  F [tuple of (i ++ j)] = \rsum_(p in {: (m + n)%nat.-tuple C}) (F p).


Lemma big_cat_tuple_seq {C:finType} m n (F : seq C R) :
  \rsum_(i in {:m.-tuple C} ) \rsum_(j in {: n.-tuple C}) (F (i ++ j)) =
  \rsum_(p in {: (m + n)%nat.-tuple C}) (F p).

Lemma rsum_rmul_tuple_pmf {C} n k (Q : dist C) :
  (\rsum_(t in {:k.-tuple ('rV[C]_n)}) \big[Rmult/1]_(x <- t) (Q `^ n) x = 1)%R.

Qed.

Local Close Scope tuple_ext_scope.

Lemma not_preimg_Cal_E k n epsilon0 :
  let M := [finType of 'I_k.+1] in
  let PHI' := jtdec P W epsilon0 in
  let Cal_E := @cal_E M n epsilon0 in
   f : encT A M n,
    not_preimg (PHI' f) ord0 =i
    (~: Cal_E f ord0) :|: \bigcup_(m : M | m != ord0) Cal_E f m.

Lemma random_coding_good_code epsilon : 0 epsilon
   (r : CodeRateType),
     epsilon0, epsilon0_condition r epsilon epsilon0
     n, n_condition r epsilon0 n
   M : finType, (0 < #|M|)%nat #|M| = Zabs_nat (Int_part (exp2 (INR n × r)))
  let Jtdec := jtdec P W epsilon0 in
  \rsum_(f : encT A M n) (Wght.d P f × echa(W , mkCode f (Jtdec f)))%R < epsilon.

End random_coding_good_code_existence.

Section channel_coding_theorem.

Variables A B : finType.
Variable W : `Ch_1(A, B).
Variable cap : R.
Hypothesis Hc : capacity W cap.

Channel Coding Theorem (direct part)


Theorem channel_coding (r : CodeRateType) : r < cap
   epsilon, 0 < epsilon
     n M (c : code A B M n), CodeRate c = r echa(W, c) < epsilon.

End channel_coding_theorem.

Check channel_coding.