F (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

F (Lemmas)

F2_0_1 [prf, in infotheo.lib.f2]
F2_addmx [prf, in infotheo.lib.f2]
F2_addmx0 [prf, in infotheo.lib.f2]
F2_eq0 [prf, in infotheo.lib.f2]
F2_eq1 [prf, in infotheo.lib.f2]
F2_mx_opp [prf, in infotheo.lib.f2]
F2_of_bool_0_inv [prf, in infotheo.lib.f2]
F2_of_bool_addr [prf, in infotheo.lib.f2]
F2_of_boolK [prf, in infotheo.lib.f2]
F2_poly_add [prf, in infotheo.lib.f2]
F2P [prf, in infotheo.lib.f2]
f_div_total_1 [prf, in infotheo.information_theory.string_entropy]
f_div_total_pos [prf, in infotheo.information_theory.string_entropy]
f_inj [prf, in infotheo.information_theory.source_coding_vl_direct]
f_inj [prf, in infotheo.information_theory.shannon_fano]
f_phi [prf, in infotheo.information_theory.source_coding_fl_direct]
factorize_range [prf, in infotheo.probability.convex]
fbig_pred1_inj [prf, in infotheo.probability.fsdist]
fdcoor0 [prf, in infotheo.lib.dft]
fdcoor_codeword [prf, in infotheo.ecc_classic.reed_solomon]
fdcoor_GRS_syndrome_coor [prf, in infotheo.ecc_classic.reed_solomon]
fdcoor_loop_rcs [prf, in infotheo.ecc_classic.cyclic_code]
fdcoor_rcs [prf, in infotheo.ecc_classic.cyclic_code]
fdcoor_rcs' [prf, in infotheo.ecc_classic.cyclic_code]
fdcoor_syndrome_coord [prf, in infotheo.ecc_classic.bch]
fdcoorB [prf, in infotheo.lib.dft]
fdcoorD [prf, in infotheo.lib.dft]
fdcoorE [prf, in infotheo.lib.dft]
fdcoorN [prf, in infotheo.lib.dft]
FDist.f1 [prf, in infotheo.probability.fdist]
FDist.ge0 [prf, in infotheo.probability.fdist]
FDist.le1 [prf, in infotheo.probability.fdist]
fdist10 [prf, in infotheo.probability.fdist]
fdist1_inj [prf, in infotheo.probability.fdist]
fdist1bind [prf, in infotheo.probability.fdist]
fdist1C [prf, in infotheo.probability.fdist]
fdist1E [prf, in infotheo.probability.fdist]
fdist1E1 [prf, in infotheo.probability.fdist]
fdist1I1 [prf, in infotheo.probability.fdist]
fdist1P [prf, in infotheo.probability.fdist]
fdist1xx [prf, in infotheo.probability.fdist]
fdist_addE [prf, in infotheo.probability.fdist]
fdist_belast_last_of_rVE [prf, in infotheo.probability.fdist]
fdist_belastE [prf, in infotheo.probability.fdist]
fdist_binaryE [prf, in infotheo.probability.fdist]
fdist_binaryxx [prf, in infotheo.probability.fdist]
fdist_card_neq0 [prf, in infotheo.probability.fdist]
fdist_card_prednK [prf, in infotheo.probability.fdist]
fdist_col'_put_front [prf, in infotheo.information_theory.entropy]
fdist_col'E [prf, in infotheo.probability.fdist]
fdist_condE [prf, in infotheo.probability.proba]
fdist_conv_bind_left_distr [prf, in infotheo.probability.fdist]
fdist_convE [prf, in infotheo.probability.fdist]
fdist_convn1 [prf, in infotheo.probability.fdist]
fdist_convn_Add [prf, in infotheo.probability.fdist]
fdist_convn_add [prf, in infotheo.probability.convex]
fdist_convn_cst [prf, in infotheo.probability.fdist]
fdist_convn_del [prf, in infotheo.probability.fdist]
fdist_convnE [prf, in infotheo.probability.fdist]
fdist_delE [prf, in infotheo.probability.fdist]
fdist_ext [prf, in infotheo.probability.fdist]
fdist_fstE [prf, in infotheo.probability.fdist]
fdist_ge0_le1 [prf, in infotheo.probability.fdist]
fdist_gt0 [prf, in infotheo.probability.fdist]
fdist_ind [prf, in infotheo.probability.fdist]
fdist_is_fdist [prf, in infotheo.probability.fdist]
fdist_lt1 [prf, in infotheo.probability.fdist]
fdist_marginal_post_probE [prf, in infotheo.information_theory.pproba]
fdist_nthE [prf, in infotheo.probability.fdist]
fdist_of_ffun_prop [prf, in infotheo.information_theory.types]
fdist_of_finFSDist.dE [prf, in infotheo.probability.fsdist]
fdist_of_finFSDist.f0 [prf, in infotheo.probability.fsdist]
fdist_of_finFSDist.f1 [prf, in infotheo.probability.fsdist]
fdist_of_FSDist.f0 [prf, in infotheo.probability.fsdist]
fdist_of_FSDist.f1 [prf, in infotheo.probability.fsdist]
fdist_of_FSDistDE [prf, in infotheo.probability.fsdist]
fdist_of_fsE [prf, in infotheo.probability.fsdist]
fdist_outE [prf, in infotheo.information_theory.channel]
fdist_permE [prf, in infotheo.probability.fdist]
fdist_post_probE [prf, in infotheo.information_theory.pproba]
fdist_prod1 [prf, in infotheo.probability.fdist]
fdist_prod1_conv [prf, in infotheo.probability.fdist]
fdist_prod2_conv [prf, in infotheo.probability.fdist]
fdist_prod_nthE [prf, in infotheo.probability.fdist]
fdist_prod_of_fdist_rV [prf, in infotheo.probability.fdist]
fdist_prod_of_rVE [prf, in infotheo.probability.fdist]
fdist_prod_of_rVK [prf, in infotheo.probability.fdist]
fdist_prodE [prf, in infotheo.probability.fdist]
fdist_prodK [prf, in infotheo.probability.jfdist_cond]
fdist_proj13_AC [prf, in infotheo.probability.fdist]
fdist_proj13_domin [prf, in infotheo.probability.fdist]
fdist_proj13_dominN [prf, in infotheo.probability.fdist]
fdist_proj13_fst [prf, in infotheo.probability.fdist]
fdist_proj13_RV3 [prf, in infotheo.probability.proba]
fdist_proj13_snd [prf, in infotheo.probability.fdist]
fdist_proj13E [prf, in infotheo.probability.fdist]
fdist_proj23_domin [prf, in infotheo.probability.fdist]
fdist_proj23_dominN [prf, in infotheo.probability.fdist]
fdist_proj23_fst [prf, in infotheo.probability.fdist]
fdist_proj23_snd [prf, in infotheo.probability.fdist]
fdist_proj23E [prf, in infotheo.probability.fdist]
fdist_rV0 [prf, in infotheo.probability.fdist]
fdist_rV1 [prf, in infotheo.probability.fdist]
fdist_rV_of_prodE [prf, in infotheo.probability.fdist]
fdist_rV_of_prodK [prf, in infotheo.probability.fdist]
fdist_rV_out [prf, in infotheo.information_theory.channel]
fdist_rVE [prf, in infotheo.probability.fdist]
fdist_rVS [prf, in infotheo.probability.fdist]
fdist_self1 [prf, in infotheo.probability.fdist]
fdist_selfE [prf, in infotheo.probability.fdist]
fdist_sndE [prf, in infotheo.probability.fdist]
fdist_supp_lg_add_1_neq_0 [prf, in infotheo.information_theory.source_coding_vl_direct]
fdist_supp_mem [prf, in infotheo.probability.fdist]
fdist_supp_neq0 [prf, in infotheo.probability.fdist]
fdist_support_LB [prf, in infotheo.information_theory.source_coding_vl_direct]
fdist_take_all [prf, in infotheo.probability.fdist]
fdist_take_dropE [prf, in infotheo.probability.fdist]
fdist_take_nth [prf, in infotheo.probability.fdist]
fdist_takeE [prf, in infotheo.probability.fdist]
fdist_uniform_eq1 [prf, in infotheo.probability.fdist]
fdist_uniform_neq0 [prf, in infotheo.probability.fdist]
fdist_uniform_supp_distrr [prf, in infotheo.probability.fdist]
fdist_uniform_supp_in [prf, in infotheo.probability.fdist]
fdist_uniform_supp_neq0 [prf, in infotheo.probability.fdist]
fdist_uniform_supp_notin [prf, in infotheo.probability.fdist]
fdist_uniform_supp_restrict [prf, in infotheo.probability.fdist]
fdist_uniformE [prf, in infotheo.probability.fdist]
fdistA1 [prf, in infotheo.probability.fdist]
fdistA21 [prf, in infotheo.probability.fdist]
fdistA22 [prf, in infotheo.probability.fdist]
fdistA_AC_fst [prf, in infotheo.probability.fdist]
fdistA_AC_snd [prf, in infotheo.probability.fdist]
fdistA_C12_fst [prf, in infotheo.probability.fdist]
fdistA_C13_snd [prf, in infotheo.probability.fdist]
fdistA_domin [prf, in infotheo.probability.fdist]
fdistA_dominN [prf, in infotheo.probability.fdist]
fdistA_RV3 [prf, in infotheo.probability.proba]
fdistAC2 [prf, in infotheo.probability.fdist]
fdistAC_fst_fst [prf, in infotheo.probability.fdist]
fdistACE [prf, in infotheo.probability.fdist]
fdistAE [prf, in infotheo.probability.fdist]
fdistAX12 [prf, in infotheo.probability.fdist]
fdistAX2 [prf, in infotheo.probability.fdist]
fdistbind1 [prf, in infotheo.probability.fdist]
fdistbindA [prf, in infotheo.probability.fdist]
fdistbindE [prf, in infotheo.probability.fdist]
fdistC12_fst [prf, in infotheo.probability.fdist]
fdistC12_RV3 [prf, in infotheo.probability.proba]
fdistC12_snd [prf, in infotheo.probability.fdist]
fdistC12E [prf, in infotheo.probability.fdist]
fdistC12I [prf, in infotheo.probability.fdist]
fdistC13_fst [prf, in infotheo.probability.fdist]
fdistC13_fst_fst [prf, in infotheo.probability.fdist]
fdistC13_snd [prf, in infotheo.probability.fdist]
fdistC13E [prf, in infotheo.probability.fdist]
fdistD1_0 [prf, in infotheo.probability.fdist]
fdistD1_eq0 [prf, in infotheo.probability.fdist]
fdistD1E [prf, in infotheo.probability.fdist]
fdistI0_False [prf, in infotheo.probability.fdist]
fdistI20 [prf, in infotheo.probability.fdist]
fdistI21 [prf, in infotheo.probability.fdist]
fdistI2E [prf, in infotheo.probability.fdist]
fdistI_perm1 [prf, in infotheo.probability.fdist]
fdistI_perm_fdist1 [prf, in infotheo.probability.fdist]
fdistI_permE [prf, in infotheo.probability.fdist]
fdistI_permM [prf, in infotheo.probability.fdist]
fdistI_tperm [prf, in infotheo.probability.fdist]
fdistmap1 [prf, in infotheo.probability.fdist]
fdistmap_comp [prf, in infotheo.probability.fdist]
fdistmap_eq0 [prf, in infotheo.probability.fdist]
fdistmap_id [prf, in infotheo.probability.fdist]
fdistmap_neq0 [prf, in infotheo.probability.fdist]
fdistmapE [prf, in infotheo.probability.fdist]
FDistPart.dE [prf, in infotheo.probability.jfdist_cond]
FDistPart.denE [prf, in infotheo.probability.jfdist_cond]
FDistPart.dK [prf, in infotheo.probability.jfdist_cond]
fdistpart1 [prf, in infotheo.probability.jfdist_cond]
fdistpart1_eq1 [prf, in infotheo.probability.jfdist_cond]
fdistpart1_eq1P [prf, in infotheo.probability.jfdist_cond]
fdistpart1_unif [prf, in infotheo.probability.jfdist_cond]
fdistpart_eq0 [prf, in infotheo.probability.jfdist_cond]
fdistpart_eq1 [prf, in infotheo.probability.jfdist_cond]
fdistpart_neq0 [prf, in infotheo.probability.jfdist_cond]
fdistpart_unif [prf, in infotheo.probability.jfdist_cond]
fdistX1 [prf, in infotheo.probability.fdist]
fdistX2 [prf, in infotheo.probability.fdist]
fdistX_dom_by [prf, in infotheo.probability.fdist]
fdistX_prod [prf, in infotheo.probability.fdist]
fdistX_prod2 [prf, in infotheo.probability.fdist]
fdistX_prod_out [prf, in infotheo.information_theory.channel]
fdistX_RV2 [prf, in infotheo.probability.proba]
fdistX_self [prf, in infotheo.probability.fdist]
fdistXE [prf, in infotheo.probability.fdist]
fdistXI [prf, in infotheo.probability.fdist]
ffun_of_fdist [prf, in infotheo.information_theory.types]
Fgraph_disjoint [prf, in infotheo.ecc_modern.tanner_partition]
Fgraph_injective [prf, in infotheo.ecc_modern.tanner_partition]
Fgraph_m0 [prf, in infotheo.ecc_modern.tanner]
Fgraph_nonempty [prf, in infotheo.ecc_modern.tanner]
Fgraph_Vnext2_Vgraph [prf, in infotheo.ecc_modern.tanner]
Fgraph_Vnext_Vgraph [prf, in infotheo.ecc_modern.tanner]
fibration_of_partitionE [prf, in infotheo.probability.fsdist]
filter1D_arg_decreasing [prf, in infotheo.robust.weightedmean]
filter1D_converges [prf, in infotheo.robust.weightedmean]
filter1D_correct [prf, in infotheo.robust.weightedmean]
filter_out_set0 [prf, in infotheo.ecc_modern.ldpc]
filter_pred1_num_occ [prf, in infotheo.lib.num_occ]
filter_zip_L [prf, in infotheo.lib.ssr_ext]
filter_zip_R [prf, in infotheo.lib.ssr_ext]
fin_img_imset [prf, in infotheo.lib.ssr_ext]
fin_imgP [prf, in infotheo.probability.bayes]
finsupp_conv_subl [prf, in infotheo.probability.fsdist]
finsupp_conv_subr [prf, in infotheo.probability.fsdist]
first_summand [prf, in infotheo.information_theory.channel_coding_direct]
fixed_point_stopset_starFnext [prf, in infotheo.ecc_modern.stopping_set]
flatten_single [prf, in infotheo.lib.ssr_ext]
fm_uniq [prf, in infotheo.information_theory.source_coding_vl_converse]
Fnext_Vnext_Vgraph [prf, in infotheo.ecc_modern.tanner]
FnextE [prf, in infotheo.ecc_modern.tanner]
freeN_combination [prf, in infotheo.probability.convex]
freeon0 [prf, in infotheo.ecc_modern.summary]
freeon1 [prf, in infotheo.ecc_modern.summary]
freeon_all [prf, in infotheo.ecc_modern.summary]
freeon_comb_dprojs_V [prf, in infotheo.ecc_modern.summary_tanner]
freeon_dproj [prf, in infotheo.ecc_modern.summary_tanner]
freeon_dprojs [prf, in infotheo.ecc_modern.summary_tanner]
freeon_notin [prf, in infotheo.ecc_modern.summary]
freeon_refl [prf, in infotheo.ecc_modern.summary]
freeon_row_set [prf, in infotheo.ecc_modern.summary]
freeon_sym [prf, in infotheo.ecc_modern.summary]
freeon_trans [prf, in infotheo.ecc_modern.summary_tanner]
FSDist.f1 [prf, in infotheo.probability.fsdist]
FSDist.ge0 [prf, in infotheo.probability.fsdist]
FSDist.gt0 [prf, in infotheo.probability.fsdist]
FSDist.le1 [prf, in infotheo.probability.fsdist]
fsdist10 [prf, in infotheo.probability.fsdist]
fsdist1_inj [prf, in infotheo.probability.fsdist]
fsdist1bind [prf, in infotheo.probability.fsdist]
fsdist1E [prf, in infotheo.probability.fsdist]
fsdist1map [prf, in infotheo.probability.fsdist]
fsdist1xx [prf, in infotheo.probability.fsdist]
fsdist_conv_bind_left_distr [prf, in infotheo.probability.fsdist]
fsdist_conv_bind_right_distr [prf, in infotheo.probability.fsdist]
fsdist_convE [prf, in infotheo.probability.fsdist]
fsdist_convnE [prf, in infotheo.probability.fsdist]
FSDist_crop0.f0 [prf, in infotheo.probability.fsdist]
FSDist_crop0.f1 [prf, in infotheo.probability.fsdist]
fsdist_eval_affine [prf, in infotheo.probability.fsdist]
fsdist_ext [prf, in infotheo.probability.fsdist]
FSDist_lift_supp.dE [prf, in infotheo.probability.fsdist]
FSDist_lift_supp.DsuppE [prf, in infotheo.probability.fsdist]
FSDist_lift_supp.f0 [prf, in infotheo.probability.fsdist]
FSDist_lift_supp.f1 [prf, in infotheo.probability.fsdist]
FSDist_lift_supp.r_surj [prf, in infotheo.probability.fsdist]
FSDist_lift_supp.s_inj [prf, in infotheo.probability.fsdist]
fsdist_scalept_conv [prf, in infotheo.probability.fsdist]
fsdist_supp_neq0 [prf, in infotheo.probability.fsdist]
fsdist_suppD1 [prf, in infotheo.probability.fsdist]
fsdistbind1 [prf, in infotheo.probability.fsdist]
fsdistbindA [prf, in infotheo.probability.fsdist]
fsdistbindE [prf, in infotheo.probability.fsdist]
fsdistbindEcond [prf, in infotheo.probability.fsdist]
fsdistbindEwiden [prf, in infotheo.probability.fsdist]
fsdistjoin1 [prf, in infotheo.probability.fsdist]
fsdistjoinE [prf, in infotheo.probability.fsdist]
fsdistmap1 [prf, in infotheo.probability.fsdist]
fsdistmap_affine [prf, in infotheo.probability.fsdist]
fsdistmap_comp [prf, in infotheo.probability.fsdist]
fsdistmap_id [prf, in infotheo.probability.fsdist]
fst_Pr_domin_setX [prf, in infotheo.probability.proba]
fst_RV2 [prf, in infotheo.probability.proba]
fst_tnth_prod_rV [prf, in infotheo.lib.ssralg_ext]
fsumr_gt0 [prf, in infotheo.lib.bigop_ext]
full_rank_inj [prf, in infotheo.lib.ssralg_ext]
full_sum_num_occ [prf, in infotheo.lib.num_occ]
full_sum_num_occ_n [prf, in infotheo.lib.num_occ]
full_take_shell [prf, in infotheo.information_theory.jtypes]
FunLe.eqfun_le [prf, in infotheo.probability.convex]
FunLe.lefun_trans [prf, in infotheo.probability.convex]
FunLe.lefunR [prf, in infotheo.probability.convex]