# Library Infotheo.source_coding_fl_converse

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

Set Implicit Arguments.
Import Prenex Implicits.

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

Section source_coding_converse'.

Variable A : finType.
Variable P : dist A.
Variables num den : nat.
Let r := INR num / INR den.+1.
Hypothesis Hr : 0 < r < `H P.

Variable n : nat.
Variable k : nat.
Variable sc : scode_fl A k.+1 n.
Hypothesis r_sc : r = SrcRate sc.

Variable epsilon : R.
Hypothesis Hepsilon : 0 < epsilon < 1.

Notation "'max(' x ',' y ')'" := (Rmax x y) : reals_ext_scope.

Definition lambda := min((1 - epsilon) / 2, (`H P - r) / 2).
Definition delta := min((`H P - r) / 2, lambda / 2).

Definition SrcConverseBound := max(max(
aep_bound P delta, - ((log delta) / (`H P - r - delta))), INR n / r).

Hypothesis Hk : SrcConverseBound INR k.+1.

Lemma Hr1 : 0 < (`H P - r) / 2.

Lemma Hepsilon1 : 0 < (1 - epsilon) / 2.

Lemma Hlambda : 0 < lambda.

Lemma Hdelta : 0 < delta.

Definition e0 := `H P - r.

Lemma e0_delta : e0 delta.

Definition no_failure := [set x : 'rV[A]_k.+1 | dec sc (enc sc x) == x].

Lemma no_failure_sup : INR #| no_failure | exp2 (INR k.+1 × (`H P - e0)).

Local Open Scope proba_scope.

Lemma step1 : (1 - esrc(P , sc)) = \rsum_(x in no_failure) P `^ k.+1 x.

Local Open Scope typ_seq_scope.

Lemma step2 : 1 - (esrc(P , sc)) =
\rsum_(x in 'rV[A]_k.+1 | x \in no_failure :&: ~: `TS P k.+1 delta) P `^ k.+1 x +
\rsum_(x in 'rV[A]_k.+1 | x \in no_failure :&: `TS P k.+1 delta) P `^ k.+1 x.

Lemma step3 : 1 - (esrc(P , sc))
\rsum_(x in 'rV[A]_k.+1 | x \in ~: `TS P k.+1 delta) P `^ k.+1 x +
\rsum_(x in 'rV[A]_k.+1 | x \in no_failure :&: `TS P k.+1 delta) P `^ k.+1 x.

Lemma step4 : 1 - (esrc(P , sc)) delta +
INR #| no_failure :&: `TS P k.+1 delta| × exp2 (- INR k.+1 × (`H P - delta)).

Lemma step5 : 1 - (esrc(P , sc)) delta + exp2 (- INR k.+1 × (e0 - delta)).

Lemma step6 : (esrc(P , sc)) 1 - 2 × delta.

Theorem source_coding_converse' : esrc(P , sc) epsilon.

End source_coding_converse'.

Section source_coding_converse.

Variable A : finType.
Variable P : dist A.

# Source coding theorem (converse part)

Theorem source_coding_converse : epsilon, 0 < epsilon < 1
r : Qplus, 0 < r < `H P
n k (sc : scode_fl A k.+1 n),
SrcRate sc = r
SrcConverseBound P (num r) (den r) n epsilon INR k.+1
esrc(P , sc) epsilon.

End source_coding_converse.

Check source_coding_converse.