E (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

E

e0 [def, in infotheo.information_theory.source_coding_fl_converse]
e0_delta [prf, in infotheo.information_theory.source_coding_fl_converse]
E_add_RV [prf, in infotheo.probability.proba]
E_cast_RV_fdist_rV1 [prf, in infotheo.probability.proba]
E_comp_RV [prf, in infotheo.probability.proba]
E_const_RV [prf, in infotheo.probability.proba]
e_hamming [prf, in infotheo.ecc_classic.hamming_code]
E_id_rem [prf, in infotheo.probability.proba]
E_id_rem_helper [prf, in infotheo.probability.proba]
E_Ind [prf, in infotheo.probability.proba]
E_leng_cw [def, in infotheo.information_theory.source_code]
E_leng_cw_le_Length [prf, in infotheo.information_theory.source_coding_vl_direct]
E_opp_RV [prf, in infotheo.probability.proba]
E_prod_2 [prf, in infotheo.probability.proba]
E_scale_RV [prf, in infotheo.probability.proba]
E_sub_RV [prf, in infotheo.probability.proba]
E_sum_2 [prf, in infotheo.probability.proba]
E_sum_n [prf, in infotheo.probability.proba]
E_SumIndCap [prf, in infotheo.probability.proba]
E_sumR [prf, in infotheo.probability.proba]
E_trans_add_RV [prf, in infotheo.probability.proba]
E_trans_RV_id_rem [prf, in infotheo.probability.proba]
E_trans_sub_RV [prf, in infotheo.probability.proba]
EC [mod, in infotheo.information_theory.erasure_channel]
EC.c [def, in infotheo.information_theory.erasure_channel]
EC.EC_non_flip [prf, in infotheo.information_theory.erasure_channel]
EC.f [def, in infotheo.information_theory.erasure_channel]
EC.f0 [prf, in infotheo.information_theory.erasure_channel]
EC.f1 [prf, in infotheo.information_theory.erasure_channel]
EC.P'W [abbrev, in infotheo.information_theory.erasure_channel]
EC.PW [abbrev, in infotheo.information_theory.erasure_channel]
EC.W [abbrev, in infotheo.information_theory.erasure_channel]
echa_ge0 [prf, in infotheo.information_theory.channel_code]
echa_le1 [prf, in infotheo.information_theory.channel_code]
ELC_fdist_rV [prf, in infotheo.information_theory.source_coding_vl_converse]
emean_cond_split [prf, in infotheo.robust.weightedmean]
emean_condE [prf, in infotheo.robust.weightedmean]
emean_sum [prf, in infotheo.robust.weightedmean]
empty_finType_code_set [prf, in infotheo.information_theory.kraft]
empty_finType_nil [prf, in infotheo.information_theory.kraft]
empty_finType_size [prf, in infotheo.information_theory.kraft]
empty_rV [prf, in infotheo.lib.ssralg_ext]
enc [proj, in infotheo.information_theory.source_code]
enc [proj, in infotheo.information_theory.channel_code]
enc_not_typ [def, in infotheo.information_theory.source_coding_vl_direct]
enc_pre_img [def, in infotheo.information_theory.types]
enc_pre_img_injective [prf, in infotheo.information_theory.types]
enc_pre_img_partition [def, in infotheo.information_theory.types]
enc_typ [def, in infotheo.information_theory.source_coding_vl_direct]
encode_decode [prf, in infotheo.ecc_classic.hamming_code]
encode_image_code [prf, in infotheo.ecc_classic.linearcode]
Encoder [mod, in infotheo.ecc_classic.linearcode]
Encoder.enc [proj, in infotheo.ecc_classic.linearcode]
Encoder.enc_img [proj, in infotheo.ecc_classic.linearcode]
Encoder.enc_inj [proj, in infotheo.ecc_classic.linearcode]
Encoder.t [rec, in infotheo.ecc_classic.linearcode]
encoder_coercion [def, in infotheo.ecc_classic.linearcode]
Encoding [mod, in infotheo.information_theory.shannon_fano]
Encoding.f [proj, in infotheo.information_theory.shannon_fano]
Encoding.f_inj [proj, in infotheo.information_theory.shannon_fano]
Encoding.t [rec, in infotheo.information_theory.shannon_fano]
encoding_coercion [def, in infotheo.information_theory.shannon_fano]
encT [def, in infotheo.information_theory.source_code]
encT [def, in infotheo.information_theory.channel_code]
entroPN_0 [prf, in infotheo.information_theory.source_coding_vl_converse]
entropy [file, in infotheo.information_theory.entropy]
entropy [def, in infotheo.information_theory.entropy]
entropy_concave [prf, in infotheo.information_theory.entropy_convex]
entropy_concave_alternative_proof_binary_case [mod, in infotheo.information_theory.entropy_convex]
entropy_concave_alternative_proof_binary_case.concavity_of_entropy [prf, in infotheo.information_theory.entropy_convex]
entropy_concave_alternative_proof_binary_case.concavity_of_entropy_x_le_y [prf, in infotheo.information_theory.entropy_convex]
entropy_concave_alternative_proof_binary_case.H2 [abbrev, in infotheo.information_theory.entropy_convex]
entropy_convex [file, in infotheo.information_theory.entropy_convex]
entropy_convex_dom_pair__canonical__choice_Choice [def, in infotheo.information_theory.entropy_convex]
entropy_convex_dom_pair__canonical__convex_ConvexSpace [def, in infotheo.information_theory.entropy_convex]
entropy_convex_dom_pair__canonical__eqtype_Equality [def, in infotheo.information_theory.entropy_convex]
entropy_Ex [prf, in infotheo.information_theory.entropy]
entropy_fdist_perm [prf, in infotheo.information_theory.entropy]
entropy_fdist_prod_of_rV [prf, in infotheo.information_theory.entropy]
entropy_fdist_rV [prf, in infotheo.information_theory.entropy]
entropy_fdist_rV_of_prod [prf, in infotheo.information_theory.entropy]
entropy_fdistA [prf, in infotheo.information_theory.entropy]
entropy_fdistmap [prf, in infotheo.information_theory.entropy]
entropy_ge0 [prf, in infotheo.information_theory.entropy]
entropy_H2 [prf, in infotheo.information_theory.entropy]
entropy_head_of1 [prf, in infotheo.information_theory.entropy]
entropy_log_div [prf, in infotheo.information_theory.entropy_convex]
entropy_max [prf, in infotheo.information_theory.entropy]
entropy_rV [prf, in infotheo.information_theory.entropy]
entropy_uniform [prf, in infotheo.information_theory.entropy]
entropyB [prf, in infotheo.information_theory.entropy]
enum_cons [prf, in infotheo.ecc_modern.degree_profile]
enum_fdist_binary_supp [prf, in infotheo.probability.fdist]
enum_id [def, in infotheo.ecc_modern.ldpc_algo_proof]
enum_id_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
enum_inord [prf, in infotheo.lib.ssr_ext]
enum_select_children [prf, in infotheo.ecc_modern.ldpc_algo_proof]
enum_val_bij_on [prf, in infotheo.ecc_modern.degree_profile]
enum_val_full [prf, in infotheo.ecc_modern.degree_profile]
enum_val_sum_num_occ [prf, in infotheo.lib.num_occ]
eps [abbrev, in infotheo.robust.weightedmean]
eps [abbrev, in infotheo.robust.weightedmean]
eps [abbrev, in infotheo.robust.weightedmean]
eps [abbrev, in infotheo.robust.weightedmean]
eps [abbrev, in infotheo.robust.weightedmean]
eps'_pos [prf, in infotheo.information_theory.source_coding_vl_direct]
eps_max [abbrev, in infotheo.robust.weightedmean]
epsilon' [def, in infotheo.information_theory.source_coding_vl_direct]
epsilon0_condition [def, in infotheo.information_theory.channel_coding_direct]
eq_alpha_beta [prf, in infotheo.ecc_modern.ldpc_algo_proof]
eq_Convn [prf, in infotheo.probability.convex]
eq_dec_refl [prf, in infotheo.probability.bayes]
eq_dep_Convn [prf, in infotheo.probability.convex]
eq_in_map_seqs [prf, in infotheo.lib.ssr_ext]
eq_path_in [prf, in infotheo.ecc_modern.degree_profile]
eq_setSU [prf, in infotheo.ecc_modern.degree_profile]
eq_sizef_Lnt [prf, in infotheo.information_theory.source_coding_vl_direct]
eq_sizef_Lt [prf, in infotheo.information_theory.source_coding_vl_direct]
eq_tcast [prf, in infotheo.lib.ssr_ext]
eql [def, in infotheo.ecc_modern.ldpc_erasure]
eqlP [prf, in infotheo.ecc_modern.ldpc_erasure]
eqn29 [prf, in infotheo.information_theory.entropy]
eqr_divrMr [prf, in infotheo.lib.realType_ext]
eqtype_Equality__to__eqtype_hasDecEq [def, in infotheo.probability.fsdist]
eqtype_Equality__to__eqtype_hasDecEq [def, in infotheo.probability.convex]
eqW [prf, in infotheo.lib.ssr_ext]
erase [def, in infotheo.ecc_modern.stopping_set]
erasure_channel [file, in infotheo.information_theory.erasure_channel]
erasures [def, in infotheo.ecc_modern.stopping_set]
erasures_erase [prf, in infotheo.ecc_modern.stopping_set]
erasures_SP_BEC_subset [prf, in infotheo.ecc_modern.stopping_set]
ErealConvex [mod, in infotheo.probability.convex]
ErealConvex.constructive_ereal_extended__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
ErealConvex.conv_erealE [prf, in infotheo.probability.convex]
ErealConvex.convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
ErealConvex.HB_unnamed_factory_36 [def, in infotheo.probability.convex]
ErealConvex.HB_unnamed_mixin_38 [def, in infotheo.probability.convex]
ErealConvex.oprob_sg1 [prf, in infotheo.probability.convex]
err_codeword [prf, in infotheo.ecc_classic.hamming_code]
erreval [def, in infotheo.ecc_classic.poly_decoding]
erreval0 [prf, in infotheo.ecc_classic.poly_decoding]
erreval_vecE [prf, in infotheo.ecc_classic.poly_decoding]
errloc [def, in infotheo.ecc_classic.poly_decoding]
errloc0 [prf, in infotheo.ecc_classic.poly_decoding]
errloc_alt [def, in infotheo.ecc_classic.poly_decoding]
errloc_neq0 [prf, in infotheo.ecc_classic.poly_decoding]
errloc_puncture [prf, in infotheo.ecc_classic.poly_decoding]
errloc_twisted [prf, in infotheo.ecc_classic.bch]
errloc_zero [prf, in infotheo.ecc_classic.poly_decoding]
error_exponent [file, in infotheo.information_theory.error_exponent]
error_exponent_bound [prf, in infotheo.information_theory.error_exponent]
error_rate_symmetry [prf, in infotheo.information_theory.channel_coding_direct]
ErrRateCond [def, in infotheo.information_theory.channel_code]
errsupp [proj, in infotheo.ecc_classic.poly_decoding]
errvec [rec, in infotheo.ecc_classic.poly_decoding]
errvect [proj, in infotheo.ecc_classic.poly_decoding]
EsetT [prf, in infotheo.probability.proba]
Esti [def, in infotheo.ecc_modern.ldpc_erasure]
esti_spec [def, in infotheo.ecc_modern.ldpc_algo]
estimation [def, in infotheo.ecc_modern.ldpc_algo]
estimation_alpha [prf, in infotheo.ecc_modern.ldpc_algo_proof]
estimation_correctness [prf, in infotheo.ecc_modern.ldpc]
estimation_ext [def, in infotheo.ecc_modern.ldpc_algo]
estimation_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
estimation_spec [def, in infotheo.ecc_modern.ldpc_algo]
euclid [file, in infotheo.lib.euclid]
Euclid [mod, in infotheo.lib.euclid]
Euclid.leq_size_r [prf, in infotheo.lib.euclid]
Euclid.ltn_size_r [prf, in infotheo.lib.euclid]
Euclid.q [def, in infotheo.lib.euclid]
Euclid.qE [prf, in infotheo.lib.euclid]
Euclid.r [def, in infotheo.lib.euclid]
Euclid.rE [prf, in infotheo.lib.euclid]
Euclid.relationA [prf, in infotheo.lib.euclid]
Euclid.relationB [prf, in infotheo.lib.euclid]
Euclid.ruv [prf, in infotheo.lib.euclid]
Euclid.u [def, in infotheo.lib.euclid]
Euclid.u0 [def, in infotheo.lib.euclid]
Euclid.u1 [def, in infotheo.lib.euclid]
Euclid.uv [def, in infotheo.lib.euclid]
Euclid.uvE [prf, in infotheo.lib.euclid]
Euclid.v [def, in infotheo.lib.euclid]
Euclid.v0 [def, in infotheo.lib.euclid]
Euclid.v1 [def, in infotheo.lib.euclid]
Euclid.vu [prf, in infotheo.lib.euclid]
euclid_back [prf, in infotheo.lib.euclid]
euclid_cont [def, in infotheo.lib.euclid]
euclid_cont_size_r [prf, in infotheo.lib.euclid]
euclid_lemma [prf, in infotheo.lib.euclid]
euclid_next [prf, in infotheo.lib.euclid]
evar0P [prf, in infotheo.robust.weightedmean]
evarE [prf, in infotheo.robust.weightedmean]
Ex [def, in infotheo.probability.proba]
ex2C [def, in infotheo.lib.realType_ext]
Ex_alt [def, in infotheo.probability.proba]
Ex_altE [prf, in infotheo.probability.proba]
Ex_cEx [prf, in infotheo.probability.proba]
Ex_cExT [prf, in infotheo.robust.robustmean]
Ex_comp_RV [prf, in infotheo.probability.proba]
ex_euclid_cont [prf, in infotheo.lib.euclid]
Ex_ge0 [prf, in infotheo.probability.proba]
EX_gt0 [prf, in infotheo.information_theory.source_coding_vl_converse]
Ex_lb [prf, in infotheo.probability.proba]
EX_ord [prf, in infotheo.information_theory.source_coding_vl_converse]
Ex_square_eq0 [prf, in infotheo.robust.robustmean]
Ex_square_expansion [prf, in infotheo.robust.robustmean]
example_proj_part_const [mod, in infotheo.probability.convex_equiv]
example_proj_part_const.axconst [prf, in infotheo.probability.convex_equiv]
example_proj_part_const.axpart [prf, in infotheo.probability.convex_equiv]
example_proj_part_const.axproj [prf, in infotheo.probability.convex_equiv]
example_proj_part_const.bigand [def, in infotheo.probability.convex_equiv]
example_proj_part_const.Datatypes_bool__canonical__convex_equiv_NaryConvOp [def, in infotheo.probability.convex_equiv]
example_proj_part_const.HB_unnamed_factory_54 [def, in infotheo.probability.convex_equiv]
example_proj_part_const.test [def, in infotheo.probability.convex_equiv]
example_proj_part_const.test [def, in infotheo.probability.convex_equiv]
except [def, in infotheo.ecc_modern.subgraph_partition]
except13 [prf, in infotheo.ecc_modern.subgraph_partition]
except_path [prf, in infotheo.ecc_modern.subgraph_partition]
except_rel [prf, in infotheo.ecc_modern.subgraph_partition]
exceptE [prf, in infotheo.ecc_modern.subgraph_partition]
exceptN [prf, in infotheo.ecc_modern.subgraph_partition]
exists_frac_part [prf, in infotheo.lib.realType_ln]
exists_non0_codeword_lowest_deg [prf, in infotheo.ecc_classic.linearcode]
exp_cdiv [def, in infotheo.information_theory.conditional_divergence]
exp_cdiv_ge0 [prf, in infotheo.information_theory.conditional_divergence]
exp_cdiv_left [prf, in infotheo.information_theory.conditional_divergence]
exp_inj [prf, in infotheo.lib.dft]
exp_inj_helper_nat [prf, in infotheo.lib.dft]
exp_inj_helper_ord [prf, in infotheo.lib.dft]
exp_strict_lb [prf, in infotheo.lib.realType_ln]
expected [prf, in infotheo.toy_examples.expected_value_variance_tuple]
expected [prf, in infotheo.toy_examples.expected_value_variance_ordn]
expected [prf, in infotheo.toy_examples.expected_value_variance]
expected_value_variance [file, in infotheo.toy_examples.expected_value_variance]
expected_value_variance_ordn [file, in infotheo.toy_examples.expected_value_variance_ordn]
expected_value_variance_tuple [file, in infotheo.toy_examples.expected_value_variance_tuple]
expR1_gt2 [prf, in infotheo.lib.realType_ext]
expr2_char2 [prf, in infotheo.lib.f2]
expr_const_RV [prf, in infotheo.probability.proba]
expr_conv_mono [prf, in infotheo.information_theory.binary_symmetric_channel]
exprRVE [prf, in infotheo.probability.proba]
ext_inj [def, in infotheo.ecc_classic.alternant]
ext_inj_rV [def, in infotheo.ecc_classic.alternant]
ext_inj_tmp [def, in infotheo.ecc_classic.alternant]
ext_uniq_path [prf, in infotheo.ecc_modern.subgraph_partition]
extension [def, in infotheo.information_theory.source_code]