I (Lemmas)

Files ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Definitions ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Lemmas ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Abbreviations ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Global Index ABCDEFGHIJKLMNOPQRSTUVWXYZ_
Notations

I (Lemmas)

I3P [prf, in infotheo.toy_examples.expected_value_variance]
id_of_kind_inj [prf, in infotheo.ecc_modern.ldpc_algo_proof]
id_of_kind_neq [prf, in infotheo.ecc_modern.ldpc_algo_proof]
id_of_kind_select_children [prf, in infotheo.ecc_modern.ldpc_algo_proof]
idft0 [prf, in infotheo.lib.dft]
if_not_prefix [prf, in infotheo.information_theory.kraft]
image2_subset [prf, in infotheo.probability.convex]
image_const [prf, in infotheo.probability.necset]
image_preserves_convex_hull [prf, in infotheo.probability.convex]
imset_preimset [prf, in infotheo.lib.ssr_ext]
imsetA [prf, in infotheo.probability.fdist]
imsetAC [prf, in infotheo.probability.fdist]
imsetPn [prf, in infotheo.lib.ssr_ext]
in_fibration_of_partition [prf, in infotheo.probability.fsdist]
in_preimset [prf, in infotheo.lib.ssr_ext]
in_preimset1 [prf, in infotheo.lib.ssr_ext]
increasing_xlnx_delta [prf, in infotheo.lib.realType_ln]
Ind_bigcap [prf, in infotheo.probability.proba]
Ind_bigcup [prf, in infotheo.probability.proba]
Ind_bigcup_incl_excl [prf, in infotheo.probability.proba]
Ind_ge0 [prf, in infotheo.probability.proba]
Ind_idem [prf, in infotheo.robust.robustmean]
Ind_inP [prf, in infotheo.probability.proba]
Ind_le1 [prf, in infotheo.probability.proba]
Ind_notinP [prf, in infotheo.probability.proba]
Ind_one [prf, in infotheo.robust.robustmean]
Ind_set0 [prf, in infotheo.probability.proba]
Ind_setD [prf, in infotheo.probability.proba]
Ind_setI [prf, in infotheo.probability.proba]
Ind_setT [prf, in infotheo.probability.proba]
Ind_setU [prf, in infotheo.probability.proba]
Ind_sqr [prf, in infotheo.probability.proba]
Ind_subset [prf, in infotheo.probability.proba]
inde_dist_of_RV2 [prf, in infotheo.probability.proba]
inde_events_cplt [prf, in infotheo.probability.proba]
inde_events_cPr [prf, in infotheo.probability.proba]
inde_RV_comp [prf, in infotheo.probability.proba]
inde_RV_events [prf, in infotheo.probability.proba]
inde_RV_joint_entropyE [prf, in infotheo.information_theory.entropy]
inde_RV_sym [prf, in infotheo.probability.proba]
inde_RVP [prf, in infotheo.probability.proba]
independence_bound_on_entropy [prf, in infotheo.information_theory.entropy]
index_enum_cast_ord [prf, in infotheo.lib.ssr_ext]
information_cant_hurt_cond [prf, in infotheo.information_theory.entropy]
inj_card [prf, in infotheo.lib.ssr_ext]
inj_enc_not_typ [prf, in infotheo.information_theory.source_coding_vl_direct]
inj_f [prf, in infotheo.probability.fdist]
inj_prodAC [prf, in infotheo.probability.fdist]
inj_row_set [prf, in infotheo.lib.ssralg_ext]
injective_ary_of_nat [prf, in infotheo.information_theory.kraft]
injective_ary_of_nat_w [prf, in infotheo.information_theory.kraft]
injective_joint_entropy [prf, in infotheo.information_theory.entropy]
injective_prepend [prf, in infotheo.information_theory.kraft]
injective_sigma [prf, in infotheo.information_theory.kraft]
injective_swap [prf, in infotheo.lib.ssr_ext]
injective_w [prf, in infotheo.information_theory.kraft]
inordfE [prf, in infotheo.information_theory.source_coding_vl_converse]
inr_inj [prf, in infotheo.ecc_modern.degree_profile]
INR_type_fun [prf, in infotheo.information_theory.types]
insupp [prf, in infotheo.lib.ssralg_ext]
intersection [prf, in infotheo.probability.graphoid]
invariant_impl [prf, in infotheo.robust.weightedmean]
invariant_update [prf, in infotheo.robust.weightedmean]
invariantW_pr_S_neq0 [prf, in infotheo.robust.weightedmean]
IPW [prf, in infotheo.information_theory.binary_symmetric_channel]
is01_update [prf, in infotheo.robust.weightedmean]
is_cgenE [prf, in infotheo.ecc_classic.cyclic_code]
is_convex_hullE [prf, in infotheo.probability.convex]
is_convex_segmentP [prf, in infotheo.probability.convex]
is_convex_set0 [prf, in infotheo.probability.convex]
is_convex_set1 [prf, in infotheo.probability.convex]
is_convex_set_image [prf, in infotheo.probability.convex]
is_convex_setP [prf, in infotheo.probability.convex]
is_convex_setT [prf, in infotheo.probability.convex]
is_derive1_lnf [prf, in infotheo.lib.derive_ext]
is_derive1_lnf_eq [prf, in infotheo.lib.derive_ext]
is_derive1_Logf [prf, in infotheo.lib.realType_ln]
is_derive1_Logf_eq [prf, in infotheo.lib.realType_ln]
is_derive1_LogfM [prf, in infotheo.lib.realType_ln]
is_derive1_LogfM_eq [prf, in infotheo.lib.realType_ln]
is_derive1_LogfV [prf, in infotheo.lib.realType_ln]
is_derive1_LogfV_eq [prf, in infotheo.lib.realType_ln]
is_derive1_pinsker_fun [prf, in infotheo.probability.pinsker]
is_derive1_pinsker_function_spec [prf, in infotheo.probability.pinsker]
is_derive_sum_eq [prf, in infotheo.lib.derive_ext]
is_deriveB_eq [prf, in infotheo.lib.derive_ext]
is_deriveD_eq [prf, in infotheo.lib.derive_ext]
is_deriveM_eq [prf, in infotheo.lib.derive_ext]
is_deriveN_eq [prf, in infotheo.lib.derive_ext]
is_deriveV_eq [prf, in infotheo.lib.derive_ext]
is_deriveX_eq [prf, in infotheo.lib.derive_ext]
is_deriveZ_eq [prf, in infotheo.lib.derive_ext]
IsetT [prf, in infotheo.probability.proba]
iSP_BEC0_Blank [prf, in infotheo.ecc_modern.ldpc_erasure]
iSP_BEC0_star_inv [prf, in infotheo.ecc_modern.stopping_set]
iter0_conv_set [prf, in infotheo.probability.necset]
iter_addr0 [prf, in infotheo.lib.ssralg_ext]
iter_addr0_cV [prf, in infotheo.lib.ssralg_ext]
iter_bigcup_conv_set [prf, in infotheo.probability.necset]
iter_conv_set_superset [prf, in infotheo.probability.necset]
iter_monotone_conv_set [prf, in infotheo.probability.necset]
iterS_conv_set [prf, in infotheo.probability.necset]