Module infotheo.information_theory.source_code
From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.From mathcomp Require Import Rstruct reals.
Require Import realType_ln fdist proba.
# Definition of a source code
```
encT, decT == types for the source encoder and source decoder
scode_fl == definition of a fixed-length source code
esrc( P , sc ) == error rate of the source code sc
```
Set Implicit Arguments.
Set SsrOldRewriteGoalsOrder.
Unset Strict Implicit.
Import Prenex Implicits.
From mathcomp Require Import normedtype.
Import numFieldNormedType.Exports.
Declare Scope source_code_scope.
Section scode_definition.
Variables (A : finType) (B : Type) (k : nat).
Definition
encT
:= 'rV[A]_k -> B.encT not a defined object.
Definition
decT
:= B -> 'rV[A]_k.decT not a defined object.
Record scode := mkScode { enc : encT ; dec : decT }.
End scode_definition.
Local Open Scope fdist_scope.
Local Open Scope proba_scope.
Section scode_vl_definition.
Variables (R : realType) (A : finType) (k n : nat).
Definition
scode_vl
:= scode A (seq bool) k.scode_vl not a defined object.
Variables (P : R.-fdist A) (f : {RV (P `^ n) -> seq bool}).
Definition
E_leng_cw
:= `E (((fun x => x%:R : R)%R \o size) `o f).E_leng_cw not a defined object.
End scode_vl_definition.
Arguments E_leng_cw {R A n} _.
Section scode_fl_definition.
Variables (R : realType) (A : finType) (k n : nat).
Definition
scode_fl
:= scode A 'rV[bool]_n k.scode_fl not a defined object.
Definition
SrcRate
(sc : scode_fl) : R := (n%:R / k%:R)%R.SrcRate not a defined object.
End scode_fl_definition.
Section code_error_rate.
Variables (R : realType) (A : finType) (B : Type) (P : R.-fdist A).
Variables (k : nat) (sc : scode A B k).
Definition
SrcErrRate
:= Pr (P `^ k) [set ta | dec sc (enc sc ta) != ta].SrcErrRate not a defined object.
End code_error_rate.
Notation "esrc( P , sc )" := (SrcErrRate P sc) (at level 40) : source_code_scope.
Section extension.
Variables (A : finType) (B : Type).
Definition
extension
(f : A -> seq B) : seq A -> seq B :=extension not a defined object.
fun a => flatten (map f a).
Definition
uniquely_decodable
(f : A -> seq B):= injective (extension f).uniquely_decodable not a defined object.
Lemma uniq_dec_inj (f : A -> seq B) : uniquely_decodable f -> injective f.
Proof.
End extension.