C (Global Index)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
C
C1_is01 [prf, in infotheo.robust.weightedmean]C_not_empty [prf, in infotheo.ecc_classic.hamming_code]
cal_E [def, in infotheo.information_theory.channel_coding_direct]
cancel_both [def, in infotheo.probability.bayes]
cancel_on [def, in infotheo.ecc_classic.decoding]
canonical_cgen [def, in infotheo.ecc_classic.cyclic_code]
canonical_cgen_lowest_size [prf, in infotheo.ecc_classic.cyclic_code]
canonical_cgenP [prf, in infotheo.ecc_classic.cyclic_code]
capacity [def, in infotheo.information_theory.channel]
caratheodory [prf, in infotheo.probability.convex]
card_ball [def, in infotheo.ecc_classic.linearcode]
card_ballE [prf, in infotheo.ecc_classic.linearcode]
card_dH [prf, in infotheo.lib.hamming]
card_dH_vec [prf, in infotheo.lib.hamming]
card_dHC [prf, in infotheo.lib.hamming]
card_Fp_F2 [prf, in infotheo.lib.hamming]
card_GFqm [prf, in infotheo.lib.ssralg_ext]
card_le_TS_Lt [prf, in infotheo.information_theory.source_coding_vl_direct]
card_le_Xn_Lnt [prf, in infotheo.information_theory.source_coding_vl_direct]
card_le_Xn_Lnt' [prf, in infotheo.information_theory.source_coding_vl_direct]
card_nu [prf, in infotheo.information_theory.jtypes]
card_Psets [prf, in infotheo.ecc_modern.max_subset]
card_rV_wo_zeros [prf, in infotheo.lib.ssralg_ext]
card_shell_leq_exp_entropy [prf, in infotheo.information_theory.jtypes]
card_shelled_tuples [prf, in infotheo.information_theory.jtypes]
card_shelled_tuples_leq_prod_card [prf, in infotheo.information_theory.jtypes]
card_shelled_tuples_perm [prf, in infotheo.information_theory.jtypes]
card_sphere [prf, in infotheo.lib.hamming]
card_suffixes [prf, in infotheo.information_theory.kraft]
card_supp_fdistD1 [prf, in infotheo.probability.fdist]
card_take_shell [prf, in infotheo.information_theory.jtypes]
card_take_shell0 [prf, in infotheo.information_theory.jtypes]
card_take_shell_incl [prf, in infotheo.information_theory.jtypes]
card_take_shell_incl0 [prf, in infotheo.information_theory.jtypes]
card_type_of_row [def, in infotheo.information_theory.jtypes]
card_typed_tuples [prf, in infotheo.information_theory.types]
card_typed_tuples_alt [prf, in infotheo.information_theory.types]
card_uniq_seq_decr [prf, in infotheo.ecc_modern.ldpc_algo_proof]
card_wH_supp [prf, in infotheo.lib.hamming]
cardEP [prf, in infotheo.ecc_modern.degree_profile]
cards2P [prf, in infotheo.lib.ssr_ext]
cardsCp [prf, in infotheo.ecc_modern.degree_profile]
cardsltn1P [prf, in infotheo.lib.ssr_ext]
cast_cols [def, in infotheo.ecc_classic.linearcode]
cast_fun_rV1 [def, in infotheo.probability.proba]
cast_fun_rV10 [def, in infotheo.probability.proba]
cast_RV_fdist_rV1 [def, in infotheo.probability.proba]
cast_RV_fdist_rV10 [def, in infotheo.probability.proba]
castmx_cols_mulmx [prf, in infotheo.ecc_classic.linearcode]
castmx_cols_mulmx2 [prf, in infotheo.ecc_classic.linearcode]
castmx_mulmx_cols_comm [prf, in infotheo.ecc_classic.linearcode]
Cauchy_Schwarz_proba [prf, in infotheo.robust.robustmean]
Ccode [mod, in infotheo.ecc_classic.cyclic_code]
Ccode.lcode0 [proj, in infotheo.ecc_classic.cyclic_code]
Ccode.P [proj, in infotheo.ecc_classic.cyclic_code]
Ccode.t [rec, in infotheo.ecc_classic.cyclic_code]
ccode_coercion [def, in infotheo.ecc_classic.cyclic_code]
cdiv [def, in infotheo.information_theory.conditional_divergence]
cdiv0P [prf, in infotheo.information_theory.conditional_divergence]
cdiv1 [def, in infotheo.information_theory.entropy]
cdiv1_ge0 [prf, in infotheo.information_theory.entropy]
cdiv1_is_div [prf, in infotheo.information_theory.entropy]
cdiv_ge0 [prf, in infotheo.information_theory.conditional_divergence]
cdiv_is_div_joint_dist [prf, in infotheo.information_theory.conditional_divergence]
cdom_by [def, in infotheo.information_theory.conditional_divergence]
centropy [def, in infotheo.information_theory.entropy]
centropy1 [def, in infotheo.information_theory.entropy]
centropy1_fdistAC [prf, in infotheo.information_theory.entropy]
centropy1_ge0 [prf, in infotheo.information_theory.entropy]
centropy1_RV [def, in infotheo.information_theory.entropy]
centropy1_RV_comp0 [prf, in infotheo.information_theory.entropy]
centropy1_RV_fdistAC [prf, in infotheo.information_theory.entropy]
centropy1_RV_ge0 [prf, in infotheo.information_theory.entropy]
centropy1_RVE [prf, in infotheo.information_theory.entropy]
centropy_fdistA [prf, in infotheo.information_theory.entropy]
centropy_ge0 [prf, in infotheo.information_theory.entropy]
centropy_indep [prf, in infotheo.information_theory.entropy]
centropy_RV [def, in infotheo.information_theory.entropy]
centropy_RV_comp0 [prf, in infotheo.information_theory.entropy]
centropy_RV_contraction [prf, in infotheo.information_theory.entropy]
centropy_RV_fdistA [prf, in infotheo.information_theory.entropy]
centropy_RV_ge0 [prf, in infotheo.information_theory.entropy]
centropy_RVE [prf, in infotheo.information_theory.entropy]
centropy_RVE' [prf, in infotheo.information_theory.entropy]
centropyC [prf, in infotheo.information_theory.entropy]
centropyE [prf, in infotheo.information_theory.entropy]
cEx [def, in infotheo.probability.proba]
cEx_add_RV [prf, in infotheo.robust.robustmean]
cEx_const_RV [prf, in infotheo.robust.robustmean]
cEx_cptl [prf, in infotheo.robust.robustmean]
cEx_cVar [prf, in infotheo.robust.robustmean]
cEx_ExInd [prf, in infotheo.robust.robustmean]
cEx_Inv [prf, in infotheo.robust.robustmean]
cEx_Inv' [prf, in infotheo.robust.robustmean]
cEx_Inv_int [prf, in infotheo.robust.robustmean]
cEx_Pr_eq0 [prf, in infotheo.robust.robustmean]
cEx_scalel_RV [prf, in infotheo.robust.robustmean]
cEx_sub [prf, in infotheo.robust.robustmean]
cEx_sub_eq [prf, in infotheo.robust.robustmean]
cEx_sub_RV [prf, in infotheo.robust.robustmean]
cEx_trans_add_RV [prf, in infotheo.robust.robustmean]
cEx_trans_RV_id_rem [prf, in infotheo.robust.robustmean]
cEx_trans_sub_RV [prf, in infotheo.robust.robustmean]
cEx_union [prf, in infotheo.robust.robustmean]
cEx_Var [prf, in infotheo.robust.robustmean]
cExE [prf, in infotheo.robust.robustmean]
cExID [prf, in infotheo.robust.robustmean]
cgen_dim [prf, in infotheo.ecc_classic.cyclic_code]
cgen_divides_Xn_sub_1 [prf, in infotheo.ecc_classic.cyclic_code]
cgen_is_pgen [prf, in infotheo.ecc_classic.cyclic_code]
chain_rule [prf, in infotheo.information_theory.entropy]
chain_rule_corollary [prf, in infotheo.information_theory.entropy]
chain_rule_information [prf, in infotheo.information_theory.entropy]
chain_rule_multivar [prf, in infotheo.information_theory.entropy]
chain_rule_mutual_info [prf, in infotheo.information_theory.entropy]
chain_rule_relative_entropy [prf, in infotheo.information_theory.entropy]
chain_rule_rV [prf, in infotheo.information_theory.entropy]
chain_rule_RV [prf, in infotheo.information_theory.entropy]
chaining_rule [prf, in infotheo.probability.graphoid]
chan_of_jtype [def, in infotheo.information_theory.jtypes]
chan_star_coercion [def, in infotheo.information_theory.channel]
change_dist [def, in infotheo.robust.weightedmean]
channel [file, in infotheo.information_theory.channel]
Channel1 [mod, in infotheo.information_theory.channel]
Channel1.c [proj, in infotheo.information_theory.channel]
Channel1.chan_star [rec, in infotheo.information_theory.channel]
Channel1.chan_star_eq [prf, in infotheo.information_theory.channel]
Channel1.input_not_0 [proj, in infotheo.information_theory.channel]
channel_code [file, in infotheo.information_theory.channel_code]
channel_coding [prf, in infotheo.information_theory.channel_coding_direct]
channel_coding_converse [file, in infotheo.information_theory.channel_coding_converse]
channel_coding_converse [prf, in infotheo.information_theory.channel_coding_converse]
channel_coding_converse_gen [prf, in infotheo.information_theory.channel_coding_converse]
channel_coding_direct [file, in infotheo.information_theory.channel_coding_direct]
channel_jcPr [prf, in infotheo.information_theory.channel]
char_GFqm [prf, in infotheo.lib.ssralg_ext]
charac_bdist [prf, in infotheo.probability.fdist]
chebyshev_inequality [prf, in infotheo.probability.proba]
checksubsum [def, in infotheo.ecc_modern.checksum]
checksubsum_add [prf, in infotheo.ecc_modern.ldpc_algo_proof]
checksubsum_D1 [prf, in infotheo.ecc_modern.checksum]
checksubsum_dproj [prf, in infotheo.ecc_modern.summary_tanner]
checksubsum_dproj_freeon [prf, in infotheo.ecc_modern.summary_tanner]
checksubsum_dprojD1 [prf, in infotheo.ecc_modern.summary_tanner]
checksubsum_dprojs_V [prf, in infotheo.ecc_modern.summary_tanner]
checksubsum_dprojs_V2 [prf, in infotheo.ecc_modern.summary_tanner]
checksubsum_in_kernel [prf, in infotheo.ecc_modern.checksum]
checksubsum_set1 [prf, in infotheo.ecc_modern.checksum]
checksubsum_set2 [prf, in infotheo.ecc_modern.checksum]
checksum [file, in infotheo.ecc_modern.checksum]
children [proj, in infotheo.ecc_modern.ldpc_algo]
children_ind [prf, in infotheo.ecc_modern.ldpc_algo_proof]
choice_Choice__to__choice_hasChoice [def, in infotheo.probability.fsdist]
choice_Choice__to__choice_hasChoice [def, in infotheo.probability.fdist]
choice_Choice__to__choice_hasChoice [def, in infotheo.probability.convex]
choice_Choice__to__eqtype_hasDecEq [def, in infotheo.probability.fdist]
choice_Choice__to__eqtype_hasDecEq [def, in infotheo.probability.convex]
choice_isCountable__to__choice_Choice_isCountable [def, in infotheo.information_theory.types]
choice_isCountable__to__choice_Choice_isCountable [def, in infotheo.information_theory.jtypes]
choice_isCountable__to__choice_Choice_isCountable [def, in infotheo.ecc_modern.ldpc_erasure]
choice_isCountable__to__choice_Choice_isCountable__14 [def, in infotheo.information_theory.jtypes]
choice_isCountable__to__choice_hasChoice [def, in infotheo.information_theory.types]
choice_isCountable__to__choice_hasChoice [def, in infotheo.information_theory.jtypes]
choice_isCountable__to__choice_hasChoice [def, in infotheo.ecc_modern.ldpc_erasure]
choice_isCountable__to__choice_hasChoice__16 [def, in infotheo.information_theory.jtypes]
choice_isCountable__to__eqtype_hasDecEq [def, in infotheo.information_theory.types]
choice_isCountable__to__eqtype_hasDecEq [def, in infotheo.information_theory.jtypes]
choice_isCountable__to__eqtype_hasDecEq__18 [def, in infotheo.information_theory.jtypes]
cinde_alt [prf, in infotheo.probability.proba]
cinde_drv_2C [prf, in infotheo.probability.graphoid]
cinde_drv_3C [prf, in infotheo.probability.graphoid]
cinde_events [def, in infotheo.probability.proba]
cinde_events_alt [prf, in infotheo.probability.proba]
cinde_events_unit [prf, in infotheo.probability.proba]
cinde_rv [abbrev, in infotheo.probability.proba]
cinde_RV [def, in infotheo.probability.proba]
cinde_rv_events [abbrev, in infotheo.probability.proba]
cinde_RV_events [prf, in infotheo.probability.proba]
cinde_rv_sym [abbrev, in infotheo.probability.proba]
cinde_RV_sym [prf, in infotheo.probability.proba]
cinde_rv_unit [abbrev, in infotheo.probability.proba]
cinde_RV_unit [prf, in infotheo.probability.proba]
classical_sets_bigcup__canonical__necset_NESet [def, in infotheo.probability.necset]
classical_sets_ext [file, in infotheo.lib.classical_sets_ext]
classical_sets_image__canonical__necset_NESet [def, in infotheo.probability.necset]
classical_sets_set0__canonical__convex_ConvexSet [def, in infotheo.probability.convex]
classical_sets_set1__canonical__convex_ConvexSet [def, in infotheo.probability.convex]
classical_sets_set1__canonical__necset_NECSet [def, in infotheo.probability.necset]
classical_sets_set1__canonical__necset_NESet [def, in infotheo.probability.necset]
classical_sets_setU__canonical__necset_NESet [def, in infotheo.probability.necset]
classify_big [prf, in infotheo.lib.bigop_ext]
code [rec, in infotheo.information_theory.channel_code]
code_set [rec, in infotheo.information_theory.kraft]
code_set_cw [rec, in infotheo.information_theory.kraft]
code_set_cw_of_code_set [def, in infotheo.information_theory.kraft]
code_set_of_code_set_cw [def, in infotheo.information_theory.kraft]
code_set_predType [def, in infotheo.information_theory.kraft]
CodeErrRate [def, in infotheo.information_theory.channel_code]
CodeRate [def, in infotheo.information_theory.channel_code]
CodeRateType [rec, in infotheo.information_theory.channel_code]
codeset [proj, in infotheo.information_theory.kraft]
codesetcw [proj, in infotheo.information_theory.kraft]
codeword_lowest_deg [def, in infotheo.ecc_classic.linearcode]
CodomDFDist [mod, in infotheo.probability.fdist]
CodomDFDist.d [def, in infotheo.probability.fdist]
CodomDFDist.d' [def, in infotheo.probability.fdist]
CodomDFDist.dE [prf, in infotheo.probability.fdist]
CodomDFDist.dE' [prf, in infotheo.probability.fdist]
CodomDFDist.f [def, in infotheo.probability.fdist]
CodomDFDist.f0 [prf, in infotheo.probability.fdist]
CodomDFDist.f1 [prf, in infotheo.probability.fdist]
CodomDFDist.f1' [prf, in infotheo.probability.fdist]
col_matrix [prf, in infotheo.lib.ssralg_ext]
col_of_bitseq [def, in infotheo.lib.ssralg_ext]
col_of_seq [def, in infotheo.lib.ssralg_ext]
col_perm_inj [prf, in infotheo.lib.ssralg_ext]
colFnext [def, in infotheo.ecc_modern.ldpc_erasure]
ColFnext [def, in infotheo.ecc_modern.ldpc_erasure]
colFnextD1 [def, in infotheo.ecc_modern.ldpc_erasure]
Colorable [mod, in infotheo.ecc_modern.subgraph_partition]
colorable [def, in infotheo.ecc_modern.subgraph_partition]
Colorable.graph [rec, in infotheo.ecc_modern.subgraph_partition]
Colorable.kind [proj, in infotheo.ecc_modern.subgraph_partition]
Colorable.prop [proj, in infotheo.ecc_modern.subgraph_partition]
colorable_is_simple [prf, in infotheo.ecc_modern.subgraph_partition]
colorable_path_kind [prf, in infotheo.ecc_modern.subgraph_partition]
colorable_tanner_rel [prf, in infotheo.ecc_modern.tanner]
cols_starblank [def, in infotheo.ecc_modern.stopping_set]
cols_starblank_mxProd [prf, in infotheo.ecc_modern.stopping_set]
cols_starblank_PCM_instance_erasures [prf, in infotheo.ecc_modern.stopping_set]
comb [def, in infotheo.ecc_modern.summary_tanner]
comb_dprojs [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_not_in_partition [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_V [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_V2 [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_V2_in_partition [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_V2_not_in_subgraph [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_V2_Vnext [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_V2_Vnext_dangling [prf, in infotheo.ecc_modern.summary_tanner]
comb_dprojs_V_not_in_partition [prf, in infotheo.ecc_modern.summary_tanner]
comb_in [prf, in infotheo.ecc_modern.summary_tanner]
comb_out [prf, in infotheo.ecc_modern.summary_tanner]
comb_V [def, in infotheo.ecc_modern.summary_tanner]
comb_V2 [def, in infotheo.ecc_modern.summary_tanner]
comb_V2_freeon [prf, in infotheo.ecc_modern.summary_tanner]
comb_V_in [prf, in infotheo.ecc_modern.summary_tanner]
comb_V_support [prf, in infotheo.ecc_modern.summary_tanner]
comp_RV [def, in infotheo.probability.proba]
comp_RVE [prf, in infotheo.probability.proba]
compfid [prf, in infotheo.lib.ssr_ext]
computed_tree_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
computed_tree_spec [def, in infotheo.ecc_modern.ldpc_algo]
concats_entropy [prf, in infotheo.information_theory.string_entropy]
concave_function [def, in infotheo.probability.convex]
concave_function_at [def, in infotheo.probability.convex]
concave_function_at' [def, in infotheo.probability.convex]
concave_function_at'P [prf, in infotheo.probability.convex]
concave_function_atN [prf, in infotheo.probability.convex]
concave_function_atxx [prf, in infotheo.probability.convex]
concave_function_in [def, in infotheo.probability.convex]
concave_functionP [def, in infotheo.probability.convex]
concavef_at_onem [prf, in infotheo.probability.convex]
ConcaveFunction [abbrev, in infotheo.probability.convex]
ConcaveFunction [mod, in infotheo.probability.convex]
ConcaveFunction.axioms_ [rec, in infotheo.probability.convex]
ConcaveFunction.class [proj, in infotheo.probability.convex]
ConcaveFunction.clone [abbrev, in infotheo.probability.convex]
ConcaveFunction.convex_isConcaveFunction_mixin [proj, in infotheo.probability.convex]
ConcaveFunction.copy [abbrev, in infotheo.probability.convex]
ConcaveFunction.Exports [mod, in infotheo.probability.convex]
ConcaveFunction.on [abbrev, in infotheo.probability.convex]
ConcaveFunction.on_ [abbrev, in infotheo.probability.convex]
ConcaveFunction.pack_ [def, in infotheo.probability.convex]
ConcaveFunction.phant_clone [def, in infotheo.probability.convex]
ConcaveFunction.phant_on_ [def, in infotheo.probability.convex]
ConcaveFunction.sort [proj, in infotheo.probability.convex]
ConcaveFunction.type [rec, in infotheo.probability.convex]
ConcaveFunctionElpiOperations [mod, in infotheo.probability.convex]
cond_entropy [abbrev, in infotheo.information_theory.entropy]
cond_entropy1 [abbrev, in infotheo.information_theory.entropy]
cond_entropy1_fdistAC [abbrev, in infotheo.information_theory.entropy]
cond_entropy1_ge0 [abbrev, in infotheo.information_theory.entropy]
cond_entropy_chan [def, in infotheo.information_theory.channel]
cond_entropy_chanE [prf, in infotheo.information_theory.channel]
cond_entropy_chanE2 [prf, in infotheo.information_theory.channel]
cond_entropy_fdistA [abbrev, in infotheo.information_theory.entropy]
cond_entropy_ge0E [abbrev, in infotheo.information_theory.entropy]
cond_entropy_self [prf, in infotheo.information_theory.entropy]
cond_entropyE [abbrev, in infotheo.information_theory.entropy]
cond_mutual_info [def, in infotheo.information_theory.entropy]
cond_mutual_info_ge0 [prf, in infotheo.information_theory.entropy]
cond_mutual_infoE [prf, in infotheo.information_theory.entropy]
cond_mutual_infoE2 [prf, in infotheo.information_theory.entropy]
cond_relative_entropy [def, in infotheo.information_theory.entropy]
cond_relative_entropy_compat [prf, in infotheo.information_theory.conditional_divergence]
cond_type [def, in infotheo.information_theory.jtypes]
cond_type_equiv [prf, in infotheo.information_theory.jtypes]
conditional_divergence [file, in infotheo.information_theory.conditional_divergence]
conditional_entropy [file, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example [mod, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.conditional_entropyE [prf, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.d [def, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.dE [prf, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.f [def, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.f0 [prf, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.f1 [prf, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.one [def, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.three [def, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.two [def, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.zero [def, in infotheo.toy_examples.conditional_entropy]
connect_except [prf, in infotheo.ecc_modern.subgraph_partition]
connect_sym [prf, in infotheo.lib.ssr_ext]
connect_sym1 [prf, in infotheo.lib.ssr_ext]
cons_tuple_inj [prf, in infotheo.ecc_modern.degree_profile]
cons_tuples [def, in infotheo.information_theory.jtypes]
cons_uniq_path [prf, in infotheo.lib.ssr_ext]
const_RC [prf, in infotheo.robust.robustmean]
const_RV [def, in infotheo.probability.proba]
const_RVE [prf, in infotheo.probability.proba]
continuous_at_diff_xlnx [prf, in infotheo.lib.realType_ln]
continuous_at_xlnx [prf, in infotheo.lib.realType_ln]
continuous_at_xlnx_delta [prf, in infotheo.lib.realType_ln]
continuous_at_xlnx_total [prf, in infotheo.lib.realType_ln]
continuous_H2 [prf, in infotheo.lib.binary_entropy_function]
continuous_id [prf, in infotheo.lib.binary_entropy_function]
continuous_log [prf, in infotheo.lib.binary_entropy_function]
continuous_onem [prf, in infotheo.lib.binary_entropy_function]
contraction [prf, in infotheo.probability.graphoid]
conv [def, in infotheo.probability.convex]
conv0 [prf, in infotheo.probability.convex]
conv0_pt_set [prf, in infotheo.probability.necset]
conv0_set [prf, in infotheo.probability.necset]
conv1 [def, in infotheo.probability.convex]
conv1_pt_set [prf, in infotheo.probability.necset]
conv1_set [prf, in infotheo.probability.necset]
conv_cset1 [prf, in infotheo.probability.necset]
conv_cset_is_convex [prf, in infotheo.probability.necset]
conv_in_conv_pt_set [prf, in infotheo.probability.necset]
conv_in_conv_set [prf, in infotheo.probability.necset]
conv_in_conv_set' [prf, in infotheo.probability.necset]
conv_in_oplus_conv_set [prf, in infotheo.probability.necset]
conv_leoppD [prf, in infotheo.probability.convex]
conv_pt_set [def, in infotheo.probability.necset]
conv_pt_set_monotone [prf, in infotheo.probability.necset]
conv_pt_set_neq0 [prf, in infotheo.probability.necset]
conv_pt_setE [prf, in infotheo.probability.necset]
conv_set [def, in infotheo.probability.necset]
conv_set_monotone [prf, in infotheo.probability.necset]
conv_set_neq0 [prf, in infotheo.probability.necset]
conv_setE [prf, in infotheo.probability.necset]
convA [def, in infotheo.probability.convex]
convA' [prf, in infotheo.probability.convex]
convA0 [prf, in infotheo.probability.convex]
convA_pt_set [prf, in infotheo.probability.necset]
convA_set [prf, in infotheo.probability.necset]
convACA [prf, in infotheo.probability.convex]
convACA' [prf, in infotheo.probability.convex]
convC [def, in infotheo.probability.convex]
convC_set [prf, in infotheo.probability.necset]
convDr [prf, in infotheo.probability.convex]
converse_case1 [prf, in infotheo.information_theory.source_coding_vl_converse]
converse_case2 [prf, in infotheo.information_theory.source_coding_vl_converse]
convex [file, in infotheo.probability.convex]
convex_addpt__canonical__Monoid_ComLaw [def, in infotheo.probability.convex]
convex_addpt__canonical__Monoid_Law [def, in infotheo.probability.convex]
convex_addpt__canonical__SemiGroup_ComLaw [def, in infotheo.probability.convex]
convex_addpt__canonical__SemiGroup_Law [def, in infotheo.probability.convex]
convex_ConvexSet__to__convex_isConvexSet [def, in infotheo.probability.necset]
convex_div [prf, in infotheo.information_theory.entropy_convex]
convex_equiv [file, in infotheo.probability.convex_equiv]
convex_function [def, in infotheo.probability.convex]
convex_function_at [def, in infotheo.probability.convex]
convex_function_at_Convn [def, in infotheo.probability.convex]
convex_function_atxx [prf, in infotheo.probability.convex]
convex_function_comp [prf, in infotheo.probability.convex]
convex_function_comp' [prf, in infotheo.probability.convex]
convex_function_in [def, in infotheo.probability.convex]
convex_function_sym [prf, in infotheo.probability.convex]
convex_functionP [def, in infotheo.probability.convex]
convex_hull__canonical__convex_ConvexSet [def, in infotheo.probability.convex]
convex_hull__canonical__necset_NECSet [def, in infotheo.probability.necset]
convex_hull__canonical__necset_NESet [def, in infotheo.probability.necset]
convex_in_both [def, in infotheo.probability.convex]
convex_in_bothP [prf, in infotheo.probability.convex]
convex_isConvexSet__to__convex_isConvexSet [def, in infotheo.probability.necset]
convex_isConvexSet__to__convex_isConvexSet__64 [def, in infotheo.probability.necset]
convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.necset]
convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.fsdist]
convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex_equiv]
convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.information_theory.entropy_convex]
convex_map_scaled__canonical__convex_Affine [def, in infotheo.probability.convex]
convex_OrderedConvexSpace__to__choice_hasChoice [def, in infotheo.probability.convex]
convex_OrderedConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
convex_OrderedConvexSpace__to__eqtype_hasDecEq [def, in infotheo.probability.convex]
convex_relative_entropy [prf, in infotheo.information_theory.entropy_convex]
convex_Rnonneg_interval__canonical__convex_ConvexSet [def, in infotheo.probability.convex]
convex_Rpos_interval__canonical__convex_ConvexSet [def, in infotheo.probability.convex]
convex_S1__canonical__convex_Affine [def, in infotheo.probability.convex]
convex_scaled__canonical__choice_Choice [def, in infotheo.probability.convex]
convex_scaled__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
convex_scaled__canonical__convex_QuasiRealCone [def, in infotheo.probability.convex]
convex_scaled__canonical__convex_RealCone [def, in infotheo.probability.convex]
convex_scaled__canonical__eqtype_Equality [def, in infotheo.probability.convex]
convex_segment__canonical__convex_ConvexSet [def, in infotheo.probability.convex]
convex_setP [prf, in infotheo.probability.convex]
convex_stone [file, in infotheo.probability.convex_stone]
convex_uniti__canonical__convex_ConvexSet [def, in infotheo.probability.convex]
convexf_at_onem [prf, in infotheo.probability.convex]
ConvexFunction [abbrev, in infotheo.probability.convex]
ConvexFunction [mod, in infotheo.probability.convex]
ConvexFunction.axioms_ [rec, in infotheo.probability.convex]
ConvexFunction.class [proj, in infotheo.probability.convex]
ConvexFunction.clone [abbrev, in infotheo.probability.convex]
ConvexFunction.convex_isConvexFunction_mixin [proj, in infotheo.probability.convex]
ConvexFunction.copy [abbrev, in infotheo.probability.convex]
ConvexFunction.Exports [mod, in infotheo.probability.convex]
ConvexFunction.on [abbrev, in infotheo.probability.convex]
ConvexFunction.on_ [abbrev, in infotheo.probability.convex]
ConvexFunction.pack_ [def, in infotheo.probability.convex]
ConvexFunction.phant_clone [def, in infotheo.probability.convex]
ConvexFunction.phant_on_ [def, in infotheo.probability.convex]
ConvexFunction.sort [proj, in infotheo.probability.convex]
ConvexFunction.type [rec, in infotheo.probability.convex]
ConvexFunctionElpiOperations [mod, in infotheo.probability.convex]
ConvexSet [abbrev, in infotheo.probability.convex]
ConvexSet [mod, in infotheo.probability.convex]
ConvexSet.axioms_ [rec, in infotheo.probability.convex]
ConvexSet.class [proj, in infotheo.probability.convex]
ConvexSet.clone [abbrev, in infotheo.probability.convex]
ConvexSet.convex_isConvexSet_mixin [proj, in infotheo.probability.convex]
ConvexSet.copy [abbrev, in infotheo.probability.convex]
ConvexSet.Exports [mod, in infotheo.probability.convex]
ConvexSet.on [abbrev, in infotheo.probability.convex]
ConvexSet.on_ [abbrev, in infotheo.probability.convex]
ConvexSet.pack_ [def, in infotheo.probability.convex]
ConvexSet.phant_clone [def, in infotheo.probability.convex]
ConvexSet.phant_on_ [def, in infotheo.probability.convex]
ConvexSet.sort [proj, in infotheo.probability.convex]
ConvexSet.type [rec, in infotheo.probability.convex]
ConvexSet_type__canonical__eqtype_Equality [def, in infotheo.probability.convex]
ConvexSetElpiOperations [mod, in infotheo.probability.convex]
ConvexSpace [abbrev, in infotheo.probability.convex]
ConvexSpace [mod, in infotheo.probability.convex]
ConvexSpace.axioms_ [rec, in infotheo.probability.convex]
ConvexSpace.choice_hasChoice_mixin [proj, in infotheo.probability.convex]
ConvexSpace.class [proj, in infotheo.probability.convex]
ConvexSpace.clone [abbrev, in infotheo.probability.convex]
ConvexSpace.convex_isConvexSpace0_mixin [proj, in infotheo.probability.convex]
ConvexSpace.copy [abbrev, in infotheo.probability.convex]
ConvexSpace.eqtype_hasDecEq_mixin [proj, in infotheo.probability.convex]
ConvexSpace.Exports [mod, in infotheo.probability.convex]
ConvexSpace.Exports.convex_ConvexSpace__to__choice_Choice [def, in infotheo.probability.convex]
ConvexSpace.Exports.convex_ConvexSpace__to__eqtype_Equality [def, in infotheo.probability.convex]
ConvexSpace.Exports.convex_ConvexSpace_class__to__choice_Choice_class [def, in infotheo.probability.convex]
ConvexSpace.Exports.convex_ConvexSpace_class__to__eqtype_Equality_class [def, in infotheo.probability.convex]
ConvexSpace.Exports.convType [abbrev, in infotheo.probability.convex]
ConvexSpace.on [abbrev, in infotheo.probability.convex]
ConvexSpace.on_ [abbrev, in infotheo.probability.convex]
ConvexSpace.pack_ [def, in infotheo.probability.convex]
ConvexSpace.phant_clone [def, in infotheo.probability.convex]
ConvexSpace.phant_on_ [def, in infotheo.probability.convex]
ConvexSpace.sort [proj, in infotheo.probability.convex]
ConvexSpace.type [rec, in infotheo.probability.convex]
ConvexSpaceElpiOperations [mod, in infotheo.probability.convex]
convmm [def, in infotheo.probability.convex]
convmm_cset [prf, in infotheo.probability.necset]
convn [def, in infotheo.probability.convex_equiv]
convn [def, in infotheo.probability.convex]
Convn [def, in infotheo.probability.convex]
Convn_comp [prf, in infotheo.probability.convex]
convn_convnfdist [prf, in infotheo.probability.convex_stone]
Convn_cst [prf, in infotheo.probability.convex]
Convn_fdist1 [prf, in infotheo.probability.convex]
convn_fdist1 [prf, in infotheo.probability.convex]
Convn_fdist_convn [prf, in infotheo.probability.convex]
Convn_finType [mod, in infotheo.probability.convex]
Convn_finType.Convn_finType [def, in infotheo.probability.convex]
Convn_finType.d [def, in infotheo.probability.convex]
Convn_finType.d_enum [def, in infotheo.probability.convex]
Convn_finType.d_enum0 [prf, in infotheo.probability.convex]
Convn_finType.d_enum1 [prf, in infotheo.probability.convex]
Convn_finType.Exports [mod, in infotheo.probability.convex]
Convn_finType.t0 [def, in infotheo.probability.convex]
Convn_idem [prf, in infotheo.probability.convex]
Convn_iter_conv_set [prf, in infotheo.probability.necset]
Convn_of_fsdist [def, in infotheo.probability.fsdist]
Convn_of_fsdist1 [prf, in infotheo.probability.fsdist]
Convn_of_fsdist_affine [prf, in infotheo.probability.fsdist]
Convn_of_fsdistjoin [prf, in infotheo.probability.fsdist]
Convn_of_fsdistmap [prf, in infotheo.probability.fsdist]
Convn_perm [prf, in infotheo.probability.convex_stone]
Convn_perm [prf, in infotheo.probability.convex]
Convn_perm_1 [prf, in infotheo.probability.convex_stone]
Convn_perm_projection [prf, in infotheo.probability.convex_stone]
Convn_perm_tperm [prf, in infotheo.probability.convex_stone]
Convn_permI1 [prf, in infotheo.probability.convex_stone]
Convn_permI2 [prf, in infotheo.probability.convex_stone]
Convn_permI3 [prf, in infotheo.probability.convex_stone]
Convn_permI3_p01 [prf, in infotheo.probability.convex_stone]
Convn_permI3_p02 [prf, in infotheo.probability.convex_stone]
Convn_proj [prf, in infotheo.probability.convex]
Convn_weak [prf, in infotheo.probability.convex]
ConvnDl [prf, in infotheo.probability.convex]
ConvnDlr [prf, in infotheo.probability.convex]
ConvnDr [prf, in infotheo.probability.convex]
convnE [def, in infotheo.probability.convex]
ConvnI1_eq [prf, in infotheo.probability.convex]
ConvnI1_eq_rect [prf, in infotheo.probability.convex]
ConvnI1E [prf, in infotheo.probability.convex]
convnI1E [prf, in infotheo.probability.convex]
ConvnI2E [prf, in infotheo.probability.convex]
convnI2E [prf, in infotheo.probability.convex]
ConvnI3E [prf, in infotheo.probability.convex_stone]
ConvnIE [prf, in infotheo.probability.convex]
convnIE [prf, in infotheo.probability.convex]
convptE [prf, in infotheo.probability.convex]
coprime_errloc_erreval [prf, in infotheo.ecc_classic.poly_decoding]
coqRE [file, in infotheo.lib.coqRE]
coqRE [def, in infotheo.lib.coqRE]
count_sumn [prf, in infotheo.lib.ssr_ext]
counterexample_bary_const_noproj [mod, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.axbary [prf, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.axconst [prf, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.Datatypes_bool__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.HB_unnamed_factory_48 [def, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.noproj [prf, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.proj_1st [def, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.test [def, in infotheo.probability.convex_equiv]
counterexample_bary_const_noproj.test [def, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj [mod, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.axconst [prf, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.axpart [prf, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.bigand [def, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.Datatypes_bool__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.HB_unnamed_factory_52 [def, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.noproj [prf, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.test [def, in infotheo.probability.convex_equiv]
counterexample_part_const_noproj.test [def, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem [mod, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.axpart [prf, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.axproj [prf, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.Datatypes_nat__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.HB_unnamed_factory_50 [def, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.noconst [prf, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.noidem [prf, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.test [def, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.test [def, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.weight1_sum [def, in infotheo.probability.convex_equiv]
Cov [def, in infotheo.robust.robustmean]
cover_enc_pre_img [prf, in infotheo.information_theory.types]
cover_Fgraph_part_Fgraph [prf, in infotheo.ecc_modern.tanner_partition]
cover_Fgraph_part_fnode [prf, in infotheo.ecc_modern.tanner_partition]
cover_set_set_co_occ [prf, in infotheo.lib.num_occ]
cover_shell [prf, in infotheo.information_theory.jtypes]
cover_subgraph_succ [prf, in infotheo.ecc_modern.subgraph_partition]
cover_subgraph_succ2_D1 [prf, in infotheo.ecc_modern.subgraph_partition]
cover_subgraph_succ_D1 [prf, in infotheo.ecc_modern.subgraph_partition]
cover_Vgraph_part_Vgraph [prf, in infotheo.ecc_modern.tanner_partition]
cover_Vgraph_part_vnode [prf, in infotheo.ecc_modern.tanner_partition]
covered_by [def, in infotheo.ecc_modern.max_subset]
covered_by_maxset [prf, in infotheo.ecc_modern.max_subset]
cplt_S [abbrev, in infotheo.robust.weightedmean]
cplt_S [abbrev, in infotheo.robust.weightedmean]
cplt_S [abbrev, in infotheo.robust.weightedmean]
cplt_S [abbrev, in infotheo.robust.weightedmean]
cplt_S [abbrev, in infotheo.robust.weightedmean]
cPr [def, in infotheo.probability.proba]
cPr_1 [prf, in infotheo.probability.jfdist_cond]
cPr_centropy1_RV_comp [prf, in infotheo.information_theory.entropy]
cPr_centropy_RV_comp [prf, in infotheo.information_theory.entropy]
cPr_cplt [prf, in infotheo.probability.proba]
cPr_diff [abbrev, in infotheo.probability.proba]
cPr_eq [def, in infotheo.probability.proba]
cpr_eq0 [abbrev, in infotheo.probability.proba]
cPr_eq0 [abbrev, in infotheo.probability.proba]
cPr_eq0P [prf, in infotheo.probability.proba]
cPr_eq_def [prf, in infotheo.probability.proba]
cPr_eq_finType [prf, in infotheo.probability.proba]
cPr_eq_id [prf, in infotheo.probability.proba]
cpr_eq_pairA [prf, in infotheo.probability.proba]
cpr_eq_pairAC [prf, in infotheo.probability.proba]
cpr_eq_pairACr [prf, in infotheo.probability.proba]
cpr_eq_pairAr [prf, in infotheo.probability.proba]
cpr_eq_pairC [prf, in infotheo.probability.proba]
cpr_eq_pairCr [prf, in infotheo.probability.proba]
cpr_eq_product_rule [prf, in infotheo.probability.proba]
cpr_eq_set [abbrev, in infotheo.probability.proba]
cpr_eq_set1 [abbrev, in infotheo.probability.proba]
cpr_eq_setE [abbrev, in infotheo.probability.proba]
cpr_eq_unit_RV [prf, in infotheo.probability.proba]
cpr_eqE [prf, in infotheo.probability.proba]
cpr_eqE' [abbrev, in infotheo.probability.proba]
cPr_ge0 [prf, in infotheo.probability.proba]
cPr_gt0P [abbrev, in infotheo.probability.proba]
cpr_in [def, in infotheo.probability.proba]
cpr_in1 [prf, in infotheo.probability.proba]
cpr_in_pairA [prf, in infotheo.probability.proba]
cpr_in_pairAC [prf, in infotheo.probability.proba]
cpr_in_pairACr [prf, in infotheo.probability.proba]
cpr_in_pairAr [prf, in infotheo.probability.proba]
cpr_in_pairC [prf, in infotheo.probability.proba]
cpr_in_pairCr [prf, in infotheo.probability.proba]
cpr_in_unit_RV [prf, in infotheo.probability.proba]
cpr_inE [prf, in infotheo.probability.proba]
cpr_inE' [prf, in infotheo.probability.proba]
cpr_inEdiv [prf, in infotheo.probability.proba]
cPr_le1 [prf, in infotheo.probability.proba]
cPr_max [abbrev, in infotheo.probability.proba]
cPr_setD [prf, in infotheo.probability.proba]
cPr_setU [prf, in infotheo.probability.proba]
cPr_union_eq [abbrev, in infotheo.probability.proba]
cPrE0 [prf, in infotheo.probability.proba]
cPrET [prf, in infotheo.probability.proba]
creasoning_by_cases [prf, in infotheo.probability.proba]
cresilience [prf, in infotheo.robust.robustmean]
cset0P [prf, in infotheo.probability.convex]
cset0PN [prf, in infotheo.probability.convex]
cset1_neq0 [prf, in infotheo.probability.convex]
cset_ext [prf, in infotheo.probability.convex]
cset_predType [def, in infotheo.probability.convex]
ctyp_element_ub [prf, in infotheo.information_theory.jtypes]
curry_imset2l_dep [prf, in infotheo.ecc_modern.degree_profile]
cV_of_nat [def, in infotheo.lib.natbin]
cVar [def, in infotheo.robust.robustmean]
cVarDist [prf, in infotheo.robust.robustmean]
cVarE [prf, in infotheo.robust.robustmean]
cvariance_ge0 [prf, in infotheo.robust.robustmean]
cycle_in_subtree [prf, in infotheo.ecc_modern.ldpc_algo_proof]
cycle_morph [prf, in infotheo.ecc_modern.degree_profile]
cyclic_code [file, in infotheo.ecc_classic.cyclic_code]