F (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

F

f [def, in infotheo.probability.fdist]
f [def, in infotheo.information_theory.source_coding_vl_direct]
f [def, in infotheo.information_theory.source_coding_fl_direct]
f [def, in infotheo.information_theory.channel]
f2 [file, in infotheo.lib.f2]
F2_0 [constr, in infotheo.lib.f2]
F2_0_1 [prf, in infotheo.lib.f2]
F2_1 [constr, 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 [def, 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_of_letter [def, in infotheo.ecc_modern.ldpc_erasure]
F2_poly_add [prf, in infotheo.lib.f2]
F2_spec [ind, in infotheo.lib.f2]
F2_to_GF2 [def, in infotheo.lib.ssralg_ext]
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]
fdcoor [def, in infotheo.lib.dft]
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 [file, in infotheo.probability.fdist]
FDist [mod, in infotheo.probability.fdist]
FDist.Exports [mod, in infotheo.probability.fdist]
FDist.Exports.fdist [abbrev, in infotheo.probability.fdist]
FDist.f [proj, in infotheo.probability.fdist]
FDist.f1 [prf, in infotheo.probability.fdist]
FDist.ge0 [prf, in infotheo.probability.fdist]
FDist.le1 [prf, in infotheo.probability.fdist]
FDist.make [def, in infotheo.probability.fdist]
FDist.t [rec, in infotheo.probability.fdist]
fdist1 [def, 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_add [def, in infotheo.probability.fdist]
fdist_addE [prf, in infotheo.probability.fdist]
fdist_belast [def, in infotheo.probability.fdist]
fdist_belast_last_of_rV [def, in infotheo.probability.fdist]
fdist_belast_last_of_rVE [prf, in infotheo.probability.fdist]
fdist_belastE [prf, in infotheo.probability.fdist]
fdist_binary [def, in infotheo.probability.fdist]
fdist_binary_supp0 [def, in infotheo.probability.fdist]
fdist_binary_supp1 [def, 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_choice [def, in infotheo.probability.bayes]
fdist_choice' [def, in infotheo.probability.bayes]
fdist_col' [def, in infotheo.probability.fdist]
fdist_col'_put_front [prf, in infotheo.information_theory.entropy]
fdist_col'E [prf, in infotheo.probability.fdist]
fdist_cond [def, in infotheo.probability.proba]
fdist_condE [prf, in infotheo.probability.proba]
fdist_conv [def, in infotheo.probability.fdist]
fdist_conv_bind_left_distr [prf, in infotheo.probability.fdist]
fdist_convE [prf, in infotheo.probability.fdist]
fdist_convn [def, 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_del [def, in infotheo.probability.fdist]
fdist_del_idx [def, in infotheo.probability.fdist]
fdist_delE [prf, in infotheo.probability.fdist]
fdist_ext [prf, in infotheo.probability.fdist]
fdist_fst [def, 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_prob [def, in infotheo.information_theory.pproba]
fdist_marginal_post_probE [prf, in infotheo.information_theory.pproba]
fdist_nth [def, in infotheo.probability.fdist]
fdist_nthE [prf, in infotheo.probability.fdist]
fdist_of_ffun [def, in infotheo.information_theory.types]
fdist_of_ffun_prop [prf, in infotheo.information_theory.types]
fdist_of_finFSDist [mod, in infotheo.probability.fsdist]
fdist_of_finFSDist.d [def, in infotheo.probability.fsdist]
fdist_of_finFSDist.dE [prf, in infotheo.probability.fsdist]
fdist_of_finFSDist.Exports [mod, in infotheo.probability.fsdist]
fdist_of_finFSDist.Exports.fdist_of_finfs [abbrev, in infotheo.probability.fsdist]
fdist_of_finFSDist.f [def, 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 [mod, in infotheo.probability.fsdist]
fdist_of_FSDist.d [def, in infotheo.probability.fsdist]
fdist_of_FSDist.D [def, in infotheo.probability.fsdist]
fdist_of_FSDist.Exports [mod, in infotheo.probability.fsdist]
fdist_of_FSDist.Exports.fdist_of_fs [abbrev, in infotheo.probability.fsdist]
fdist_of_FSDist.f [def, 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_out [def, in infotheo.information_theory.channel]
fdist_outE [prf, in infotheo.information_theory.channel]
fdist_perm [def, in infotheo.probability.fdist]
fdist_permE [prf, in infotheo.probability.fdist]
fdist_post_prob [def, in infotheo.information_theory.pproba]
fdist_post_prob_den_ge0 [def, in infotheo.information_theory.pproba]
fdist_post_probE [prf, in infotheo.information_theory.pproba]
fdist_prod [def, in infotheo.probability.fdist]
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_nth [def, 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_rV [def, in infotheo.probability.fdist]
fdist_prod_of_rVE [prf, in infotheo.probability.fdist]
fdist_prod_of_rVK [prf, in infotheo.probability.fdist]
fdist_prod_take [def, in infotheo.probability.fdist]
fdist_prodE [prf, in infotheo.probability.fdist]
fdist_prodK [prf, in infotheo.probability.jfdist_cond]
fdist_proj13 [def, in infotheo.probability.fdist]
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 [def, 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_rV [def, in infotheo.probability.fdist]
fdist_rV0 [prf, in infotheo.probability.fdist]
fdist_rV1 [prf, in infotheo.probability.fdist]
fdist_rV_of_prod [def, 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_self [def, in infotheo.probability.fdist]
fdist_self1 [prf, in infotheo.probability.fdist]
fdist_selfE [prf, in infotheo.probability.fdist]
fdist_snd [def, in infotheo.probability.fdist]
fdist_sndE [prf, in infotheo.probability.fdist]
fdist_split [def, in infotheo.probability.jfdist_cond]
fdist_supp [def, in infotheo.probability.fdist]
fdist_supp_choice [def, in infotheo.robust.robustmean]
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_t__canonical__choice_Choice [def, in infotheo.probability.fdist]
FDist_t__canonical__choice_SubChoice [def, in infotheo.probability.fdist]
FDist_t__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
FDist_t__canonical__eqtype_Equality [def, in infotheo.probability.fdist]
FDist_t__canonical__eqtype_SubEquality [def, in infotheo.probability.fdist]
FDist_t__canonical__eqtype_SubType [def, in infotheo.probability.fdist]
fdist_take [def, in infotheo.probability.fdist]
fdist_take_all [prf, in infotheo.probability.fdist]
fdist_take_drop [def, 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 [def, in infotheo.probability.fdist]
fdist_uniform_eq1 [prf, in infotheo.probability.fdist]
fdist_uniform_neq0 [prf, in infotheo.probability.fdist]
fdist_uniform_supp [def, 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]
fdistA [def, 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]
fdistAC [def, in infotheo.probability.fdist]
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]
fdistbind [def, in infotheo.probability.fdist]
fdistbind1 [prf, in infotheo.probability.fdist]
fdistbindA [prf, in infotheo.probability.fdist]
fdistbindE [prf, in infotheo.probability.fdist]
fdistC12 [def, 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 [def, 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 [def, in infotheo.probability.fdist]
fdistD1_0 [prf, in infotheo.probability.fdist]
fdistD1_eq0 [prf, in infotheo.probability.fdist]
fdistD1E [prf, in infotheo.probability.fdist]
fdistE [def, in infotheo.probability.fdist]
fdistI0_False [prf, in infotheo.probability.fdist]
fdistI2 [def, in infotheo.probability.fdist]
fdistI20 [prf, in infotheo.probability.fdist]
fdistI21 [prf, in infotheo.probability.fdist]
fdistI2E [prf, in infotheo.probability.fdist]
fdistI_perm [def, 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]
fdistmap [def, 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 [mod, in infotheo.probability.jfdist_cond]
FDistPart.d [def, in infotheo.probability.jfdist_cond]
FDistPart.dE [prf, in infotheo.probability.jfdist_cond]
FDistPart.den [def, 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]
fdistX [def, in infotheo.probability.fdist]
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]
ffun1 [def, in infotheo.robust.weightedmean]
ffun_of_fdist [prf, in infotheo.information_theory.types]
ffun_of_jtype [def, in infotheo.information_theory.jtypes]
ffun_of_type [def, in infotheo.information_theory.types]
Fgraph [def, in infotheo.ecc_modern.tanner]
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_part_Fgraph [def, in infotheo.ecc_modern.tanner_partition]
Fgraph_part_fnode [def, in infotheo.ecc_modern.tanner_partition]
Fgraph_Vnext2_Vgraph [prf, in infotheo.ecc_modern.tanner]
Fgraph_Vnext_Vgraph [prf, in infotheo.ecc_modern.tanner]
fibration_of_partition [def, in infotheo.probability.fsdist]
fibration_of_partitionE [prf, in infotheo.probability.fsdist]
filter1D [def, in infotheo.robust.weightedmean]
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 [def, 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 [def, in infotheo.ecc_modern.tanner]
Fnext_Vnext_Vgraph [prf, in infotheo.ecc_modern.tanner]
FnextE [prf, in infotheo.ecc_modern.tanner]
frac_part [def, in infotheo.lib.realType_ext]
freeN_combination [prf, in infotheo.probability.convex]
freeon [def, in infotheo.ecc_modern.summary]
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 [file, in infotheo.probability.fsdist]
fsdist [abbrev, in infotheo.probability.fsdist]
FSDist [mod, in infotheo.probability.fsdist]
FSDist.f [proj, in infotheo.probability.fsdist]
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]
FSDist.make [def, in infotheo.probability.fsdist]
FSDist.t [rec, in infotheo.probability.fsdist]
fsdist1 [def, 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 [def, 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_Convn_of_fsdist__canonical__convex_Affine [def, in infotheo.probability.fsdist]
fsdist_convnE [prf, in infotheo.probability.fsdist]
FSDist_crop0 [mod, in infotheo.probability.fsdist]
FSDist_crop0.d [def, in infotheo.probability.fsdist]
FSDist_crop0.D [def, in infotheo.probability.fsdist]
FSDist_crop0.f [def, in infotheo.probability.fsdist]
FSDist_crop0.f' [def, in infotheo.probability.fsdist]
FSDist_crop0.f0 [prf, in infotheo.probability.fsdist]
FSDist_crop0.f1 [prf, in infotheo.probability.fsdist]
fsdist_eval [def, in infotheo.probability.fsdist]
fsdist_eval_affine [prf, in infotheo.probability.fsdist]
fsdist_ext [prf, in infotheo.probability.fsdist]
fsdist_fsdist_eval__canonical__convex_Affine [def, in infotheo.probability.fsdist]
fsdist_fsdistmap__canonical__convex_Affine [def, in infotheo.probability.fsdist]
FSDist_lift_supp [mod, in infotheo.probability.fsdist]
FSDist_lift_supp.d [def, in infotheo.probability.fsdist]
FSDist_lift_supp.D [def, 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_of_fdist [mod, in infotheo.probability.fsdist]
FSDist_of_fdist.d [def, in infotheo.probability.fsdist]
FSDist_of_fdist.f [def, in infotheo.probability.fsdist]
fsdist_P__canonical__measure_function_Content [def, in infotheo.probability.fsdist]
fsdist_P__canonical__measure_function_Measure [def, in infotheo.probability.fsdist]
FSDist_prob [def, 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]
FSDist_t__canonical__choice_Choice [def, in infotheo.probability.fsdist]
FSDist_t__canonical__choice_SubChoice [def, in infotheo.probability.fsdist]
FSDist_t__canonical__convex_ConvexSpace [def, in infotheo.probability.fsdist]
FSDist_t__canonical__eqtype_Equality [def, in infotheo.probability.fsdist]
FSDist_t__canonical__eqtype_SubEquality [def, in infotheo.probability.fsdist]
FSDist_t__canonical__eqtype_SubType [def, in infotheo.probability.fsdist]
fsdistbind [def, 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]
fsdistjoin [def, in infotheo.probability.fsdist]
fsdistjoin1 [prf, in infotheo.probability.fsdist]
fsdistjoinE [prf, in infotheo.probability.fsdist]
fsdistmap [def, 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]
fsdistmapE [def, 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]
Func [constr, in infotheo.ecc_modern.ldpc_algo]
FunConvexSpace [mod, in infotheo.probability.convex]
FunConvexSpace.avg [def, in infotheo.probability.convex]
FunConvexSpace.choice_Choice__to__choice_hasChoice [def, in infotheo.probability.convex]
FunConvexSpace.choice_Choice__to__eqtype_hasDecEq [def, in infotheo.probability.convex]
FunConvexSpace.convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
FunConvexSpace.FunConvexSpace_funT__canonical__choice_Choice [def, in infotheo.probability.convex]
FunConvexSpace.FunConvexSpace_funT__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
FunConvexSpace.FunConvexSpace_funT__canonical__eqtype_Equality [def, in infotheo.probability.convex]
FunConvexSpace.funT [def, in infotheo.probability.convex]
FunConvexSpace.HB_unnamed_factory_63 [def, in infotheo.probability.convex]
FunConvexSpace.HB_unnamed_factory_68 [def, in infotheo.probability.convex]
FunConvexSpace.HB_unnamed_mixin_66 [def, in infotheo.probability.convex]
FunConvexSpace.HB_unnamed_mixin_67 [def, in infotheo.probability.convex]
FunConvexSpace.HB_unnamed_mixin_70 [def, in infotheo.probability.convex]
FunConvexSpace.T [abbrev, in infotheo.probability.convex]
FunLe [mod, in infotheo.probability.convex]
FunLe.eqfun_le [prf, in infotheo.probability.convex]
FunLe.lefun [def, in infotheo.probability.convex]
FunLe.lefun_trans [prf, in infotheo.probability.convex]
FunLe.lefunR [prf, in infotheo.probability.convex]