# Library Infotheo.source_coding_fl_direct

Require Import Reals Fourier.
Require Import Reals_ext ssr_ext ssralg_ext Rssr log2 natbin Rbigop proba entropy aep.
Require Import typ_seq source_code.

Set Implicit Arguments.
Import Prenex Implicits.

Local Open Scope ring_scope.

Section encoder_and_decoder.

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

Variable S : {set 'rV[A]_k.+1}.

Definition f : encT A 'rV_n k.+1 := fun x
if x \in S then
let i := seq.index x (enum S) in row_of_tuple (Tuple (size_nat2bin i.+1 n))
else
\row_(j < n) false.

Variable def : 'rV[A]_k.+1.
Hypothesis Hdef : def \in S.

Definition phi : decT A 'rV_n k.+1 := fun x
let i := tuple2N (tuple_of_row x) in
if i is N0 then def else
if (i.-1 < #| S |)%nat then nth def (enum S) i.-1 else def.

Lemma phi_f i : phi (f i) = i i \in S.

Hypothesis HS : (#| S | < expn 2 n)%nat.

Lemma f_phi i : i \in S phi (f i) = i.

End encoder_and_decoder.

Lemma SrcDirectBound' d D : { k | D INR (k × (d.+1)) }.

Lemma SrcDirectBound d D : { k | D INR ((k.+1) × (d.+1)) }.

Local Open Scope source_code_scope.
Local Open Scope entropy_scope.
Local Open Scope reals_ext_scope.

Section source_coding_direct'.

Variable A : finType.
Variable P : dist A.
Variables num den : nat.

Let r := (INR num / INR den.+1)%R.

Hypothesis Hr : `H P < r.
Variable epsilon : R.
Hypothesis Hepsilon : 0 < epsilon < 1.

Definition lambda := min(r - `H P, epsilon).

Definition delta := max(aep_bound P (lambda / 2), 2 / lambda).

Let k' := sval (SrcDirectBound den delta).

Definition k := (k'.+1 × den.+1)%nat.

Definition n := (k'.+1 × num)%nat.

Lemma lambda0 : 0 < lambda.

Lemma halflambdaepsilon : lambda / 2 epsilon.

Lemma halflambda0 : 0 < lambda / 2.

Lemma halflambda1 : lambda / 2 < 1.

Lemma lambdainv2 : 0 < 2 / lambda.

Lemma Hlambdar : `H P + lambda r.

Local Open Scope proba_scope.
Local Open Scope typ_seq_scope.

Theorem source_coding' : sc : scode_fl A k n,
SrcRate sc = r esrc(P , sc) epsilon.

End source_coding_direct'.

Section source_coding_direct.

Variable A : finType.
Variable P : dist A.

# Source coding theorem (direct part)

Theorem source_coding_direct : epsilon, 0 < epsilon < 1
r : Qplus, `H P < r
k n (sc : scode_fl A k n), SrcRate sc = r esrc(P , sc) epsilon.

End source_coding_direct.

Check source_coding_direct.