Infotheo--rocqnavi-sample_68d899e

Files ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Definitions ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Lemmas ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Abbreviations ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Global Index ABCDEFGHIJKLMNOPQRSTUVWXYZ_
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