C (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

C (Lemmas)

C1_is01 [prf, in infotheo.robust.weightedmean]
C_not_empty [prf, in infotheo.ecc_classic.hamming_code]
canonical_cgen_lowest_size [prf, in infotheo.ecc_classic.cyclic_code]
canonical_cgenP [prf, in infotheo.ecc_classic.cyclic_code]
caratheodory [prf, in infotheo.probability.convex]
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_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]
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]
cdiv0P [prf, in infotheo.information_theory.conditional_divergence]
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]
centropy1_fdistAC [prf, in infotheo.information_theory.entropy]
centropy1_ge0 [prf, 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_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_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]
Channel1.chan_star_eq [prf, in infotheo.information_theory.channel]
channel_coding [prf, in infotheo.information_theory.channel_coding_direct]
channel_coding_converse [prf, in infotheo.information_theory.channel_coding_converse]
channel_coding_converse_gen [prf, in infotheo.information_theory.channel_coding_converse]
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_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]
children_ind [prf, in infotheo.ecc_modern.ldpc_algo_proof]
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_alt [prf, in infotheo.probability.proba]
cinde_events_unit [prf, in infotheo.probability.proba]
cinde_RV_events [prf, in infotheo.probability.proba]
cinde_RV_sym [prf, in infotheo.probability.proba]
cinde_RV_unit [prf, in infotheo.probability.proba]
classify_big [prf, in infotheo.lib.bigop_ext]
CodomDFDist.dE [prf, in infotheo.probability.fdist]
CodomDFDist.dE' [prf, 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_perm_inj [prf, in infotheo.lib.ssralg_ext]
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_mxProd [prf, in infotheo.ecc_modern.stopping_set]
cols_starblank_PCM_instance_erasures [prf, in infotheo.ecc_modern.stopping_set]
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_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_RVE [prf, in infotheo.probability.proba]
compfid [prf, in infotheo.lib.ssr_ext]
computed_tree_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
concats_entropy [prf, in infotheo.information_theory.string_entropy]
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]
concavef_at_onem [prf, in infotheo.probability.convex]
cond_entropy_chanE [prf, in infotheo.information_theory.channel]
cond_entropy_chanE2 [prf, in infotheo.information_theory.channel]
cond_entropy_self [prf, 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_compat [prf, in infotheo.information_theory.conditional_divergence]
cond_type_equiv [prf, in infotheo.information_theory.jtypes]
conditional_entropy_example.conditional_entropyE [prf, in infotheo.toy_examples.conditional_entropy]
conditional_entropy_example.dE [prf, 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]
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_uniq_path [prf, in infotheo.lib.ssr_ext]
const_RC [prf, in infotheo.robust.robustmean]
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]
conv0 [prf, in infotheo.probability.convex]
conv0_pt_set [prf, in infotheo.probability.necset]
conv0_set [prf, in infotheo.probability.necset]
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_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_monotone [prf, in infotheo.probability.necset]
conv_set_neq0 [prf, in infotheo.probability.necset]
conv_setE [prf, in infotheo.probability.necset]
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_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_div [prf, in infotheo.information_theory.entropy_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_sym [prf, in infotheo.probability.convex]
convex_in_bothP [prf, in infotheo.probability.convex]
convex_relative_entropy [prf, in infotheo.information_theory.entropy_convex]
convex_setP [prf, in infotheo.probability.convex]
convexf_at_onem [prf, in infotheo.probability.convex]
convmm_cset [prf, in infotheo.probability.necset]
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.d_enum0 [prf, in infotheo.probability.convex]
Convn_finType.d_enum1 [prf, in infotheo.probability.convex]
Convn_idem [prf, in infotheo.probability.convex]
Convn_iter_conv_set [prf, in infotheo.probability.necset]
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]
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]
count_sumn [prf, in infotheo.lib.ssr_ext]
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.noproj [prf, 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.noproj [prf, 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.noconst [prf, in infotheo.probability.convex_equiv]
counterexample_proj_part_noconst_noidem.noidem [prf, in infotheo.probability.convex_equiv]
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_maxset [prf, in infotheo.ecc_modern.max_subset]
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_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_unit_RV [prf, in infotheo.probability.proba]
cpr_eqE [prf, in infotheo.probability.proba]
cPr_ge0 [prf, 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_setD [prf, in infotheo.probability.proba]
cPr_setU [prf, 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]
ctyp_element_ub [prf, in infotheo.information_theory.jtypes]
curry_imset2l_dep [prf, in infotheo.ecc_modern.degree_profile]
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]