Files

  • infotheo

    • B (Global Index)

    Files ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Definitions ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Lemmas ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Abbreviations ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Global Index ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Notations

    B

    ball [def, in infotheo.ecc_classic.linearcode]
    ball_disjoint_min_dist_lb [prf, in infotheo.ecc_classic.linearcode]
    barycenter [def, in infotheo.probability.convex]
    barycenter_map [prf, in infotheo.probability.convex]
    base_case [prf, in infotheo.robust.weightedmean]
    bayes [file, in infotheo.probability.bayes]
    Bayes [prf, in infotheo.probability.proba]
    Bayes_extended [prf, in infotheo.probability.proba]
    bch [file, in infotheo.ecc_classic.bch]
    BCH [mod, in infotheo.ecc_classic.bch]
    BCH.BCH_PCM_altP1 [prf, in infotheo.ecc_classic.bch]
    BCH.BCH_PCM_altP2 [prf, in infotheo.ecc_classic.bch]
    BCH.code [def, in infotheo.ecc_classic.bch]
    BCH.PCM [def, in infotheo.ecc_classic.bch]
    BCH.PCM_alt [def, 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.syndromep [def, 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 [def, in infotheo.ecc_classic.bch]
    BCH_err_is_correct [prf, in infotheo.ecc_classic.bch]
    BCH_erreval [def, 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 [def, in infotheo.ecc_classic.bch]
    BCH_mod_is_GRS_mod [prf, in infotheo.ecc_classic.bch]
    BCH_repair [def, 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]
    BD_decoding [def, in infotheo.ecc_classic.decoding]
    Beaulieu_technical_equality [prf, in infotheo.probability.necset]
    BEC_IO [def, in infotheo.ecc_modern.ldpc_erasure]
    BEC_IO_erase [prf, in infotheo.ecc_modern.stopping_set]
    belast_last_take [prf, in infotheo.probability.fdist]
    beta [def, in infotheo.ecc_modern.ldpc_algo]
    beta [def, in infotheo.ecc_modern.ldpc]
    beta0x [prf, in infotheo.ecc_modern.ldpc_algo]
    beta_def [prf, in infotheo.ecc_modern.ldpc_algo_proof]
    beta_fun [def, in infotheo.ecc_modern.ldpc]
    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]
    beta_op [def, in infotheo.ecc_modern.ldpc_algo]
    betaA [prf, in infotheo.ecc_modern.ldpc_algo]
    betaC [prf, in infotheo.ecc_modern.ldpc_algo]
    biconvex_function [def, in infotheo.probability.convex]
    biconvex_is_not_convex_in_both [def, in infotheo.probability.convex]
    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 [def, in infotheo.ecc_modern.degree_profile]
    big_enum_in_cond [prf, in infotheo.ecc_modern.degree_profile]
    big_enum_in_nocond [prf, in infotheo.ecc_modern.degree_profile]
    big_morph_oppr [def, in infotheo.lib.bigop_ext]
    big_morph_scalept [def, in infotheo.probability.convex]
    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 [def, in infotheo.probability.convex]
    big_scaleptl' [prf, in infotheo.probability.convex]
    big_scaler [def, 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_disj [def, 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 [def, in infotheo.probability.necset]
    biglub1 [def, in infotheo.probability.necset]
    biglub_bigcup [prf, in infotheo.probability.necset]
    biglub_bignesetU [def, 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_morph [def, in infotheo.probability.necset]
    biglub_oplus_conv_setE [prf, in infotheo.probability.necset]
    biglub_setU [prf, in infotheo.probability.necset]
    BiglubAffine [abbrev, in infotheo.probability.necset]
    BiglubAffine [mod, in infotheo.probability.necset]
    BiglubAffine.axioms_ [rec, in infotheo.probability.necset]
    BiglubAffine.class [proj, in infotheo.probability.necset]
    BiglubAffine.clone [abbrev, in infotheo.probability.necset]
    BiglubAffine.convex_isAffine_mixin [proj, in infotheo.probability.necset]
    BiglubAffine.copy [abbrev, in infotheo.probability.necset]
    BiglubAffine.Exports [mod, in infotheo.probability.necset]
    BiglubAffine.Exports.join_necset_BiglubAffine_between_convex_Affine_and_necset_BiglubMorph [def, in infotheo.probability.necset]
    BiglubAffine.Exports.necset_BiglubAffine__to__convex_Affine [def, in infotheo.probability.necset]
    BiglubAffine.Exports.necset_BiglubAffine__to__necset_BiglubMorph [def, in infotheo.probability.necset]
    BiglubAffine.Exports.necset_BiglubAffine_class__to__convex_Affine_class [def, in infotheo.probability.necset]
    BiglubAffine.Exports.necset_BiglubAffine_class__to__necset_BiglubMorph_class [def, in infotheo.probability.necset]
    BiglubAffine.necset_isBiglubMorph_mixin [proj, in infotheo.probability.necset]
    BiglubAffine.on [abbrev, in infotheo.probability.necset]
    BiglubAffine.on_ [abbrev, in infotheo.probability.necset]
    BiglubAffine.pack_ [def, in infotheo.probability.necset]
    BiglubAffine.phant_clone [def, in infotheo.probability.necset]
    BiglubAffine.phant_on_ [def, in infotheo.probability.necset]
    BiglubAffine.sort [proj, in infotheo.probability.necset]
    BiglubAffine.type [rec, in infotheo.probability.necset]
    BiglubAffineElpiOperations [mod, in infotheo.probability.necset]
    biglubDl [prf, in infotheo.probability.necset]
    biglubDr [def, in infotheo.probability.necset]
    BiglubMorph [abbrev, in infotheo.probability.necset]
    BiglubMorph [mod, in infotheo.probability.necset]
    biglubmorph [def, in infotheo.probability.necset]
    BiglubMorph.axioms_ [rec, in infotheo.probability.necset]
    BiglubMorph.class [proj, in infotheo.probability.necset]
    BiglubMorph.clone [abbrev, in infotheo.probability.necset]
    BiglubMorph.copy [abbrev, in infotheo.probability.necset]
    BiglubMorph.Exports [mod, in infotheo.probability.necset]
    BiglubMorph.necset_isBiglubMorph_mixin [proj, in infotheo.probability.necset]
    BiglubMorph.on [abbrev, in infotheo.probability.necset]
    BiglubMorph.on_ [abbrev, in infotheo.probability.necset]
    BiglubMorph.pack_ [def, in infotheo.probability.necset]
    BiglubMorph.phant_clone [def, in infotheo.probability.necset]
    BiglubMorph.phant_on_ [def, in infotheo.probability.necset]
    BiglubMorph.sort [proj, in infotheo.probability.necset]
    BiglubMorph.type [rec, in infotheo.probability.necset]
    BiglubMorphElpiOperations [mod, 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]
    bigop_ext [file, in infotheo.lib.bigop_ext]
    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]
    binary_entropy_function [file, in infotheo.lib.binary_entropy_function]
    binary_symmetric_channel [file, in infotheo.information_theory.binary_symmetric_channel]
    binomial_theorem [prf, in infotheo.lib.hamming]
    BinPos_nat_of_P_nat_of_pos [prf, in infotheo.lib.ssr_ext]
    BinToNary [mod, in infotheo.probability.convex_equiv]
    BinToNary.axbary [def, in infotheo.probability.convex_equiv]
    BinToNary.axproj [def, in infotheo.probability.convex_equiv]
    BinToNary.ConvexSpace_sort__canonical__convex_equiv_NaryConvexSpace [def, in infotheo.probability.convex_equiv]
    BinToNary.ConvexSpace_sort__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
    BinToNary.HB_unnamed_factory_21 [def, in infotheo.probability.convex_equiv]
    BinToNary.HB_unnamed_factory_25 [def, in infotheo.probability.convex_equiv]
    BinToNary.HB_unnamed_mixin_23 [def, in infotheo.probability.convex_equiv]
    BinToNary.HB_unnamed_mixin_24 [def, in infotheo.probability.convex_equiv]
    BinToNary.HB_unnamed_mixin_27 [def, in infotheo.probability.convex_equiv]
    BinToNary.HB_unnamed_mixin_28 [def, in infotheo.probability.convex_equiv]
    BinToNaryToBin [mod, in infotheo.probability.convex_equiv]
    BinToNaryToBin._equiv_convn [prf, in infotheo.probability.convex_equiv]
    BinToNaryToBin.equiv_conv [prf, in infotheo.probability.convex_equiv]
    bipart [def, in infotheo.probability.partition_inequality]
    bipart_dominates [prf, in infotheo.probability.pinsker]
    bipart_pmf [def, in infotheo.probability.partition_inequality]
    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 [constr, in infotheo.ecc_modern.ldpc_erasure]
    Bit_col [prf, in infotheo.ecc_modern.ldpc_erasure]
    bitseq_of_N [def, in infotheo.lib.natbin]
    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 [def, 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 [def, 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]
    Blank [constr, in infotheo.ecc_modern.ldpc_erasure]
    blank_to_star [def, in infotheo.ecc_modern.ldpc_erasure]
    BN [mod, in infotheo.probability.bayes]
    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 [def, 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.indep [proj, in infotheo.probability.bayes]
    BN.independence [def, in infotheo.probability.bayes]
    BN.parent [proj, 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_vars [def, 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_vars [def, 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.t [rec, in infotheo.probability.bayes]
    BN.topo [proj, in infotheo.probability.bayes]
    BN.topological [def, in infotheo.probability.bayes]
    BN.vals0 [def, in infotheo.probability.bayes]
    BN.vals1to2 [def, in infotheo.probability.bayes]
    BN.vals_at [def, in infotheo.probability.bayes]
    BN.wrap_set_vals [def, in infotheo.probability.bayes]
    BN_factorization [prf, in infotheo.probability.bayes]
    bool_of_F2 [def, in infotheo.lib.f2]
    bool_of_F2_add_xor [prf, in infotheo.lib.f2]
    bool_of_F2K [prf, in infotheo.lib.f2]
    bool_of_kind [def, in infotheo.ecc_modern.ldpc_algo]
    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 [def, 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_intermediate [def, in infotheo.robust.weightedmean]
    bound_mean [prf, in infotheo.robust.weightedmean]
    bound_mean_emean [prf, in infotheo.robust.weightedmean]
    BSC [mod, in infotheo.information_theory.binary_symmetric_channel]
    BSC.c [def, in infotheo.information_theory.binary_symmetric_channel]
    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]
    bseq_take [def, in infotheo.lib.ssr_ext]
    bseqval_inj [prf, in infotheo.lib.ssr_ext]
    build_computed_tree [abbrev, in infotheo.ecc_modern.ldpc_algo_proof]
    build_computed_tree [def, in infotheo.ecc_modern.ldpc_algo]
    build_tree [def, in infotheo.ecc_modern.ldpc_algo]
    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 [def, in infotheo.ecc_modern.ldpc_algo]
    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 [mod, in infotheo.probability.convex_equiv]
    Builders_1.axbary [prf, in infotheo.probability.convex_equiv]
    Builders_1.axidem [abbrev, in infotheo.probability.convex_equiv]
    Builders_1.axpart [abbrev, in infotheo.probability.convex_equiv]
    Builders_1.axproj [prf, in infotheo.probability.convex_equiv]
    Builders_1.Builders_1_T__canonical__choice_Choice [def, in infotheo.probability.convex_equiv]
    Builders_1.Builders_1_T__canonical__convex_equiv_NaryConvexSpace [def, in infotheo.probability.convex_equiv]
    Builders_1.Builders_1_T__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
    Builders_1.Builders_1_T__canonical__eqtype_Equality [def, in infotheo.probability.convex_equiv]
    Builders_1.Builders_Export_5 [mod, in infotheo.probability.convex_equiv]
    Builders_1.HB_unnamed_factory_3 [def, in infotheo.probability.convex_equiv]
    Builders_1.Super [mod, in infotheo.probability.convex_equiv]
    Builders_11 [mod, in infotheo.probability.convex_equiv]
    Builders_11.axbary [prf, in infotheo.probability.convex_equiv]
    Builders_11.axbarypart [abbrev, in infotheo.probability.convex_equiv]
    Builders_11.axidem [abbrev, in infotheo.probability.convex_equiv]
    Builders_11.axproj [prf, in infotheo.probability.convex_equiv]
    Builders_11.Builders_11_T__canonical__choice_Choice [def, in infotheo.probability.convex_equiv]
    Builders_11.Builders_11_T__canonical__convex_equiv_NaryConvexSpace [def, in infotheo.probability.convex_equiv]
    Builders_11.Builders_11_T__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
    Builders_11.Builders_11_T__canonical__eqtype_Equality [def, in infotheo.probability.convex_equiv]
    Builders_11.Builders_Export_15 [mod, in infotheo.probability.convex_equiv]
    Builders_11.HB_unnamed_factory_13 [def, in infotheo.probability.convex_equiv]
    Builders_11.Super [mod, in infotheo.probability.convex_equiv]
    Builders_16 [mod, in infotheo.probability.convex_equiv]
    Builders_16.axconst [abbrev, in infotheo.probability.convex_equiv]
    Builders_16.axidem [prf, in infotheo.probability.convex_equiv]
    Builders_16.axpart [abbrev, in infotheo.probability.convex_equiv]
    Builders_16.axproj [abbrev, in infotheo.probability.convex_equiv]
    Builders_16.Builders_16_T__canonical__choice_Choice [def, in infotheo.probability.convex_equiv]
    Builders_16.Builders_16_T__canonical__convex_equiv_NaryConvexSpace [def, in infotheo.probability.convex_equiv]
    Builders_16.Builders_16_T__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
    Builders_16.Builders_16_T__canonical__eqtype_Equality [def, in infotheo.probability.convex_equiv]
    Builders_16.Builders_Export_20 [mod, in infotheo.probability.convex_equiv]
    Builders_16.convex_equiv_isNaryProjPartConstConvexSpace__to__convex_equiv_isNaryConvexSpace [def, in infotheo.probability.convex_equiv]
    Builders_16.HB_unnamed_factory_18 [def, in infotheo.probability.convex_equiv]
    Builders_16.Super [mod, in infotheo.probability.convex_equiv]
    Builders_31 [mod, in infotheo.probability.convex]
    Builders_31.Builders_31_T__canonical__choice_Choice [def, in infotheo.probability.convex]
    Builders_31.Builders_31_T__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
    Builders_31.Builders_31_T__canonical__eqtype_Equality [def, in infotheo.probability.convex]
    Builders_31.Builders_Export_35 [mod, in infotheo.probability.convex]
    Builders_31.conv [abbrev, in infotheo.probability.convex]
    Builders_31.conv1 [abbrev, in infotheo.probability.convex]
    Builders_31.convA [abbrev, in infotheo.probability.convex]
    Builders_31.convC [abbrev, in infotheo.probability.convex]
    Builders_31.convmm [abbrev, in infotheo.probability.convex]
    Builders_31.convn [def, in infotheo.probability.convex]
    Builders_31.HB_unnamed_factory_33 [def, in infotheo.probability.convex]
    Builders_31.Super [mod, in infotheo.probability.convex]
    Builders_6 [mod, in infotheo.probability.convex_equiv]
    Builders_6.axbary [abbrev, in infotheo.probability.convex_equiv]
    Builders_6.axconst [abbrev, in infotheo.probability.convex_equiv]
    Builders_6.axmap [abbrev, in infotheo.probability.convex_equiv]
    Builders_6.axproj [prf, in infotheo.probability.convex_equiv]
    Builders_6.Builders_6_T__canonical__choice_Choice [def, in infotheo.probability.convex_equiv]
    Builders_6.Builders_6_T__canonical__convex_equiv_NaryConvexSpace [def, in infotheo.probability.convex_equiv]
    Builders_6.Builders_6_T__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
    Builders_6.Builders_6_T__canonical__eqtype_Equality [def, in infotheo.probability.convex_equiv]
    Builders_6.Builders_Export_10 [mod, in infotheo.probability.convex_equiv]
    Builders_6.HB_unnamed_factory_8 [def, in infotheo.probability.convex_equiv]
    Builders_6.Super [mod, in infotheo.probability.convex_equiv]
    Generated by rocqnavi