Library Infotheo.channel_coding_converse

Require Import Reals Fourier.
Require Import Reals_ext ssr_ext ssralg_ext log2 ln_facts Rssr Rbigop arg_rmax.
Require Import num_occ proba entropy types jtypes divergence conditional_divergence.
Require Import error_exponent channel_code channel success_decode_bound.

Set Implicit Arguments.
Import Prenex Implicits.

Local Open Scope channel_code_scope.
Local Open Scope channel_scope.
Local Open Scope entropy_scope.
Local Open Scope tuple_ext_scope.
Local Open Scope reals_ext_scope.
Local Open Scope proba_scope.
Local Open Scope types_scope.

Section channel_coding_converse_intermediate_lemma.

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

Variable minRate : R.
Hypothesis HminRate : minRate > cap.

Let Anot0 : (0 < #|A|)%nat.

Let Bnot0 : (0 < #|B|)%nat.

Lemma channel_coding_converse_gen : Delta, 0 < Delta n',
  let n := n'.+1 in (M : finType) (c : code A B M n), (0 < #|M|)%nat
    minRate CodeRate c
      scha(W, c) INR (n.+1)^(#|A| + #|A| × #|B|) × exp2 (- INR n × Delta).

End channel_coding_converse_intermediate_lemma.

Section channel_coding_converse.

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

Variable epsilon : R.
Hypothesis eps_gt0 : 0 < epsilon.

Variable minRate : R.
Hypothesis minRate_cap : minRate > cap.

Converse of the Channel Coding Theorem

Theorem channel_coding_converse : n0,
   n M (c : code A B M n),
    (0 < #|M|)%nat n0 < INR n minRate CodeRate c scha(W, c) < epsilon.

End channel_coding_converse.

Check channel_coding_converse.