E (Lemmas)
| 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 |
E (Lemmas)
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_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.EC_non_flip [prf, in infotheo.information_theory.erasure_channel]
EC.f0 [prf, in infotheo.information_theory.erasure_channel]
EC.f1 [prf, 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_pre_img_injective [prf, in infotheo.information_theory.types]
encode_decode [prf, in infotheo.ecc_classic.hamming_code]
encode_image_code [prf, in infotheo.ecc_classic.linearcode]
entroPN_0 [prf, in infotheo.information_theory.source_coding_vl_converse]
entropy_concave [prf, 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_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_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'_pos [prf, in infotheo.information_theory.source_coding_vl_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]
eqlP [prf, in infotheo.ecc_modern.ldpc_erasure]
eqn29 [prf, in infotheo.information_theory.entropy]
eqr_divrMr [prf, in infotheo.lib.realType_ext]
eqW [prf, in infotheo.lib.ssr_ext]
erasures_erase [prf, in infotheo.ecc_modern.stopping_set]
erasures_SP_BEC_subset [prf, in infotheo.ecc_modern.stopping_set]
ErealConvex.conv_erealE [prf, in infotheo.probability.convex]
ErealConvex.oprob_sg1 [prf, in infotheo.probability.convex]
err_codeword [prf, in infotheo.ecc_classic.hamming_code]
erreval0 [prf, in infotheo.ecc_classic.poly_decoding]
erreval_vecE [prf, in infotheo.ecc_classic.poly_decoding]
errloc0 [prf, 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_bound [prf, in infotheo.information_theory.error_exponent]
error_rate_symmetry [prf, in infotheo.information_theory.channel_coding_direct]
EsetT [prf, in infotheo.probability.proba]
estimation_alpha [prf, in infotheo.ecc_modern.ldpc_algo_proof]
estimation_correctness [prf, in infotheo.ecc_modern.ldpc]
estimation_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
Euclid.leq_size_r [prf, in infotheo.lib.euclid]
Euclid.ltn_size_r [prf, in infotheo.lib.euclid]
Euclid.qE [prf, 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.uvE [prf, in infotheo.lib.euclid]
Euclid.vu [prf, in infotheo.lib.euclid]
euclid_back [prf, 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_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.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]
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_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]
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_uniq_path [prf, in infotheo.ecc_modern.subgraph_partition]