A (Global Index)
| 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 |
A
ACode [def, in infotheo.information_theory.kraft]acode [def, in infotheo.information_theory.kraft]
acyclic [def, in infotheo.ecc_modern.subgraph_partition]
acyclic' [def, in infotheo.ecc_modern.subgraph_partition]
acyclic_equiv [prf, in infotheo.ecc_modern.subgraph_partition]
add0pt [prf, in infotheo.probability.convex]
addb_nseq [prf, in infotheo.lib.ssr_ext]
addb_seq [def, in infotheo.lib.ssr_ext]
addb_seq_cat [prf, in infotheo.lib.ssr_ext]
addb_seq_com [prf, in infotheo.lib.ssr_ext]
addb_seq_map [prf, in infotheo.lib.ssr_ext]
addb_tri_ine [prf, in infotheo.lib.ssr_ext]
additive_GF2_of_F2 [def, in infotheo.lib.ssralg_ext]
additive_sbound_f' [prf, in infotheo.ecc_classic.linearcode]
additive_syndrome [prf, in infotheo.ecc_classic.linearcode]
addpt [def, in infotheo.probability.convex]
addpt0 [def, in infotheo.probability.convex]
addpt_scaled_set [prf, in infotheo.probability.convex]
addptA [def, in infotheo.probability.convex]
addptC [def, in infotheo.probability.convex]
addptE [prf, in infotheo.probability.convex]
addr_const_RV [prf, in infotheo.probability.proba]
addrRVE [prf, in infotheo.probability.proba]
aep [file, in infotheo.information_theory.aep]
aep [prf, in infotheo.information_theory.aep]
aep_bound [def, in infotheo.information_theory.aep]
aep_bound_decreasing [prf, in infotheo.information_theory.aep]
aep_bound_ge0 [prf, in infotheo.information_theory.aep]
aep_sigma2 [def, in infotheo.information_theory.aep]
aep_sigma2_ge0 [prf, in infotheo.information_theory.aep]
aep_sigma2E [prf, in infotheo.information_theory.aep]
Affine [abbrev, in infotheo.probability.convex]
Affine [mod, in infotheo.probability.convex]
affine [def, in infotheo.probability.convex]
Affine.axioms_ [rec, in infotheo.probability.convex]
Affine.class [proj, in infotheo.probability.convex]
Affine.clone [abbrev, in infotheo.probability.convex]
Affine.convex_isAffine_mixin [proj, in infotheo.probability.convex]
Affine.copy [abbrev, in infotheo.probability.convex]
Affine.Exports [mod, in infotheo.probability.convex]
Affine.on [abbrev, in infotheo.probability.convex]
Affine.on_ [abbrev, in infotheo.probability.convex]
Affine.pack_ [def, in infotheo.probability.convex]
Affine.phant_clone [def, in infotheo.probability.convex]
Affine.phant_on_ [def, in infotheo.probability.convex]
Affine.sort [proj, in infotheo.probability.convex]
Affine.type [rec, in infotheo.probability.convex]
affine_conv [def, in infotheo.probability.convex]
affine_function_Sum [prf, in infotheo.probability.convex_stone]
affine_functionP [prf, in infotheo.probability.convex]
affine_image_conv_set [prf, in infotheo.probability.necset]
affine_map_scaled [prf, in infotheo.probability.convex]
affine_S1 [prf, in infotheo.probability.convex]
AffineElpiOperations [mod, in infotheo.probability.convex]
all_mxStar [prf, in infotheo.ecc_modern.ldpc_erasure]
all_starblank_colFNext_mxSum_stopset [prf, in infotheo.ecc_modern.stopping_set]
all_starblank_colFNextD1_mxSum_stopset [prf, in infotheo.ecc_modern.stopping_set]
all_starletter_iSP_BEC0 [prf, in infotheo.ecc_modern.stopping_set]
all_starletter_iSP_BEC0D1 [prf, in infotheo.ecc_modern.stopping_set]
all_starletter_iSP_BEC0S [prf, in infotheo.ecc_modern.stopping_set]
all_stopsets_in_erasures_in_SP_BEC [prf, in infotheo.ecc_modern.stopping_set]
alpha [def, in infotheo.ecc_modern.ldpc_algo]
alpha [def, in infotheo.ecc_modern.ldpc]
alpha0x [prf, in infotheo.ecc_modern.ldpc_algo]
alpha_beta [def, in infotheo.ecc_modern.ldpc_algo]
alpha_beta_tag_of_id [prf, in infotheo.ecc_modern.ldpc_algo_proof]
alpha_def [prf, in infotheo.ecc_modern.ldpc_algo_proof]
alpha_def_sub [prf, in infotheo.ecc_modern.ldpc_algo_proof]
alpha_fun [def, in infotheo.ecc_modern.ldpc]
alpha_inva [prf, in infotheo.ecc_modern.ldpc]
alpha_map [prf, in infotheo.ecc_modern.ldpc_algo_proof]
alpha_one_successor [prf, in infotheo.ecc_modern.ldpc]
alpha_op [def, in infotheo.ecc_modern.ldpc_algo]
alpha_two_successors [prf, in infotheo.ecc_modern.ldpc]
alphaA [prf, in infotheo.ecc_modern.ldpc_algo]
alphaC [prf, in infotheo.ecc_modern.ldpc_algo]
alt_hamming_err [def, in infotheo.ecc_classic.hamming_code]
alt_hamming_err_ub [prf, in infotheo.ecc_classic.hamming_code]
alternant [file, in infotheo.ecc_classic.alternant]
alternant_code [def, in infotheo.ecc_classic.alternant]
alternant_PCM [def, in infotheo.ecc_classic.alternant]
ambient_dist [def, in infotheo.probability.proba]
and_curry [prf, in infotheo.robust.robustmean]
Anot0 [prf, in infotheo.information_theory.success_decode_bound]
another_Fgraph_injective [prf, in infotheo.ecc_modern.tanner_partition]
apply_le_HN_logE_loge [prf, in infotheo.information_theory.source_coding_vl_converse]
apply_max_HPN [prf, in infotheo.information_theory.source_coding_vl_converse]
apply_seq [def, in infotheo.ecc_modern.ldpc_algo]
apply_seqs_but1 [prf, in infotheo.ecc_modern.ldpc_algo_proof]
approx [def, in infotheo.ecc_modern.ldpc_erasure]
approx_BEC_input [def, in infotheo.ecc_modern.ldpc_erasure]
approx_BEC_input_mxStar [prf, in infotheo.ecc_modern.ldpc_erasure]
approx_mxStar [prf, in infotheo.ecc_modern.ldpc_erasure]
approx_mxSumProd [prf, in infotheo.ecc_modern.ldpc_erasure]
arg_rmax2 [prf, in infotheo.information_theory.success_decode_bound]
arg_tau_max [def, in infotheo.robust.weightedmean]
ary_of_nat [def, in infotheo.information_theory.kraft]
ary_of_nat' [def, in infotheo.information_theory.kraft]
ary_of_nat0 [prf, in infotheo.information_theory.kraft]
ary_of_nat_head [prf, in infotheo.information_theory.kraft]
ary_of_nat_head' [prf, in infotheo.information_theory.kraft]
ary_of_nat_unfold [prf, in infotheo.information_theory.kraft]
ary_of_natK [prf, in infotheo.information_theory.kraft]
asboolTE [prf, in infotheo.lib.realType_ext]
average [def, in infotheo.information_theory.shannon_fano]
avg_dom_pair [def, in infotheo.information_theory.entropy_convex]
avgnr [def, in infotheo.probability.convex]
avgnr_add [prf, in infotheo.probability.convex]
avgnrE [prf, in infotheo.probability.convex]
avgr_addD [prf, in infotheo.probability.convex]
avgr_oppD [prf, in infotheo.probability.convex]
avgr_scalerDl [prf, in infotheo.probability.convex]
avgr_scalerDr [prf, in infotheo.probability.convex]
axbary [def, in infotheo.probability.convex_equiv]
axproj [def, in infotheo.probability.convex_equiv]