T (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 |
T (Lemmas)
tag_eqP [prf, in infotheo.ecc_modern.ldpc_algo_proof]tail_of_fdist_rV_fdist_col' [prf, in infotheo.probability.fdist]
tail_of_fdist_rV_fdist_rV [prf, in infotheo.probability.fdist]
take_index [prf, in infotheo.lib.ssr_ext]
tanner_rel_split [prf, in infotheo.ecc_modern.ldpc_algo_proof]
tanner_relE [prf, in infotheo.ecc_modern.tanner]
tanner_split_cons [prf, in infotheo.ecc_modern.ldpc_algo_proof]
tanner_split_nil [prf, in infotheo.ecc_modern.ldpc_algo_proof]
tanner_split_tanner [prf, in infotheo.ecc_modern.ldpc_algo_proof]
tanner_split_uncons [prf, in infotheo.ecc_modern.ldpc_algo_proof]
tbeheadE [prf, in infotheo.ecc_modern.degree_profile]
tcast2tval [prf, in infotheo.lib.ssr_ext]
tcast_take_inj [prf, in infotheo.lib.ssr_ext]
tcode_typed_prop [prf, in infotheo.information_theory.types]
td [prf, in infotheo.ecc_classic.reed_solomon]
tdcoor_of_fdcoor [prf, in infotheo.lib.dft]
tdcoorZ [prf, in infotheo.lib.dft]
test_acyclic [prf, in infotheo.ecc_modern.ldpc_algo_proof]
test_connected [prf, in infotheo.ecc_modern.ldpc_algo_proof]
test_graph [prf, in infotheo.ecc_modern.ldpc_algo_proof]
thead_tuple1 [prf, in infotheo.lib.ssr_ext]
time_shift [prf, in infotheo.lib.dft]
tn_tree_eqP [prf, in infotheo.ecc_modern.ldpc_algo_proof]
tnth_uniq [prf, in infotheo.lib.ssr_ext]
tnth_zip_1 [prf, in infotheo.lib.ssr_ext]
tnth_zip_2 [prf, in infotheo.lib.ssr_ext]
total_cEx [prf, in infotheo.robust.robustmean]
total_prob [prf, in infotheo.probability.proba]
total_prob_cond [prf, in infotheo.probability.proba]
trans_add_RVE [prf, in infotheo.probability.proba]
trans_RV_unif [prf, in infotheo.probability.proba]
trans_sub_RVE [prf, in infotheo.probability.proba]
tree_ok [prf, in infotheo.ecc_modern.ldpc_algo_proof]
TreeEnsemble.all_max_def_tree_enum [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.allpairs_flatten [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.cancel_fintree [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.cancel_tree [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.count_allpairs [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.count_map_muln [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.f0 [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.f0_tree [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.f0R [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.f1 [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.f1_tree [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.f1R [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.finseqs_deg [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.fintree_enumP [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.foldr_maxnE [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.kind_eqP [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.limit_get_fintree [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.limit_get_id [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.LR_pos [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.max_deg_all [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.negk_involution [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.Node_inj [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.nseqs_deg [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.size_finseqs [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.size_integ [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.size_integ_eq0 [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.size_norm [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.size_nseqs [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.size_take_leq [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.tree_children_node [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.tree_enumP [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.tree_frontier [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.tree_node_children [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.tree_node_inv [prf, in infotheo.ecc_modern.degree_profile]
TreeEnsemble.uniq_tree_enum [prf, in infotheo.ecc_modern.degree_profile]
tri_ine [prf, in infotheo.lib.hamming]
triangular_laws_left0 [prf, in infotheo.probability.fsdist]
trivIset0 [prf, in infotheo.ecc_modern.degree_profile]
trivIset1 [prf, in infotheo.ecc_modern.degree_profile]
trivIset_disjoint [prf, in infotheo.ecc_modern.degree_profile]
trivIset_enc_pre_img [prf, in infotheo.information_theory.types]
trivIset_Fgraph_part_Fgraph [prf, in infotheo.ecc_modern.tanner_partition]
trivIset_Fgraph_part_fnode [prf, in infotheo.ecc_modern.tanner_partition]
trivIset_I1 [prf, in infotheo.ecc_modern.degree_profile]
trivIset_in [prf, in infotheo.ecc_modern.degree_profile]
trivIset_out [prf, in infotheo.ecc_modern.degree_profile]
trivIset_set_set_co_occ [prf, in infotheo.lib.num_occ]
trivIset_shell [prf, in infotheo.information_theory.jtypes]
trivIset_shell' [prf, in infotheo.information_theory.jtypes]
trivIset_sub_ver_suc_suc_helper [prf, in infotheo.ecc_modern.subgraph_partition]
trivIset_subgraph_succ [prf, in infotheo.ecc_modern.subgraph_partition]
trivIset_subgraph_succ2_D1 [prf, in infotheo.ecc_modern.subgraph_partition]
trivIset_subgraph_succ2_D1_helper [prf, in infotheo.ecc_modern.subgraph_partition]
trivIset_Vgraph_part_Vgraph [prf, in infotheo.ecc_modern.tanner_partition]
trivIset_Vgraph_part_vnode [prf, in infotheo.ecc_modern.tanner_partition]
trivIsetS_f [prf, in infotheo.ecc_modern.tanner_partition]
TS_0_is_typ_seq [prf, in infotheo.information_theory.typ_seq]
TS_inf [prf, in infotheo.information_theory.typ_seq]
TS_sup [prf, in infotheo.information_theory.typ_seq]
Tset0 [prf, in infotheo.probability.proba]
TsetT [prf, in infotheo.probability.proba]
tuple2N_0 [prf, in infotheo.lib.natbin]
tuple_dist_type [prf, in infotheo.information_theory.types]
tuple_dist_type_entropy [prf, in infotheo.information_theory.types]
tuple_exist_perm_sort [prf, in infotheo.lib.ssr_ext]
tuple_of_row_inj [prf, in infotheo.lib.ssralg_ext]
tuple_of_row_ord0 [prf, in infotheo.lib.ssralg_ext]
tuple_of_row_row_mx [prf, in infotheo.lib.ssralg_ext]
tuple_of_rowK [prf, in infotheo.lib.ssralg_ext]
typ_seq_definition_equiv [prf, in infotheo.information_theory.typ_seq]
typ_seq_definition_equiv2 [prf, in infotheo.information_theory.typ_seq]
type_card_neq0 [prf, in infotheo.information_theory.types]
type_choice_pcancel [prf, in infotheo.information_theory.types]
type_co_occ [prf, in infotheo.information_theory.jtypes]
type_counting [prf, in infotheo.information_theory.types]
type_empty1 [prf, in infotheo.information_theory.types]
type_empty2 [prf, in infotheo.information_theory.types]
type_enumP [prf, in infotheo.information_theory.types]
type_eqP [prf, in infotheo.information_theory.types]
type_ext [prf, in infotheo.information_theory.types]
type_ffunP [prf, in infotheo.information_theory.types]
type_fun_type [prf, in infotheo.information_theory.types]
type_numocc [prf, in infotheo.information_theory.types]
typed_success [prf, in infotheo.information_theory.success_decode_bound]
typed_success_bound [prf, in infotheo.information_theory.success_decode_bound]
typed_tuples_are_typ_seq [prf, in infotheo.information_theory.types]
typed_tuples_not_empty [prf, in infotheo.information_theory.types]
typed_tuples_not_empty' [prf, in infotheo.information_theory.types]
typed_tuples_not_empty_alt [prf, in infotheo.information_theory.types]
typical_sequence1_JTS [prf, in infotheo.information_theory.joint_typ_seq]
typical_sequence1_JTS' [prf, in infotheo.information_theory.joint_typ_seq]