Skip to content

palmskog/infotheo

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

298 Commits
.gitignore
.gitignore
 
 
README.org
README.org
 
 
Ranalysis_ext.v
Ranalysis_ext.v
 
 
Rbigop.v
Rbigop.v
 
 
Reals_ext.v
Reals_ext.v
 
 
_CoqProject
_CoqProject
 
 
aep.v
aep.v
 
 
alternant.v
alternant.v
 
 
arg_rmax.v
arg_rmax.v
 
 
bch.v
bch.v
 
 
bigop_ext.v
bigop_ext.v
 
 
binary_entropy_function.v
binary_entropy_function.v
 
 
binary_symmetric_channel.v
binary_symmetric_channel.v
 
 
channel.v
channel.v
 
 
channel_code.v
channel_code.v
 
 
channel_coding_converse.v
channel_coding_converse.v
 
 
channel_coding_direct.v
channel_coding_direct.v
 
 
chap2.v
chap2.v
 
 
checksum.v
checksum.v
 
 
cinde.v
cinde.v
 
 
conditional_divergence.v
conditional_divergence.v
 
 
convex.v
convex.v
 
 
convex_dist.v
convex_dist.v
 
 
convex_stone.v
convex_stone.v
 
 
cproba.v
cproba.v
 
 
cyclic_code.v
cyclic_code.v
 
 
decoding.v
decoding.v
 
 
degree_profile.v
degree_profile.v
 
 
dft.v
dft.v
 
 
dist.v
dist.v
 
 
divergence.v
divergence.v
 
 
entropy.v
entropy.v
 
 
erasure_channel.v
erasure_channel.v
 
 
error_exponent.v
error_exponent.v
 
 
euclid.v
euclid.v
 
 
f2.v
f2.v
 
 
grs.v
grs.v
 
 
hamming.v
hamming.v
 
 
hamming_code.v
hamming_code.v
 
 
infotheo_authors.txt
infotheo_authors.txt
 
 
jensen.v
jensen.v
 
 
joint_typ_seq.v
joint_typ_seq.v
 
 
jtypes.v
jtypes.v
 
 
kraft.v
kraft.v
 
 
ldpc.v
ldpc.v
 
 
ldpc_algo.v
ldpc_algo.v
 
 
ldpc_algo_proof.v
ldpc_algo_proof.v
 
 
ldpc_erasure.v
ldpc_erasure.v
 
 
linearcode.v
linearcode.v
 
 
ln_facts.v
ln_facts.v
 
 
log_sum.v
log_sum.v
 
 
logb.v
logb.v
 
 
max_subset.v
max_subset.v
 
 
mceliece.v
mceliece.v
 
 
natbin.v
natbin.v
 
 
num_occ.v
num_occ.v
 
 
partition_inequality.v
partition_inequality.v
 
 
pinsker.v
pinsker.v
 
 
pinsker_function.v
pinsker_function.v
 
 
poly_decoding.v
poly_decoding.v
 
 
poly_ext.v
poly_ext.v
 
 
pproba.v
pproba.v
 
 
proba.v
proba.v
 
 
proba_ssrnum.v
proba_ssrnum.v
 
 
reed_solomon.v
reed_solomon.v
 
 
repcode.v
repcode.v
 
 
shannon_fano.v
shannon_fano.v
 
 
source_code.v
source_code.v
 
 
source_coding_fl_converse.v
source_coding_fl_converse.v
 
 
source_coding_fl_direct.v
source_coding_fl_direct.v
 
 
ssrR.v
ssrR.v
 
 
ssrZ.v
ssrZ.v
 
 
ssr_ext.v
ssr_ext.v
 
 
ssralg_ext.v
ssralg_ext.v
 
 
stopping_set.v
stopping_set.v
 
 
string_entropy.v
string_entropy.v
 
 
subgraph_partition.v
subgraph_partition.v
 
 
success_decode_bound.v
success_decode_bound.v
 
 
summary.v
summary.v
 
 
summary_tanner.v
summary_tanner.v
 
 
tanner.v
tanner.v
 
 
tanner_partition.v
tanner_partition.v
 
 
typ_seq.v
typ_seq.v
 
 
types.v
types.v
 
 
vandermonde.v
vandermonde.v
 
 
variation_dist.v
variation_dist.v
 
 

Repository files navigation

infotheo

This is a Coq formalization of information theory and linear error-correcting codes.

Requirements

All versions available from opam.

See branch mathcomp-1.9.0 [2019-05-30 Thu] for a version compatible with mathcomp 1.9.0, analysis 0.2.2, finmap 1.2.1.

Installation

  1. coq_makefile -f _CoqProject -o Makefile
  2. make
  3. make install (if needed in another project)

License

GNU GPLv3

Authors

See infotheo_authors.txt

References

There are a few papers available here (information theory) and here (error-correcting codes) that provide explanations and references.

About

No description, website, or topics provided.

Resources

Readme
Activity

Stars

0 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages

  • Rocq Prover 100.0%