Files
infotheo
ecc_classic
alternant
bch
cyclic_code
decoding
grs
hamming_code
linearcode
mceliece
poly_decoding
reed_solomon
repcode
ecc_modern
checksum
degree_profile
ldpc
ldpc_algo
ldpc_algo_proof
ldpc_erasure
max_subset
stopping_set
subgraph_partition
summary
summary_tanner
tanner
tanner_partition
information_theory
aep
binary_symmetric_channel
channel
channel_code
channel_coding_converse
channel_coding_direct
conditional_divergence
entropy
entropy_convex
erasure_channel
error_exponent
joint_typ_seq
jtypes
kraft
pproba
shannon_fano
source_code
source_coding_fl_converse
source_coding_fl_direct
source_coding_vl_converse
source_coding_vl_direct
string_entropy
success_decode_bound
typ_seq
types
lib
bigop_ext
binary_entropy_function
classical_sets_ext
coqRE
derive_ext
dft
euclid
f2
hamming
natbin
num_occ
poly_ext
realType_ext
realType_ln
ssr_ext
ssralg_ext
probability
bayes
convex
convex_equiv
convex_stone
divergence
fdist
fsdist
graphoid
jensen
jfdist_cond
log_sum
necset
partition_inequality
pinsker
proba
variation_dist
robust
robustmean
weightedmean
toy_examples
conditional_entropy
expected_value_variance
expected_value_variance_ordn
expected_value_variance_tuple
Infotheo--rocqnavi-sample_68d899e
Files
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
Definitions
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
Lemmas
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
Abbreviations
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
Global Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
Notations
Clickable Dependency Graph of Files
depend
cluster_lib
lib
cluster_probability
probability
cluster_information_theory
information_theory
cluster_ecc_classic
ecc_classic
cluster_ecc_modern
ecc_modern
cluster_robust
robust
cluster_toy_examples
toy_examples
lib.coqRE
coqRE
robust.weightedmean
weightedmean
lib.coqRE->robust.weightedmean
lib.realType_ext
realType_ext
lib.derive_ext
derive_ext
lib.realType_ext->lib.derive_ext
probability.fdist
fdist
lib.realType_ext->probability.fdist
lib.realType_ln
realType_ln
lib.binary_entropy_function
binary_entropy_function
lib.realType_ln->lib.binary_entropy_function
probability.proba
proba
lib.realType_ln->probability.proba
probability.convex
convex
lib.realType_ln->probability.convex
probability.log_sum
log_sum
lib.realType_ln->probability.log_sum
lib.derive_ext->lib.realType_ln
lib.ssr_ext
ssr_ext
lib.ssralg_ext
ssralg_ext
lib.ssr_ext->lib.ssralg_ext
lib.num_occ
num_occ
lib.ssr_ext->lib.num_occ
information_theory.kraft
kraft
lib.ssr_ext->information_theory.kraft
ecc_modern.subgraph_partition
subgraph_partition
lib.ssr_ext->ecc_modern.subgraph_partition
lib.f2
f2
lib.f2->lib.ssralg_ext
lib.f2->lib.num_occ
lib.ssralg_ext->lib.derive_ext
lib.bigop_ext
bigop_ext
lib.ssralg_ext->lib.bigop_ext
lib.natbin
natbin
lib.ssralg_ext->lib.natbin
lib.poly_ext
poly_ext
lib.ssralg_ext->lib.poly_ext
ecc_modern.summary
summary
lib.ssralg_ext->ecc_modern.summary
lib.hamming
hamming
lib.bigop_ext->lib.hamming
lib.bigop_ext->probability.fdist
lib.bigop_ext->probability.log_sum
ecc_modern.tanner
tanner
lib.bigop_ext->ecc_modern.tanner
lib.natbin->lib.hamming
information_theory.source_coding_fl_direct
source_coding_fl_direct
lib.natbin->information_theory.source_coding_fl_direct
information_theory.source_coding_vl_direct
source_coding_vl_direct
lib.natbin->information_theory.source_coding_vl_direct
information_theory.entropy
entropy
lib.binary_entropy_function->information_theory.entropy
lib.num_occ->lib.hamming
information_theory.types
types
lib.num_occ->information_theory.types
information_theory.string_entropy
string_entropy
lib.num_occ->information_theory.string_entropy
lib.dft
dft
lib.hamming->lib.dft
information_theory.erasure_channel
erasure_channel
lib.hamming->information_theory.erasure_channel
information_theory.binary_symmetric_channel
binary_symmetric_channel
lib.hamming->information_theory.binary_symmetric_channel
ecc_classic.linearcode
linearcode
lib.poly_ext->ecc_classic.linearcode
lib.euclid
euclid
ecc_classic.reed_solomon
reed_solomon
lib.euclid->ecc_classic.reed_solomon
ecc_classic.bch
bch
lib.euclid->ecc_classic.bch
ecc_classic.cyclic_code
cyclic_code
lib.dft->ecc_classic.cyclic_code
lib.classical_sets_ext
classical_sets_ext
probability.necset
necset
lib.classical_sets_ext->probability.necset
probability.fdist->probability.proba
probability.fdist->probability.convex
probability.variation_dist
variation_dist
probability.fdist->probability.variation_dist
ecc_modern.degree_profile
degree_profile
probability.fdist->ecc_modern.degree_profile
probability.jfdist_cond
jfdist_cond
probability.proba->probability.jfdist_cond
probability.jensen
jensen
probability.proba->probability.jensen
probability.divergence
divergence
probability.proba->probability.divergence
probability.bayes
bayes
probability.proba->probability.bayes
information_theory.source_code
source_code
probability.proba->information_theory.source_code
robust.robustmean
robustmean
probability.proba->robust.robustmean
toy_examples.expected_value_variance
expected_value_variance
probability.proba->toy_examples.expected_value_variance
toy_examples.expected_value_variance_ordn
expected_value_variance_ordn
probability.proba->toy_examples.expected_value_variance_ordn
toy_examples.expected_value_variance_tuple
expected_value_variance_tuple
probability.proba->toy_examples.expected_value_variance_tuple
probability.fsdist
fsdist
probability.convex_equiv
convex_equiv
probability.fsdist->probability.convex_equiv
probability.fsdist->probability.necset
probability.convex->probability.fsdist
probability.convex_stone
convex_stone
probability.convex->probability.convex_stone
probability.convex->probability.jensen
information_theory.entropy_convex
entropy_convex
probability.convex->information_theory.entropy_convex
probability.jfdist_cond->probability.convex_equiv
probability.graphoid
graphoid
probability.jfdist_cond->probability.graphoid
probability.jfdist_cond->information_theory.entropy
probability.jensen->information_theory.string_entropy
probability.partition_inequality
partition_inequality
probability.divergence->probability.partition_inequality
probability.divergence->information_theory.entropy
probability.variation_dist->probability.partition_inequality
probability.log_sum->probability.partition_inequality
probability.log_sum->information_theory.entropy_convex
information_theory.source_coding_vl_converse
source_coding_vl_converse
probability.log_sum->information_theory.source_coding_vl_converse
probability.pinsker
pinsker
probability.partition_inequality->probability.pinsker
information_theory.error_exponent
error_exponent
probability.pinsker->information_theory.error_exponent
information_theory.source_code->information_theory.source_coding_fl_direct
information_theory.source_coding_fl_converse
source_coding_fl_converse
information_theory.source_code->information_theory.source_coding_fl_converse
information_theory.source_code->information_theory.source_coding_vl_direct
information_theory.source_code->information_theory.source_coding_vl_converse
information_theory.channel
channel
information_theory.entropy->information_theory.channel
information_theory.aep
aep
information_theory.entropy->information_theory.aep
information_theory.shannon_fano
shannon_fano
information_theory.entropy->information_theory.shannon_fano
information_theory.entropy->information_theory.string_entropy
information_theory.entropy->information_theory.entropy_convex
information_theory.entropy->information_theory.source_coding_vl_converse
toy_examples.conditional_entropy
conditional_entropy
information_theory.entropy->toy_examples.conditional_entropy
information_theory.pproba
pproba
information_theory.channel->information_theory.pproba
information_theory.channel_code
channel_code
information_theory.channel->information_theory.channel_code
information_theory.joint_typ_seq
joint_typ_seq
information_theory.channel->information_theory.joint_typ_seq
information_theory.pproba->information_theory.binary_symmetric_channel
information_theory.channel_code->information_theory.erasure_channel
information_theory.channel_code->information_theory.binary_symmetric_channel
information_theory.channel_code->information_theory.types
information_theory.channel_coding_direct
channel_coding_direct
information_theory.channel_code->information_theory.channel_coding_direct
ecc_classic.decoding
decoding
information_theory.binary_symmetric_channel->ecc_classic.decoding
information_theory.typ_seq
typ_seq
information_theory.aep->information_theory.typ_seq
information_theory.typ_seq->information_theory.types
information_theory.typ_seq->information_theory.source_coding_fl_direct
information_theory.typ_seq->information_theory.source_coding_fl_converse
information_theory.typ_seq->information_theory.joint_typ_seq
information_theory.typ_seq->information_theory.source_coding_vl_direct
information_theory.jtypes
jtypes
information_theory.types->information_theory.jtypes
information_theory.conditional_divergence
conditional_divergence
information_theory.jtypes->information_theory.conditional_divergence
information_theory.conditional_divergence->information_theory.error_exponent
information_theory.success_decode_bound
success_decode_bound
information_theory.conditional_divergence->information_theory.success_decode_bound
information_theory.joint_typ_seq->information_theory.channel_coding_direct
information_theory.channel_coding_converse
channel_coding_converse
information_theory.error_exponent->information_theory.channel_coding_converse
information_theory.success_decode_bound->information_theory.channel_coding_converse
information_theory.kraft->information_theory.shannon_fano
ecc_classic.mceliece
mceliece
ecc_classic.linearcode->ecc_classic.mceliece
ecc_classic.linearcode->ecc_classic.cyclic_code
ecc_classic.hamming_code
hamming_code
ecc_classic.linearcode->ecc_classic.hamming_code
ecc_classic.repcode
repcode
ecc_classic.linearcode->ecc_classic.repcode
ecc_modern.checksum
checksum
ecc_classic.linearcode->ecc_modern.checksum
ecc_modern.ldpc_erasure
ldpc_erasure
ecc_classic.linearcode->ecc_modern.ldpc_erasure
ecc_classic.decoding->ecc_classic.linearcode
ecc_classic.poly_decoding
poly_decoding
ecc_classic.cyclic_code->ecc_classic.poly_decoding
ecc_classic.grs
grs
ecc_classic.poly_decoding->ecc_classic.grs
ecc_classic.grs->ecc_classic.reed_solomon
ecc_classic.grs->ecc_classic.bch
ecc_classic.alternant
alternant
ecc_classic.bch->ecc_classic.alternant
ecc_modern.subgraph_partition->ecc_modern.tanner
ecc_modern.tanner_partition
tanner_partition
ecc_modern.tanner->ecc_modern.tanner_partition
ecc_modern.tanner->ecc_modern.checksum
ecc_modern.tanner->ecc_modern.ldpc_erasure
ecc_modern.tanner->ecc_modern.degree_profile
ecc_modern.summary_tanner
summary_tanner
ecc_modern.tanner_partition->ecc_modern.summary_tanner
ecc_modern.summary->ecc_modern.summary_tanner
ecc_modern.checksum->ecc_modern.summary_tanner
ecc_modern.ldpc
ldpc
ecc_modern.summary_tanner->ecc_modern.ldpc
ecc_modern.ldpc_algo
ldpc_algo
ecc_modern.ldpc->ecc_modern.ldpc_algo
ecc_modern.ldpc_algo_proof
ldpc_algo_proof
ecc_modern.ldpc_algo->ecc_modern.ldpc_algo_proof
ecc_modern.stopping_set
stopping_set
ecc_modern.ldpc_erasure->ecc_modern.stopping_set
ecc_modern.max_subset
max_subset
ecc_modern.max_subset->ecc_modern.stopping_set
robust.robustmean->robust.weightedmean
View raw SVG