A (Lemmas)
| 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 (Lemmas)
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_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_sbound_f' [prf, in infotheo.ecc_classic.linearcode]
additive_syndrome [prf, in infotheo.ecc_classic.linearcode]
addpt_scaled_set [prf, 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 [prf, 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_ge0 [prf, in infotheo.information_theory.aep]
aep_sigma2E [prf, in infotheo.information_theory.aep]
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]
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]
alpha0x [prf, 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_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_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_ub [prf, in infotheo.ecc_classic.hamming_code]
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_seqs_but1 [prf, in infotheo.ecc_modern.ldpc_algo_proof]
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]
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]
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]