R (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

R

R [def, in infotheo.information_theory.joint_typ_seq]
R [def, in infotheo.information_theory.channel_coding_direct]
R0E [prf, in infotheo.lib.coqRE]
r10_stop'0 [prf, in infotheo.lib.euclid]
R1E [prf, in infotheo.lib.coqRE]
R2 [def, in infotheo.ecc_modern.ldpc_algo]
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 [def, 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]
rate [proj, in infotheo.information_theory.channel_code]
raw_weight [def, in infotheo.probability.convex]
rbehead [def, in infotheo.lib.ssralg_ext]
rbehead_row_mx [prf, in infotheo.lib.ssralg_ext]
rbelast [def, in infotheo.lib.ssralg_ext]
rbelast_row_mx [prf, in infotheo.lib.ssralg_ext]
Rcode [mod, in infotheo.ecc_classic.linearcode]
Rcode.c [proj, in infotheo.ecc_classic.linearcode]
Rcode.P [proj, in infotheo.ecc_classic.linearcode]
Rcode.t [rec, in infotheo.ecc_classic.linearcode]
Rcode.t_ind [scheme, in infotheo.ecc_classic.linearcode]
Rcode.t_rec [scheme, in infotheo.ecc_classic.linearcode]
Rcode.t_rect [scheme, in infotheo.ecc_classic.linearcode]
Rcode.t_sind [scheme, in infotheo.ecc_classic.linearcode]
rcode_coercion [def, in infotheo.ecc_classic.linearcode]
RConvex [mod, in infotheo.probability.convex]
RConvex.avgnR [def, in infotheo.probability.convex]
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.big_scaleR [def, in infotheo.probability.convex]
RConvex.convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
RConvex.GRing_regular__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
RConvex.HB_unnamed_factory_60 [def, in infotheo.probability.convex]
RConvex.HB_unnamed_mixin_62 [def, in infotheo.probability.convex]
RConvex.onem_affine [prf, in infotheo.probability.convex]
RConvex.Scaled1RK [prf, in infotheo.probability.convex]
RConvex.scaleR [def, 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 [def, in infotheo.ecc_classic.cyclic_code]
rcs' [def, in infotheo.ecc_classic.cyclic_code]
rcs'0 [prf, in infotheo.ecc_classic.cyclic_code]
rcs'_rcs [prf, in infotheo.ecc_classic.cyclic_code]
rcs_perm [def, in infotheo.ecc_classic.cyclic_code]
rcs_perm_ffun [def, in infotheo.ecc_classic.cyclic_code]
rcs_perm_ffun_injectiveb [prf, in infotheo.ecc_classic.cyclic_code]
rcs_poly [def, 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 [def, in infotheo.ecc_classic.cyclic_code]
rcsP_BCH_cyclic [prf, in infotheo.ecc_classic.bch]
real_magnify_self [prf, in infotheo.probability.convex]
RealCone [abbrev, in infotheo.probability.convex]
RealCone [mod, in infotheo.probability.convex]
RealCone.axioms_ [rec, in infotheo.probability.convex]
RealCone.choice_hasChoice_mixin [proj, in infotheo.probability.convex]
RealCone.class [proj, in infotheo.probability.convex]
RealCone.clone [abbrev, in infotheo.probability.convex]
RealCone.convex_isQuasiRealCone_mixin [proj, in infotheo.probability.convex]
RealCone.convex_isRealCone_mixin [proj, in infotheo.probability.convex]
RealCone.copy [abbrev, in infotheo.probability.convex]
RealCone.eqtype_hasDecEq_mixin [proj, in infotheo.probability.convex]
RealCone.Exports [mod, in infotheo.probability.convex]
RealCone.Exports.convex_RealCone__to__choice_Choice [def, in infotheo.probability.convex]
RealCone.Exports.convex_RealCone__to__convex_QuasiRealCone [def, in infotheo.probability.convex]
RealCone.Exports.convex_RealCone__to__eqtype_Equality [def, in infotheo.probability.convex]
RealCone.Exports.convex_RealCone_class__to__choice_Choice_class [def, in infotheo.probability.convex]
RealCone.Exports.convex_RealCone_class__to__convex_QuasiRealCone_class [def, in infotheo.probability.convex]
RealCone.Exports.convex_RealCone_class__to__eqtype_Equality_class [def, in infotheo.probability.convex]
RealCone.Exports.realCone [abbrev, in infotheo.probability.convex]
RealCone.on [abbrev, in infotheo.probability.convex]
RealCone.on_ [abbrev, in infotheo.probability.convex]
RealCone.pack_ [def, in infotheo.probability.convex]
RealCone.phant_clone [def, in infotheo.probability.convex]
RealCone.phant_on_ [def, in infotheo.probability.convex]
RealCone.sort [proj, in infotheo.probability.convex]
RealCone.type [rec, in infotheo.probability.convex]
RealConeElpiOperations [mod, in infotheo.probability.convex]
realType_ext [file, in infotheo.lib.realType_ext]
realType_ln [file, in infotheo.lib.realType_ln]
reasoning_by_cases [prf, in infotheo.probability.proba]
receivable [rec, in infotheo.information_theory.pproba]
receivable_prop [def, in infotheo.information_theory.pproba]
receivable_propE [prf, in infotheo.information_theory.pproba]
receivable_rV [proj, in infotheo.information_theory.pproba]
receivableP [proj, in infotheo.information_theory.pproba]
recursive_computation [prf, in infotheo.ecc_modern.ldpc]
recursive_computation_helper [prf, in infotheo.ecc_modern.ldpc]
reed_solomon [file, in infotheo.ecc_classic.reed_solomon]
reflexive_relYn [prf, in infotheo.information_theory.jtypes]
reg_ldpc [rec, in infotheo.ecc_modern.ldpc]
reg_ldpc_prop [prf, in infotheo.ecc_modern.ldpc]
reg_rate [def, in infotheo.ecc_modern.ldpc]
regH [proj, in infotheo.ecc_modern.ldpc]
reglambda [proj, in infotheo.ecc_modern.ldpc]
regrho [proj, in infotheo.ecc_modern.ldpc]
relationF [prf, in infotheo.lib.euclid]
relYn [def, in infotheo.information_theory.jtypes]
rem_lea_false [def, in infotheo.lib.natbin]
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 [mod, in infotheo.ecc_classic.repcode]
Rep.code [def, in infotheo.ecc_classic.repcode]
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.CSM [def, in infotheo.ecc_classic.repcode]
Rep.dimlen [prf, in infotheo.ecc_classic.repcode]
Rep.encodeE [prf, in infotheo.ecc_classic.repcode]
Rep.Lcode_wo_repair [def, in infotheo.ecc_classic.repcode]
rep_encode_decode [prf, in infotheo.ecc_classic.repcode]
repair [def, 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]
repairT [def, in infotheo.ecc_classic.decoding]
repcode [file, 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_img [def, in infotheo.probability.bayes]
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]
rlast [def, in infotheo.lib.ssralg_ext]
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]
Rnonneg_interval [def, in infotheo.probability.convex]
robust_mean [prf, in infotheo.robust.robustmean]
robustmean [file, in infotheo.robust.robustmean]
root_in_Vgraph [prf, in infotheo.ecc_modern.tanner]
root_notin_subgraph [prf, in infotheo.ecc_modern.subgraph_partition]
row_drop [def, in infotheo.lib.ssralg_ext]
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_num_occ [def, in infotheo.information_theory.jtypes]
row_of_bitseq [def, in infotheo.lib.ssralg_ext]
row_of_seq [def, in infotheo.lib.ssralg_ext]
row_of_seqK [prf, in infotheo.lib.ssralg_ext]
row_of_tuple [def, 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_set [def, in infotheo.lib.ssralg_ext]
row_setC [prf, in infotheo.lib.ssralg_ext]
row_setK [prf, in infotheo.lib.ssralg_ext]
row_take [def, in infotheo.lib.ssralg_ext]
row_to_seq_0 [prf, in infotheo.lib.ssralg_ext]
rowF2_tuplebool [def, in infotheo.lib.ssralg_ext]
rowVnextD1 [def, in infotheo.ecc_modern.ldpc_erasure]
Rpos_convex [prf, in infotheo.probability.convex]
Rpos_interval [def, 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 [mod, in infotheo.ecc_classic.reed_solomon]
RS.addr_closed [prf, in infotheo.ecc_classic.reed_solomon]
RS.all_root_codeword [prf, in infotheo.ecc_classic.reed_solomon]
RS.code [def, in infotheo.ecc_classic.reed_solomon]
RS.codebook [def, 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.errors_ub [def, 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.PCM [def, in infotheo.ecc_classic.reed_solomon]
RS.redundancy_ub [def, 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 [mod, in infotheo.ecc_classic.reed_solomon]
RS_encoder.decoder [def, in infotheo.ecc_classic.reed_solomon]
RS_encoder.decomp_codeword [prf, in infotheo.ecc_classic.reed_solomon]
RS_encoder.encoder [def, in infotheo.ecc_classic.reed_solomon]
RS_encoder.high [def, in infotheo.ecc_classic.reed_solomon]
RS_encoder.low [def, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_as_lcode [def, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_code [def, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_discard [def, in infotheo.ecc_classic.reed_solomon]
RS_encoder.RS_discard' [def, 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 [def, in infotheo.ecc_classic.reed_solomon]
RS_err_is_correct [prf, in infotheo.ecc_classic.reed_solomon]
rs_gen [def, 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 [def, 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 [def, 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]
RV [def, in infotheo.probability.proba]
RV02 [prf, in infotheo.probability.proba]
RV2 [def, in infotheo.probability.proba]
RV20 [prf, in infotheo.probability.proba]
RV_equiv [def, in infotheo.probability.bayes]
RV_equivC [prf, in infotheo.probability.bayes]
RV_fctE [def, in infotheo.probability.proba]
RV_lmodMixin [def, in infotheo.probability.proba]
RV_of [def, in infotheo.probability.proba]
rV_of_nat [def, in infotheo.lib.natbin]
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_op [def, in infotheo.probability.proba]
rV_prod [def, in infotheo.lib.ssralg_ext]
rV_prodK [prf, in infotheo.lib.ssralg_ext]
rvar_choice [def, in infotheo.probability.bayes]
rVexp [def, in infotheo.lib.dft]
rVexp_inj [prf, in infotheo.lib.dft]
rVexp_neq0 [prf, in infotheo.lib.dft]
RVn [def, in infotheo.probability.proba]
rVpoly0 [prf, in infotheo.lib.poly_ext]