L (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

L

L [def, in infotheo.probability.convex]
L_not_typ [def, in infotheo.information_theory.source_coding_vl_direct]
L_typ [def, in infotheo.information_theory.source_coding_vl_direct]
labels [def, in infotheo.ecc_modern.ldpc_algo]
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]
lambda [def, in infotheo.information_theory.source_coding_fl_direct]
lambda [def, in infotheo.information_theory.source_coding_fl_converse]
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]
Lambda_of_L [def, in infotheo.ecc_modern.degree_profile]
largest_stopset [def, in infotheo.ecc_modern.stopping_set]
largest_stopset_erasures_SP_BEC [prf, in infotheo.ecc_modern.stopping_set]
largest_stopset_is_unique [prf, in infotheo.ecc_modern.stopping_set]
lastE [def, in infotheo.ecc_modern.ldpc_algo_proof]
lb_entro_plus_eps [prf, in infotheo.information_theory.source_coding_vl_direct]
Lcode [mod, in infotheo.ecc_classic.linearcode]
lcode [def, in infotheo.ecc_classic.hamming_code]
Lcode.compatible [proj, in infotheo.ecc_classic.linearcode]
Lcode.dec [proj, in infotheo.ecc_classic.linearcode]
Lcode.dimlen [prf, in infotheo.ecc_classic.linearcode]
Lcode.enc [proj, in infotheo.ecc_classic.linearcode]
Lcode.lcode0_of [proj, in infotheo.ecc_classic.linearcode]
Lcode.lcode_coercion [def, in infotheo.ecc_classic.linearcode]
Lcode.min_dist_prop_old [prf, in infotheo.ecc_classic.linearcode]
Lcode.t [rec, in infotheo.ecc_classic.linearcode]
Lcode0 [mod, in infotheo.ecc_classic.linearcode]
Lcode0.aclosed [prf, in infotheo.ecc_classic.linearcode]
Lcode0.mem_poly_rV [prf, in infotheo.ecc_classic.linearcode]
Lcode0.not_empty [def, in infotheo.ecc_classic.linearcode]
Lcode0.oclosed [prf, in infotheo.ecc_classic.linearcode]
Lcode0.sclosed [prf, in infotheo.ecc_classic.linearcode]
Lcode0.t [def, in infotheo.ecc_classic.linearcode]
lcode_coercion [def, in infotheo.ecc_classic.linearcode]
ldpc [file, in infotheo.ecc_modern.ldpc]
ldpc_algo [file, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_alpha_op__canonical__Monoid_ComLaw [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_alpha_op__canonical__Monoid_Law [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_alpha_op__canonical__SemiGroup_ComLaw [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_alpha_op__canonical__SemiGroup_Law [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_beta_op__canonical__Monoid_ComLaw [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_beta_op__canonical__Monoid_Law [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_beta_op__canonical__SemiGroup_ComLaw [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_beta_op__canonical__SemiGroup_Law [def, in infotheo.ecc_modern.ldpc_algo]
ldpc_algo_kind__canonical__eqtype_Equality [def, in infotheo.ecc_modern.ldpc_algo_proof]
ldpc_algo_proof [file, in infotheo.ecc_modern.ldpc_algo_proof]
ldpc_algo_tag__canonical__eqtype_Equality [def, in infotheo.ecc_modern.ldpc_algo_proof]
ldpc_algo_tn_tree__canonical__eqtype_Equality [def, in infotheo.ecc_modern.ldpc_algo_proof]
ldpc_erasure [file, in infotheo.ecc_modern.ldpc_erasure]
ldpc_erasure_letter__canonical__choice_Choice [def, in infotheo.ecc_modern.ldpc_erasure]
ldpc_erasure_letter__canonical__choice_Countable [def, in infotheo.ecc_modern.ldpc_erasure]
ldpc_erasure_letter__canonical__eqtype_Equality [def, in infotheo.ecc_modern.ldpc_erasure]
ldpc_erasure_letter__canonical__fintype_Finite [def, in infotheo.ecc_modern.ldpc_erasure]
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 [def, in infotheo.lib.ssr_ext]
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 [def, in infotheo.ecc_modern.ldpc_erasure]
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 [ind, in infotheo.ecc_modern.ldpc_erasure]
letter_count [prf, in infotheo.ecc_modern.ldpc_erasure]
letter_enumP [prf, in infotheo.ecc_modern.ldpc_erasure]
letter_ind [scheme, in infotheo.ecc_modern.ldpc_erasure]
letter_pickle [def, in infotheo.ecc_modern.ldpc_erasure]
letter_rec [scheme, in infotheo.ecc_modern.ldpc_erasure]
letter_rect [scheme, in infotheo.ecc_modern.ldpc_erasure]
letter_sind [scheme, in infotheo.ecc_modern.ldpc_erasure]
letter_spec [ind, in infotheo.ecc_modern.ldpc_erasure]
letter_spec0 [constr, in infotheo.ecc_modern.ldpc_erasure]
letter_spec1 [constr, in infotheo.ecc_modern.ldpc_erasure]
letter_specblank [constr, in infotheo.ecc_modern.ldpc_erasure]
letter_specstar [constr, in infotheo.ecc_modern.ldpc_erasure]
letter_split [prf, in infotheo.ecc_modern.ldpc_erasure]
letter_unpickle [def, in infotheo.ecc_modern.ldpc_erasure]
letterP [prf, in infotheo.ecc_modern.ldpc_erasure]
LinearAffine [mod, in infotheo.probability.convex]
LinearAffine.HB_unnamed_factory_58 [def, in infotheo.probability.convex]
LinearAffine.Linear_sort__canonical__convex_Affine [def, in infotheo.probability.convex]
linearcode [file, in infotheo.ecc_classic.linearcode]
linearcode_sbound_f'__canonical__Algebra_Additive [def, in infotheo.ecc_classic.linearcode]
linearcode_sbound_f'__canonical__GRing_Linear [def, in infotheo.ecc_classic.linearcode]
linearcode_syndrome__canonical__Algebra_Additive [def, in infotheo.ecc_classic.linearcode]
linearcode_syndrome__canonical__GRing_Linear [def, in infotheo.ecc_classic.linearcode]
lmat_le_decr [prf, in infotheo.ecc_modern.ldpc_erasure]
LmoduleConvex [mod, in infotheo.probability.convex]
LmoduleConvex.avgrE [prf, in infotheo.probability.convex]
LmoduleConvex.convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
LmoduleConvex.HB_unnamed_factory_53 [def, in infotheo.probability.convex]
LmoduleConvex.HB_unnamed_mixin_55 [def, in infotheo.probability.convex]
LmoduleConvex.HB_unnamed_mixin_56 [def, in infotheo.probability.convex]
LmoduleConvex.HB_unnamed_mixin_57 [def, in infotheo.probability.convex]
LmoduleConvex.Lmodule_sort__canonical__convex_ConvexSpace [def, 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]
location_polynomial_points [def, in infotheo.ecc_classic.alternant]
log [def, in infotheo.lib.realType_ln]
Log [def, in infotheo.lib.realType_ln]
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_RV [def, in infotheo.probability.proba]
log_sum [file, in infotheo.probability.log_sum]
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]
log_sum_stmt [def, in infotheo.probability.log_sum]
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]
loop [def, in infotheo.ecc_classic.cyclic_code]
lowest_size [def, in infotheo.ecc_classic.linearcode]
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 [def, in infotheo.lib.ssr_ext]
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 [abbrev, in infotheo.probability.necset]
lub [def, in infotheo.probability.necset]
lub_absorbs_conv [prf, in infotheo.probability.necset]
lub_absorbs_convn [prf, in infotheo.probability.necset]
lub_morph [def, in infotheo.probability.necset]
lubA [def, in infotheo.probability.necset]
lubAC [prf, in infotheo.probability.necset]
lubACA [prf, in infotheo.probability.necset]
lubC [def, in infotheo.probability.necset]
lubCA [prf, in infotheo.probability.necset]
lubDl [prf, in infotheo.probability.necset]
lubDr [def, in infotheo.probability.necset]
lubE [def, 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]
lubxx [def, in infotheo.probability.necset]