R (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

R (Lemmas)

R0E [prf, in infotheo.lib.coqRE]
r10_stop'0 [prf, in infotheo.lib.euclid]
R1E [prf, in infotheo.lib.coqRE]
R_affine_functionN [prf, in infotheo.probability.convex]
R_concave_function_atN [prf, in infotheo.probability.convex]
R_concave_functionB [prf, in infotheo.probability.convex]
R_concave_functionN [prf, in infotheo.probability.convex]
R_convex_function_atN [prf, in infotheo.probability.convex]
R_convex_functionB [prf, in infotheo.probability.convex]
R_convex_functionN [prf, in infotheo.probability.convex]
r_of_0q [prf, in infotheo.lib.realType_ext]
r_of_1q [prf, in infotheo.lib.realType_ext]
r_of_p0 [prf, in infotheo.lib.realType_ext]
r_of_p0_oprob [prf, in infotheo.lib.realType_ext]
r_of_p1 [prf, in infotheo.lib.realType_ext]
r_of_pq_is_r [prf, in infotheo.lib.realType_ext]
r_of_pqE [prf, in infotheo.lib.realType_ext]
r_of_pqK [prf, in infotheo.lib.realType_ext]
r_of_rpos_probA [prf, in infotheo.lib.realType_ext]
Rabs_xlnx [prf, in infotheo.lib.realType_ln]
random_coding_good_code [prf, in infotheo.information_theory.channel_coding_direct]
rank_cast_cols_comm [prf, in infotheo.ecc_classic.linearcode]
rank_GRS_PCM [prf, in infotheo.ecc_classic.grs]
rank_GRS_PCM_sq [prf, in infotheo.ecc_classic.grs]
rank_I [prf, in infotheo.lib.ssralg_ext]
rank_row_mx [prf, in infotheo.lib.ssralg_ext]
rbehead_row_mx [prf, in infotheo.lib.ssralg_ext]
rbelast_row_mx [prf, in infotheo.lib.ssralg_ext]
RConvex.avgnRE [prf, in infotheo.probability.convex]
RConvex.avgR_mulDl [prf, in infotheo.probability.convex]
RConvex.avgR_mulDr [prf, in infotheo.probability.convex]
RConvex.avgR_oppD [prf, in infotheo.probability.convex]
RConvex.avgRE [prf, in infotheo.probability.convex]
RConvex.onem_affine [prf, in infotheo.probability.convex]
RConvex.Scaled1RK [prf, in infotheo.probability.convex]
RConvex.scaleR0 [prf, in infotheo.probability.convex]
RConvex.scaleR_addpt [prf, in infotheo.probability.convex]
RConvex.scaleR_scalept [prf, in infotheo.probability.convex]
rcs'0 [prf, in infotheo.ecc_classic.cyclic_code]
rcs'_rcs [prf, in infotheo.ecc_classic.cyclic_code]
rcs_perm_ffun_injectiveb [prf, in infotheo.ecc_classic.cyclic_code]
rcs_poly_rcs [prf, in infotheo.ecc_classic.cyclic_code]
rcs_rcs_poly [prf, in infotheo.ecc_classic.cyclic_code]
rcsP_BCH_cyclic [prf, in infotheo.ecc_classic.bch]
real_magnify_self [prf, in infotheo.probability.convex]
reasoning_by_cases [prf, in infotheo.probability.proba]
receivable_propE [prf, in infotheo.information_theory.pproba]
recursive_computation [prf, in infotheo.ecc_modern.ldpc]
recursive_computation_helper [prf, in infotheo.ecc_modern.ldpc]
reflexive_relYn [prf, in infotheo.information_theory.jtypes]
reg_ldpc_prop [prf, in infotheo.ecc_modern.ldpc]
relationF [prf, in infotheo.lib.euclid]
rem_lea_false_nseq [prf, in infotheo.lib.natbin]
rem_lea_false_pad_seqL [prf, in infotheo.lib.natbin]
remainder_in_code [prf, in infotheo.ecc_classic.cyclic_code]
Rep.codewords [prf, in infotheo.ecc_classic.repcode]
Rep.compatible [prf, in infotheo.ecc_classic.repcode]
Rep.const_mx_in_code [prf, in infotheo.ecc_classic.repcode]
Rep.dimlen [prf, in infotheo.ecc_classic.repcode]
Rep.encodeE [prf, in infotheo.ecc_classic.repcode]
rep_encode_decode [prf, in infotheo.ecc_classic.repcode]
repair_codeword [prf, in infotheo.ecc_classic.hamming_code]
repair_failure [prf, in infotheo.ecc_classic.hamming_code]
repair_failure1 [prf, in infotheo.ecc_classic.hamming_code]
repair_failure2 [prf, in infotheo.ecc_classic.hamming_code]
repair_odd [prf, in infotheo.ecc_classic.repcode]
repcode_MD_decoding [prf, in infotheo.ecc_classic.repcode]
repcode_not_empty [prf, in infotheo.ecc_classic.repcode]
repr_in_neset [prf, in infotheo.probability.necset]
reprepair_img [prf, in infotheo.ecc_classic.repcode]
resilience [prf, in infotheo.robust.robustmean]
rev7_bin [prf, in infotheo.lib.natbin]
rev7_lb [prf, in infotheo.lib.natbin]
rev7_neq0 [prf, in infotheo.lib.natbin]
rev7_ub [prf, in infotheo.lib.natbin]
rev_bitseq_of_nat_7 [prf, in infotheo.lib.natbin]
rev_fin_imgK [prf, in infotheo.probability.bayes]
rev_nseq [prf, in infotheo.lib.ssr_ext]
rev_path_rcons [prf, in infotheo.lib.ssr_ext]
rewrite_HP_with_HPN [prf, in infotheo.information_theory.source_coding_vl_converse]
rewrite_HP_with_Pf [prf, in infotheo.information_theory.source_coding_vl_converse]
rewrite_HP_with_PN [prf, in infotheo.information_theory.source_coding_vl_converse]
Rle0Pf [prf, in infotheo.information_theory.source_coding_vl_converse]
Rle0Pf' [prf, in infotheo.information_theory.source_coding_vl_converse]
rmul_foldr_rsum [prf, in infotheo.ecc_modern.ldpc_algo_proof]
rmul_rsum_commute0 [prf, in infotheo.ecc_modern.summary_tanner]
RNconcave_function [prf, in infotheo.probability.convex]
RNconcave_function_at [prf, in infotheo.probability.convex]
RNconvex_function [prf, in infotheo.probability.convex]
RNconvex_function_at [prf, in infotheo.probability.convex]
Rnonneg_convex [prf, in infotheo.probability.convex]
robust_mean [prf, in infotheo.robust.robustmean]
root_in_Vgraph [prf, in infotheo.ecc_modern.tanner]
root_notin_subgraph [prf, in infotheo.ecc_modern.subgraph_partition]
row_mx_rbehead [prf, in infotheo.lib.ssralg_ext]
row_mx_rbelast [prf, in infotheo.lib.ssralg_ext]
row_mx_row_ord0 [prf, in infotheo.lib.ssralg_ext]
row_mx_row_ord_max [prf, in infotheo.lib.ssralg_ext]
row_mx_take_drop [prf, in infotheo.lib.ssralg_ext]
row_mxA' [prf, in infotheo.lib.ssralg_ext]
row_of_seqK [prf, in infotheo.lib.ssralg_ext]
row_of_tuple_inj [prf, in infotheo.lib.ssralg_ext]
row_of_tupleK [prf, in infotheo.lib.ssralg_ext]
row_setC [prf, in infotheo.lib.ssralg_ext]
row_setK [prf, in infotheo.lib.ssralg_ext]
row_to_seq_0 [prf, in infotheo.lib.ssralg_ext]
Rpos_convex [prf, in infotheo.probability.convex]
rprod_Fgraph_part_fnode [prf, in infotheo.ecc_modern.tanner_partition]
rprod_rsum_commute [prf, in infotheo.ecc_modern.summary_tanner]
rprod_sub_vec [prf, in infotheo.information_theory.channel]
RS.addr_closed [prf, in infotheo.ecc_classic.reed_solomon]
RS.all_root_codeword [prf, in infotheo.ecc_classic.reed_solomon]
RS.codebook_syndrome [prf, in infotheo.ecc_classic.reed_solomon]
RS.deg_lb [prf, in infotheo.ecc_classic.reed_solomon]
RS.lcode0_codebook [prf, in infotheo.ecc_classic.reed_solomon]
RS.O_in_codebook [prf, in infotheo.ecc_classic.reed_solomon]
RS.oppr_closed [prf, in infotheo.ecc_classic.reed_solomon]
RS.RS_syndromep_codeword [prf, in infotheo.ecc_classic.reed_solomon]
RS.RS_syndromep_codeword' [prf, in infotheo.ecc_classic.reed_solomon]
RS.scaler_closed [prf, in infotheo.ecc_classic.reed_solomon]
RS.submod_closed [prf, in infotheo.ecc_classic.reed_solomon]
RS.syndrome_syndromep [prf, in infotheo.ecc_classic.reed_solomon]
RS.uniq_roots_exp [prf, in infotheo.ecc_classic.reed_solomon]
RS_cyclic [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.decomp_codeword [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_enc_discard_is_id [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_enc_img [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_enc_injective [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_enc_surjective [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_repair_img [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_repair_output_is_in_the_code [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.tmp [prf, in infotheo.ecc_classic.reed_solomon]
RS_err_is_correct [prf, in infotheo.ecc_classic.reed_solomon]
rs_gen_is_gen [prf, in infotheo.ecc_classic.reed_solomon]
rs_gen_is_pgen [prf, in infotheo.ecc_classic.reed_solomon]
rs_genP [prf, in infotheo.ecc_classic.reed_solomon]
RS_GRS_PCM [prf, in infotheo.ecc_classic.reed_solomon]
RS_GRS_syndromep [prf, in infotheo.ecc_classic.reed_solomon]
RS_Hchar [prf, in infotheo.ecc_classic.reed_solomon]
RS_key_equation [prf, in infotheo.ecc_classic.reed_solomon]
RS_MDS [prf, in infotheo.ecc_classic.reed_solomon]
RS_message_size [prf, in infotheo.ecc_classic.reed_solomon]
RS_min_dist [prf, in infotheo.ecc_classic.reed_solomon]
RS_min_dist1 [prf, in infotheo.ecc_classic.reed_solomon]
RS_mod_is_GRS_mod [prf, in infotheo.ecc_classic.reed_solomon]
RS_not_trivial [prf, in infotheo.ecc_classic.reed_solomon]
RS_repair_is_correct [prf, in infotheo.ecc_classic.reed_solomon]
rsum_disjoints_set [prf, in infotheo.information_theory.source_coding_vl_converse]
rsum_freeon0 [prf, in infotheo.ecc_modern.summary]
rsum_freeon1 [prf, in infotheo.ecc_modern.summary]
rsum_rmul_rV_pmf_tnth [prf, in infotheo.probability.fdist]
rsum_rmul_tuple_pmf [prf, in infotheo.information_theory.channel_coding_direct]
rsum_rmul_tuple_pmf_tnth [prf, in infotheo.information_theory.channel_coding_direct]
RV02 [prf, in infotheo.probability.proba]
RV20 [prf, in infotheo.probability.proba]
RV_equivC [prf, in infotheo.probability.bayes]
rV_of_nat_0 [prf, in infotheo.lib.natbin]
rV_of_nat_inj [prf, in infotheo.lib.natbin]
rV_of_nat_neq0 [prf, in infotheo.lib.natbin]
rV_of_natD_neq0 [prf, in infotheo.lib.natbin]
rV_prodK [prf, in infotheo.lib.ssralg_ext]
rVexp_inj [prf, in infotheo.lib.dft]
rVexp_neq0 [prf, in infotheo.lib.dft]
rVpoly0 [prf, in infotheo.lib.poly_ext]