B (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

B (Lemmas)

ball_disjoint_min_dist_lb [prf, in infotheo.ecc_classic.linearcode]
barycenter_map [prf, in infotheo.probability.convex]
base_case [prf, in infotheo.robust.weightedmean]
Bayes [prf, in infotheo.probability.proba]
Bayes_extended [prf, in infotheo.probability.proba]
BCH.BCH_PCM_altP1 [prf, in infotheo.ecc_classic.bch]
BCH.BCH_PCM_altP2 [prf, in infotheo.ecc_classic.bch]
BCH.PCM_alt_GRS [prf, in infotheo.ecc_classic.bch]
BCH.PCM_altP [prf, in infotheo.ecc_classic.bch]
BCH_argument_lemma [prf, in infotheo.lib.dft]
BCH_codebook [prf, in infotheo.ecc_classic.bch]
BCH_det_mlinear [prf, in infotheo.ecc_classic.bch]
BCH_err_is_correct [prf, in infotheo.ecc_classic.bch]
BCH_key_equation [prf, in infotheo.ecc_classic.bch]
BCH_key_equation_old [prf, in infotheo.ecc_classic.bch]
BCH_min_dist1 [prf, in infotheo.ecc_classic.bch]
BCH_mod_is_GRS_mod [prf, in infotheo.ecc_classic.bch]
BCH_repair_is_correct [prf, in infotheo.ecc_classic.bch]
BCH_syndrome_synp [prf, in infotheo.ecc_classic.bch]
BCH_syndromep_is_GRS_syndromep [prf, in infotheo.ecc_classic.bch]
Beaulieu_technical_equality [prf, in infotheo.probability.necset]
BEC_IO_erase [prf, in infotheo.ecc_modern.stopping_set]
belast_last_take [prf, in infotheo.probability.fdist]
beta0x [prf, in infotheo.ecc_modern.ldpc_algo]
beta_def [prf, in infotheo.ecc_modern.ldpc_algo_proof]
beta_inva [prf, in infotheo.ecc_modern.ldpc]
beta_inva_helper [prf, in infotheo.ecc_modern.ldpc]
beta_map [prf, in infotheo.ecc_modern.ldpc_algo_proof]
beta_one_successor [prf, in infotheo.ecc_modern.ldpc]
betaA [prf, in infotheo.ecc_modern.ldpc_algo]
betaC [prf, in infotheo.ecc_modern.ldpc_algo]
big_beta_mul [prf, in infotheo.ecc_modern.ldpc_algo_proof]
big_bigcup_partition [prf, in infotheo.lib.bigop_ext]
big_bool [prf, in infotheo.lib.bigop_ext]
big_cast_rV [prf, in infotheo.lib.bigop_ext]
big_cat_tuple [prf, in infotheo.information_theory.channel_coding_direct]
big_cat_tuple_seq [prf, in infotheo.information_theory.channel_coding_direct]
big_enum_in_cond [prf, in infotheo.ecc_modern.degree_profile]
big_enum_in_nocond [prf, in infotheo.ecc_modern.degree_profile]
big_pred1_inj [prf, in infotheo.lib.bigop_ext]
big_prod_ord [prf, in infotheo.probability.convex]
big_rV0_row_of_tuple [prf, in infotheo.lib.bigop_ext]
big_rV1_ord0 [prf, in infotheo.lib.bigop_ext]
big_rV_1 [prf, in infotheo.lib.bigop_ext]
big_rV_behead [prf, in infotheo.lib.bigop_ext]
big_rV_belast_last [prf, in infotheo.lib.bigop_ext]
big_rV_cons [prf, in infotheo.lib.bigop_ext]
big_rV_cons_behead [prf, in infotheo.lib.bigop_ext]
big_rV_cons_behead_support [prf, in infotheo.lib.bigop_ext]
big_rV_prod [prf, in infotheo.lib.bigop_ext]
big_scalept_conv_split [prf, in infotheo.probability.convex]
big_scaleptl' [prf, in infotheo.probability.convex]
big_seq_tuple [prf, in infotheo.information_theory.source_coding_vl_converse]
big_set2 [prf, in infotheo.lib.ssr_ext]
big_setX [prf, in infotheo.lib.bigop_ext]
big_tcast [prf, in infotheo.lib.bigop_ext]
big_tuple_cons_behead [prf, in infotheo.information_theory.channel_coding_direct]
big_tuple_ffun [prf, in infotheo.lib.bigop_ext]
big_union [prf, in infotheo.lib.bigop_ext]
big_union_nondisj [prf, in infotheo.lib.bigop_ext]
bigA_distr [prf, in infotheo.lib.bigop_ext]
bigcup_Fgraph_set0 [prf, in infotheo.ecc_modern.tanner]
bigcup_of_const [prf, in infotheo.lib.classical_sets_ext]
bigcup_preimset [prf, in infotheo.lib.bigop_ext]
bigcup_set0 [prf, in infotheo.lib.bigop_ext]
bigcup_set0P [prf, in infotheo.lib.classical_sets_ext]
bigcup_set1 [prf, in infotheo.lib.bigop_ext]
bigcup_setX [prf, in infotheo.lib.bigop_ext]
bigcup_succ_set0 [prf, in infotheo.ecc_modern.tanner]
bigfcup_imfset [prf, in infotheo.probability.fsdist]
bigID2 [prf, in infotheo.lib.bigop_ext]
bigID_setC [prf, in infotheo.lib.bigop_ext]
biglub_bigcup [prf, in infotheo.probability.necset]
biglub_conv_pt_setD [prf, in infotheo.probability.necset]
biglub_conv_pt_setE [prf, in infotheo.probability.necset]
biglub_conv_setD [prf, in infotheo.probability.necset]
biglub_conv_setE [prf, in infotheo.probability.necset]
biglub_flatten [prf, in infotheo.probability.necset]
biglub_hull [prf, in infotheo.probability.necset]
biglub_iter_conv_set [prf, in infotheo.probability.necset]
biglub_lub_morph [prf, in infotheo.probability.necset]
biglub_oplus_conv_setE [prf, in infotheo.probability.necset]
biglub_setU [prf, in infotheo.probability.necset]
biglubDl [prf, in infotheo.probability.necset]
bigmax_gt0P_seq [prf, in infotheo.lib.bigop_ext]
bigmax_le_seq [prf, in infotheo.lib.bigop_ext]
bigmax_leP_seq [prf, in infotheo.lib.bigop_ext]
bigmaxR_bigmin_vec_helper [prf, in infotheo.ecc_classic.decoding]
bigmaxR_distrl [prf, in infotheo.ecc_classic.decoding]
bigmaxR_distrr [prf, in infotheo.ecc_classic.decoding]
bigmaxR_eq [prf, in infotheo.ecc_classic.decoding]
bigmaxR_seq_eq [prf, in infotheo.ecc_classic.decoding]
bigsubsetU [prf, in infotheo.lib.classical_sets_ext]
bij_comp_RV [prf, in infotheo.probability.proba]
bij_RV_unif [prf, in infotheo.probability.proba]
bij_swap [prf, in infotheo.lib.ssr_ext]
bijective_F2_of_bool [prf, in infotheo.lib.f2]
bin_of_nat_7 [prf, in infotheo.lib.natbin]
bin_of_nat_expn2 [prf, in infotheo.lib.ssr_ext]
bin_of_nat_inj [prf, in infotheo.lib.ssr_ext]
bin_of_nat_nat_of_pos_not_0 [prf, in infotheo.lib.ssr_ext]
bin_of_nat_rev7 [prf, in infotheo.lib.natbin]
binomial_theorem [prf, in infotheo.lib.hamming]
BinPos_nat_of_P_nat_of_pos [prf, in infotheo.lib.ssr_ext]
BinToNaryToBin._equiv_convn [prf, in infotheo.probability.convex_equiv]
BinToNaryToBin.equiv_conv [prf, in infotheo.probability.convex_equiv]
bipart_dominates [prf, in infotheo.probability.pinsker]
bipartite_cycle_even [prf, in infotheo.ecc_modern.subgraph_partition]
bipartite_path_kind_even [prf, in infotheo.ecc_modern.subgraph_partition]
bipartite_path_kind_next [prf, in infotheo.ecc_modern.subgraph_partition]
Bit_col [prf, in infotheo.ecc_modern.ldpc_erasure]
bitseq_of_N_2 [prf, in infotheo.lib.natbin]
bitseq_of_N_bin_of_nat_expn2 [prf, in infotheo.lib.natbin]
bitseq_of_N_inj [prf, in infotheo.lib.natbin]
bitseq_of_N_leading_bit [prf, in infotheo.lib.natbin]
bitseq_of_N_nseq_false [prf, in infotheo.lib.natbin]
bitseq_of_nat_0 [prf, in infotheo.lib.natbin]
bitseq_of_nat_expn2 [prf, in infotheo.lib.natbin]
bitseq_of_nat_inj [prf, in infotheo.lib.natbin]
bitseq_of_nat_nseq_false [prf, in infotheo.lib.natbin]
bitseq_of_pos_inj [prf, in infotheo.lib.natbin]
bitseq_of_pos_not_false [prf, in infotheo.lib.natbin]
bitseq_of_pos_not_nil [prf, in infotheo.lib.natbin]
bitseq_of_pos_not_nseq_false [prf, in infotheo.lib.natbin]
bitseq_of_pos_true [prf, in infotheo.lib.natbin]
bitseq_row_nth [prf, in infotheo.lib.f2]
BN.cancel_both_disjoint [prf, in infotheo.probability.bayes]
BN.cinde_events_cPr1 [prf, in infotheo.probability.bayes]
BN.cinde_events_vals [prf, in infotheo.probability.bayes]
BN.cinde_eventsC [prf, in infotheo.probability.bayes]
BN.cinde_preim_equiv [prf, in infotheo.probability.bayes]
BN.cinde_preim_equiv1 [prf, in infotheo.probability.bayes]
BN.cinde_preim_inter [prf, in infotheo.probability.bayes]
BN.cinde_preim_ok [prf, in infotheo.probability.bayes]
BN.cinde_preim_ok1 [prf, in infotheo.probability.bayes]
BN.cinde_preim_sub [prf, in infotheo.probability.bayes]
BN.cinde_preimC [prf, in infotheo.probability.bayes]
BN.disjoint_preim_vars [prf, in infotheo.probability.bayes]
BN.Pr_preim_vars_sub [prf, in infotheo.probability.bayes]
BN.preim_inter [prf, in infotheo.probability.bayes]
BN.preim_prod_vars [prf, in infotheo.probability.bayes]
BN.preim_vars12 [prf, in infotheo.probability.bayes]
BN.preim_vars_inter [prf, in infotheo.probability.bayes]
BN.preim_vars_set_vals_tl [prf, in infotheo.probability.bayes]
BN.preim_vars_vals [prf, in infotheo.probability.bayes]
BN.preim_varsP [prf, in infotheo.probability.bayes]
BN.prod_vars1 [prf, in infotheo.probability.bayes]
BN.prod_vars_inter [prf, in infotheo.probability.bayes]
BN.prod_vars_pair [prf, in infotheo.probability.bayes]
BN.Rxx2 [prf, in infotheo.probability.bayes]
BN.set_vals_prod_vars [prf, in infotheo.probability.bayes]
BN_factorization [prf, in infotheo.probability.bayes]
bool_of_F2_add_xor [prf, in infotheo.lib.f2]
bool_of_F2K [prf, in infotheo.lib.f2]
Boole_eq [prf, in infotheo.probability.proba]
boolPF [prf, in infotheo.lib.ssr_ext]
boolPT [prf, in infotheo.lib.ssr_ext]
bound_card_jtype [prf, in infotheo.information_theory.jtypes]
bound_emean [prf, in infotheo.robust.weightedmean]
bound_empirical_variance_cplt_S [prf, in infotheo.robust.weightedmean]
bound_empirical_variance_S [prf, in infotheo.robust.weightedmean]
bound_evar_ineq_by_interval [prf, in infotheo.robust.weightedmean]
bound_evar_ineq_S [prf, in infotheo.robust.weightedmean]
bound_evar_ineq_S_intermediate [prf, in infotheo.robust.weightedmean]
bound_mean [prf, in infotheo.robust.weightedmean]
bound_mean_emean [prf, in infotheo.robust.weightedmean]
BSC_capacity [prf, in infotheo.information_theory.binary_symmetric_channel]
bsc_post [prf, in infotheo.information_theory.binary_symmetric_channel]
bsc_prob_prop [prf, in infotheo.information_theory.binary_symmetric_channel]
bseqval_inj [prf, in infotheo.lib.ssr_ext]
build_tree_full [prf, in infotheo.ecc_modern.ldpc_algo_proof]
build_tree_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
build_tree_rec_full [prf, in infotheo.ecc_modern.ldpc_algo_proof]
build_tree_rec_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
build_tree_rec_sound [prf, in infotheo.ecc_modern.ldpc_algo_proof]
Builders_1.axbary [prf, in infotheo.probability.convex_equiv]
Builders_1.axproj [prf, in infotheo.probability.convex_equiv]
Builders_11.axbary [prf, in infotheo.probability.convex_equiv]
Builders_11.axproj [prf, in infotheo.probability.convex_equiv]
Builders_16.axidem [prf, in infotheo.probability.convex_equiv]
Builders_6.axproj [prf, in infotheo.probability.convex_equiv]