L (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 |
L (Lemmas)
labels_build_tree_rec [prf, in infotheo.ecc_modern.ldpc_algo_proof]labels_sumprod_down [prf, in infotheo.ecc_modern.ldpc_algo_proof]
labels_sumprod_up [prf, in infotheo.ecc_modern.ldpc_algo_proof]
lambda0 [prf, in infotheo.information_theory.source_coding_fl_converse]
lambda2_epsilon [prf, in infotheo.information_theory.source_coding_fl_direct]
lambda2_gt0 [prf, in infotheo.information_theory.source_coding_fl_direct]
lambda2_lt1 [prf, in infotheo.information_theory.source_coding_fl_direct]
lambda_gt0 [prf, in infotheo.information_theory.source_coding_fl_direct]
largest_stopset_erasures_SP_BEC [prf, in infotheo.ecc_modern.stopping_set]
largest_stopset_is_unique [prf, in infotheo.ecc_modern.stopping_set]
lb_entro_plus_eps [prf, in infotheo.information_theory.source_coding_vl_direct]
Lcode.dimlen [prf, in infotheo.ecc_classic.linearcode]
Lcode.min_dist_prop_old [prf, in infotheo.ecc_classic.linearcode]
Lcode0.aclosed [prf, in infotheo.ecc_classic.linearcode]
Lcode0.mem_poly_rV [prf, in infotheo.ecc_classic.linearcode]
Lcode0.oclosed [prf, in infotheo.ecc_classic.linearcode]
Lcode0.sclosed [prf, in infotheo.ecc_classic.linearcode]
LE [prf, in infotheo.probability.convex]
le_1_EX [prf, in infotheo.information_theory.source_coding_vl_converse]
le_aepbound_n [prf, in infotheo.information_theory.source_coding_vl_direct]
le_centropy [prf, in infotheo.information_theory.entropy]
le_entroPN_logeEX [prf, in infotheo.information_theory.source_coding_vl_converse]
le_entroPN_logeEX' [prf, in infotheo.information_theory.source_coding_vl_converse]
le_eps [prf, in infotheo.information_theory.source_coding_vl_converse]
le_lt_rank_trans [prf, in infotheo.lib.ssr_ext]
le_Pr_setU [prf, in infotheo.probability.proba]
le_rank_asym [prf, in infotheo.lib.ssr_ext]
le_rank_refl [prf, in infotheo.lib.ssr_ext]
le_rank_total [prf, in infotheo.lib.ssr_ext]
le_rank_trans [prf, in infotheo.lib.ssr_ext]
le_sum_all [prf, in infotheo.ecc_modern.degree_profile]
le_Sum_Star [prf, in infotheo.ecc_modern.ldpc_erasure]
lead_coef_F2 [prf, in infotheo.lib.f2]
lel_Bit [prf, in infotheo.ecc_modern.ldpc_erasure]
lel_Blank [prf, in infotheo.ecc_modern.ldpc_erasure]
lel_mat_erase [prf, in infotheo.ecc_modern.stopping_set]
lel_Star [prf, in infotheo.ecc_modern.ldpc_erasure]
lel_trans [prf, in infotheo.ecc_modern.ldpc_erasure]
lel_trans_mat [prf, in infotheo.ecc_modern.ldpc_erasure]
lell [prf, in infotheo.ecc_modern.ldpc_erasure]
lell_mat [prf, in infotheo.ecc_modern.ldpc_erasure]
lelmxStar [prf, in infotheo.ecc_modern.ldpc_erasure]
leoppP [prf, in infotheo.probability.convex]
leq_bigmin [prf, in infotheo.ecc_classic.decoding]
leq_cards_ord [prf, in infotheo.ecc_modern.degree_profile]
leq_lmax [prf, in infotheo.information_theory.kraft]
leq_size_v [prf, in infotheo.lib.euclid]
leq_size_v_incr [prf, in infotheo.lib.euclid]
leq_take [prf, in infotheo.lib.ssr_ext]
leq_var_dist [prf, in infotheo.probability.variation_dist]
leqnmul2 [prf, in infotheo.ecc_classic.reed_solomon]
ler_abs_sqr [prf, in infotheo.lib.ssralg_ext]
ler_log [prf, in infotheo.lib.realType_ln]
ler_Log [prf, in infotheo.lib.realType_ln]
ler_sum_predU [prf, in infotheo.lib.bigop_ext]
ler_suml [prf, in infotheo.lib.bigop_ext]
leR_sumR_eq [prf, in infotheo.lib.realType_ext]
leR_sumR_support [prf, in infotheo.lib.realType_ext]
leR_sumRl [prf, in infotheo.lib.realType_ext]
leR_sumRl_support [prf, in infotheo.lib.realType_ext]
letter_count [prf, in infotheo.ecc_modern.ldpc_erasure]
letter_enumP [prf, in infotheo.ecc_modern.ldpc_erasure]
letter_split [prf, in infotheo.ecc_modern.ldpc_erasure]
letterP [prf, in infotheo.ecc_modern.ldpc_erasure]
lmat_le_decr [prf, in infotheo.ecc_modern.ldpc_erasure]
LmoduleConvex.avgrE [prf, in infotheo.probability.convex]
ln2_ge0 [prf, in infotheo.lib.realType_ln]
ln2_gt0 [prf, in infotheo.lib.realType_ln]
ln2_neq0 [prf, in infotheo.lib.realType_ln]
ln_id_cmp [prf, in infotheo.lib.realType_ln]
ln_id_eq [prf, in infotheo.lib.realType_ln]
Lnt_nonneg [prf, in infotheo.information_theory.source_coding_vl_direct]
log1 [prf, in infotheo.lib.realType_ln]
Log1 [prf, in infotheo.lib.realType_ln]
log16 [prf, in infotheo.lib.realType_ln]
log2 [prf, in infotheo.lib.realType_ln]
log32 [prf, in infotheo.lib.realType_ln]
log4 [prf, in infotheo.lib.realType_ln]
log8 [prf, in infotheo.lib.realType_ln]
log_concave [prf, in infotheo.information_theory.string_entropy]
log_exp1_Rle_0 [prf, in infotheo.lib.realType_ln]
log_exprz [prf, in infotheo.lib.realType_ln]
log_id_cmp [prf, in infotheo.lib.realType_ln]
log_id_diff [prf, in infotheo.probability.divergence]
log_id_eq [prf, in infotheo.probability.divergence]
Log_increasing_le [prf, in infotheo.lib.realType_ln]
log_pow_natmul [prf, in infotheo.lib.realType_ln]
log_powR [prf, in infotheo.lib.realType_ln]
log_prodr_sumr_mlog [prf, in infotheo.lib.realType_ln]
log_sum [prf, in infotheo.probability.log_sum]
log_sum1 [prf, in infotheo.probability.log_sum]
log_sum_inequality_ord_add1 [prf, in infotheo.information_theory.source_coding_vl_converse]
log_sum_inequality_ord_add1' [prf, in infotheo.information_theory.source_coding_vl_converse]
logDiv [prf, in infotheo.lib.realType_ln]
LogDiv [prf, in infotheo.lib.realType_ln]
logexp1E [prf, in infotheo.lib.realType_ln]
logK [prf, in infotheo.lib.realType_ln]
LogK [prf, in infotheo.lib.realType_ln]
logM [prf, in infotheo.lib.realType_ln]
LogM [prf, in infotheo.lib.realType_ln]
logV [prf, in infotheo.lib.realType_ln]
LogV [prf, in infotheo.lib.realType_ln]
logX2 [prf, in infotheo.lib.realType_ln]
lt0cPr [prf, in infotheo.probability.proba]
lt0Pr [prf, in infotheo.probability.proba]
lt_le_rank_trans [prf, in infotheo.lib.ssr_ext]
lt_le_rank_weak [prf, in infotheo.lib.ssr_ext]
lt_ln1Dx [prf, in infotheo.lib.realType_ln]
lt_neq_rank [prf, in infotheo.lib.ssr_ext]
Lt_pos [prf, in infotheo.information_theory.source_coding_vl_direct]
lt_rank_alt [prf, in infotheo.lib.ssr_ext]
ltn_size_q [prf, in infotheo.lib.euclid]
ltn_size_q' [prf, in infotheo.lib.euclid]
ltn_size_r_stop [prf, in infotheo.lib.euclid]
ltn_size_r_stop_r0 [prf, in infotheo.lib.euclid]
ltn_size_v [prf, in infotheo.lib.euclid]
ltnS' [prf, in infotheo.lib.ssralg_ext]
ltPr1 [prf, in infotheo.probability.proba]
ltr0_derive1_decr [prf, in infotheo.lib.realType_ln]
ltr_log [prf, in infotheo.lib.realType_ln]
ltR_sumR [prf, in infotheo.lib.realType_ext]
ltR_sumR_support [prf, in infotheo.lib.realType_ext]
lub_absorbs_conv [prf, in infotheo.probability.necset]
lub_absorbs_convn [prf, in infotheo.probability.necset]
lubAC [prf, in infotheo.probability.necset]
lubACA [prf, in infotheo.probability.necset]
lubCA [prf, in infotheo.probability.necset]
lubDl [prf, in infotheo.probability.necset]
lubKU [prf, in infotheo.probability.necset]
lubKUC [prf, in infotheo.probability.necset]
lubUK [prf, in infotheo.probability.necset]
lubUKC [prf, in infotheo.probability.necset]