P (Global Index)

Files

I

O

Q

U

X

Y

Z

_

Definitions

Y

_

Lemmas

Y

_

Abbreviations

G

K

T

U

V

X

Y

Z

_

Global Index

Y

_

P

P [def, in infotheo.toy_examples.expected_value_variance_tuple]
p [def, in infotheo.toy_examples.expected_value_variance_tuple]
P [def, in infotheo.toy_examples.expected_value_variance_ordn]
P [def, in infotheo.probability.fsdist]
P_fin [prf, in infotheo.probability.fsdist]
P_fssum [prf, in infotheo.probability.fsdist]
P_fssum' [prf, in infotheo.probability.fsdist]
P_ge0 [prf, in infotheo.probability.fsdist]
P_is_probability [prf, in infotheo.probability.fsdist]
p_is_rs [prf, in infotheo.lib.realType_ext]
p_nonneg [prf, in infotheo.toy_examples.expected_value_variance_tuple]
p_of_0s [prf, in infotheo.lib.realType_ext]
p_of_1s [prf, in infotheo.lib.realType_ext]
p_of_neq1 [prf, in infotheo.lib.realType_ext]
p_of_r0 [prf, in infotheo.lib.realType_ext]
p_of_r1 [prf, in infotheo.lib.realType_ext]
p_of_rs [def, in infotheo.lib.realType_ext]
p_of_rs1 [prf, in infotheo.lib.realType_ext]
p_of_rs1P [prf, in infotheo.lib.realType_ext]
p_of_rsC [prf, in infotheo.lib.realType_ext]
p_of_rsE [prf, in infotheo.lib.realType_ext]
P_semi_sigma_additive [prf, in infotheo.probability.fsdist]
P_set0 [prf, in infotheo.probability.fsdist]
p_sum01 [prf, in infotheo.toy_examples.expected_value_variance_tuple]
pad_seqL [def, in infotheo.lib.ssr_ext]
pad_seqL_inj [prf, in infotheo.lib.ssr_ext]
pad_seqL_leading_true_inj [prf, in infotheo.lib.natbin]
pad_seqR [def, in infotheo.lib.ssr_ext]
pad_seqR_size [prf, in infotheo.lib.ssr_ext]
pair_big_fst [prf, in infotheo.lib.bigop_ext]
pair_big_snd [prf, in infotheo.lib.bigop_ext]
pair_ind [prf, in infotheo.lib.euclid]
PairConvexSpace [mod, in infotheo.probability.convex]
PairConvexSpace.convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
PairConvexSpace.Datatypes_prod__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
PairConvexSpace.HB_unnamed_factory_74 [def, in infotheo.probability.convex]
PairConvexSpace.HB_unnamed_mixin_76 [def, in infotheo.probability.convex]
pairwise_inde [def, in infotheo.probability.proba]
pairwise_indeE [prf, in infotheo.probability.proba]
parity_check [def, in infotheo.ecc_classic.cyclic_code]
PartialComputationGraph [mod, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.add_edge_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.border [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.border_nodes_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.border_p [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.build_traces [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.card_border_ports [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.card_nodes [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.card_nodes2 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.card_nodes3 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.card_ports_nodes_start [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.cards_conode_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.check_ports [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.comp_graph [rec, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.comp_graph_eqb [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.comp_graph_eqP [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.connected_ports [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.connected_start [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.connected_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.connected_step_ep [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.connected_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.connected_step_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.connected_switch [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.conode_outside_ports [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.conodes [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.conodes_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.conodes_switch_nodes [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_dist [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_dist1 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_dist_ge0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_dist_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_port [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_port_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_ports [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_ports_0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_ports_seqs [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_ports_seqs_0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_ports_seqs_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.dest_ports_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.edges [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.edges_inj [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.edges_out [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.edom [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.edom_codom [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.empty_hemi_graph [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.en_in_step_conodes [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.enum_step_border [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.ep_in_en [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.eq_edom_edges_inout [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.fintree_of_graph [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.fintree_of_trace [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.flip [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.flip_graph_rel [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.flip_seq_path [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.free_coports [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.free_coports_card [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.free_step_coports_gt [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.graph_dom [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.graph_node [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.graph_of_trace [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.graph_rel [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.graph_rel_irrel [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.graph_rel_known_port [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.graph_rel_switch [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.HB_unnamed_factory_42 [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.HB_unnamed_factory_44 [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.hemi_comp_graph [rec, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.hemi_comp_graph_eqb [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.hemi_comp_graph_eqP [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.inj_switch_path_node [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.known_coports [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.known_port [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.known_port_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.ksets [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.ksetsP [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.le_sum_all_cond [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotone_conodes_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotone_conodes_switch_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotone_nodes_switch_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_codom_step_it [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_edges_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_edges_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_edom_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_edom_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_step_rel [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_switch_edges_step_it [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_switch_progress [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_switch_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.monotonic_switch_step_it_odd [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.no_cycle_in_known_ports [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.no_sharing_tree_like [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.node_of_hemi_comp_graph [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.nodes [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.nodes_switch_conodes [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.part [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.part_nodes_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.part_p [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.partial_connected [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.partial_to_tuple [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.partial_to_tupleK [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.PartialComputationGraph_comp_graph__canonical__eqtype_Equality [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.PartialComputationGraph_hemi_comp_graph__canonical__eqtype_Equality [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.partition_big_nodes_arities [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.ports [proj, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.ports_conodes_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.single_hemi_graph [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.sp_in_step_edom [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.start_dist [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.start_dist_ge0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.start_graph [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_border [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_border_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_coborder [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_coborder_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_codom_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_cond [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_conodes [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_conodes_id [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_conodes_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_coports_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_dest_port [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_dist [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_dist_ge0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_dist_it [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_dist_it_1 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_dist_it_const [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_dist_it_ge0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edges [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edges_id [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edges_inj [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edges_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edges_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edges_sp_ep [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edom_codom [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edom_edom [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edom_id [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_edom_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_end_cond [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_it [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_nodes [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_nodes_id [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_nodes_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_ports_ok [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_start_cond [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.step_trivIset [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.sum_lambda_pred [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.sum_step_border [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.sum_step_dist_it_eq0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.sum_step_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.sum_step_used [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.sum_weighted_count_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_edges [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_edges_cancel [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_edges_cancel2 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_edges_inj [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_edges_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_edom_codom [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_graph_node [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_graph_nodeK [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_graph_rel [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_path_node [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_step_dist_it [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_step_dist_it_1 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_step_dist_it_const [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_step_dist_it_ge0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_step_it [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switch_step_it_cat [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switchK [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.switchK_edges [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree'_of_graph [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree'_of_graph_deg [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree'_of_trace [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree'_of_trace_deg [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree'_of_trace_graph [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_after [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_empty_border [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_neighbor [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_no_sharing [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_rev_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_rev_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_rev_subrel [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_rev_switch_step_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_start [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_switch [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_like_switch_imp [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_of_graph [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_of_graph_deg [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_of_trace [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_of_trace_deg [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tree_of_trace_graph [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.trivIset_port_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tuple_to_partial [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tuple_to_partial_enumK [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tuple_to_partial_in [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tuple_to_partial_out [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.tuple_to_partialK [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weight_is_dist [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count [def, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_it_eq0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_it_ge0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_next [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_start_is_dist [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_step [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_switch_ge0 [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_switch_it [prf, in infotheo.ecc_modern.degree_profile]
PartialComputationGraph.weighted_count_switch_step [prf, in infotheo.ecc_modern.degree_profile]
partition_big_fin_img [prf, in infotheo.lib.bigop_ext]
partition_big_fin_img_set [prf, in infotheo.lib.bigop_ext]
partition_big_preimset [prf, in infotheo.lib.bigop_ext]
partition_big_undup_map [prf, in infotheo.lib.bigop_ext]
partition_inequality [file, in infotheo.probability.partition_inequality]
partition_inequality [prf, in infotheo.probability.partition_inequality]
path_except [prf, in infotheo.ecc_modern.subgraph_partition]
path_except_neq [prf, in infotheo.ecc_modern.subgraph_partition]
path_except_notin [prf, in infotheo.ecc_modern.subgraph_partition]
PC1_neq0 [prf, in infotheo.robust.weightedmean]
pchar [def, in infotheo.information_theory.string_entropy]
PCM_instance [def, in infotheo.ecc_modern.stopping_set]
PCM_instanceE [prf, in infotheo.ecc_modern.stopping_set]
PCM_lin1_mx [prf, in infotheo.ecc_classic.reed_solomon]
PCM_V [prf, in infotheo.ecc_modern.tanner]
Pcode [mod, in infotheo.ecc_classic.cyclic_code]
Pcode.gen [proj, in infotheo.ecc_classic.cyclic_code]
Pcode.lcode0 [proj, in infotheo.ecc_classic.cyclic_code]
Pcode.P [proj, in infotheo.ecc_classic.cyclic_code]
Pcode.size_gen [proj, in infotheo.ecc_classic.cyclic_code]
Pcode.t [rec, in infotheo.ecc_classic.cyclic_code]
pcode_coercion [def, in infotheo.ecc_classic.cyclic_code]
perfect [def, in infotheo.ecc_classic.linearcode]
perm_eq_perm [prf, in infotheo.lib.ssr_ext]
perm_filter_enum_ord [prf, in infotheo.lib.ssr_ext]
perm_map_bij [prf, in infotheo.lib.ssr_ext]
perm_mx_vec [prf, in infotheo.lib.ssralg_ext]
perm_on_Sn [prf, in infotheo.lib.ssr_ext]
perm_Stuples_Stuples_perm [prf, in infotheo.information_theory.jtypes]
perm_tuple [def, in infotheo.lib.ssr_ext]
perm_tuple0 [prf, in infotheo.lib.ssr_ext]
perm_tuple_comp [prf, in infotheo.lib.ssr_ext]
perm_tuple_id [prf, in infotheo.lib.ssr_ext]
perm_tuple_in_Ttuples [prf, in infotheo.information_theory.types]
perm_tuple_inj [prf, in infotheo.lib.ssr_ext]
perm_tuple_set [def, in infotheo.lib.ssr_ext]
Pf [def, in infotheo.information_theory.source_coding_vl_converse]
Pf' [def, in infotheo.information_theory.source_coding_vl_converse]
pfamily_dprojs_V [prf, in infotheo.ecc_modern.summary_tanner]
pfwd1 [def, in infotheo.probability.proba]
pfwd1_comp [prf, in infotheo.probability.proba]
pfwd1_diag [prf, in infotheo.probability.proba]
pfwd1_domin_RV1 [prf, in infotheo.probability.proba]
pfwd1_domin_RV2 [prf, in infotheo.probability.proba]
pfwd1_eq0 [prf, in infotheo.probability.proba]
pfwd1_ge0 [prf, in infotheo.probability.proba]
pfwd1_neq0 [prf, in infotheo.probability.proba]
pfwd1_pairA [prf, in infotheo.probability.proba]
pfwd1_pairAC [prf, in infotheo.probability.proba]
pfwd1_pairC [prf, in infotheo.probability.proba]
pfwd1_pairCA [prf, in infotheo.probability.proba]
pfwd1_RV2_compl [prf, in infotheo.probability.proba]
pfwd1_RV2_op [prf, in infotheo.probability.proba]
pfwd1_RV_op [prf, in infotheo.probability.proba]
pfwd1E [prf, in infotheo.probability.proba]
pfwd1EfinType [prf, in infotheo.probability.proba]
pgen_cgen [prf, in infotheo.ecc_classic.cyclic_code]
pgen_is_cgen [prf, in infotheo.ecc_classic.cyclic_code]
phase_shift [def, in infotheo.lib.dft]
phi [def, in infotheo.information_theory.source_coding_vl_direct]
phi [def, in infotheo.information_theory.source_coding_fl_direct]
phi_def [def, in infotheo.information_theory.source_coding_vl_direct]
phi_f [prf, in infotheo.information_theory.source_coding_vl_direct]
phi_f [prf, in infotheo.information_theory.source_coding_fl_direct]
pid_mx_inj [prf, in infotheo.lib.ssralg_ext]
pinsker [file, in infotheo.probability.pinsker]
Pinsker_2_inequality [prf, in infotheo.probability.pinsker]
Pinsker_2_inequality_bdist [prf, in infotheo.probability.pinsker]
pinsker_fun [def, in infotheo.probability.pinsker]
pinsker_fun' [def, in infotheo.probability.pinsker]
pinsker_fun'_ge0 [prf, in infotheo.probability.pinsker]
pinsker_fun'_le0 [prf, in infotheo.probability.pinsker]
pinsker_fun_decreasing_on_0_to_p [prf, in infotheo.probability.pinsker]
pinsker_fun_increasing_on_p_to_1 [prf, in infotheo.probability.pinsker]
pinsker_fun_onem [prf, in infotheo.probability.pinsker]
pinsker_fun_p [prf, in infotheo.probability.pinsker]
pinsker_fun_p0 [prf, in infotheo.probability.pinsker]
pinsker_fun_p0_increasing_on_0_to_1 [prf, in infotheo.probability.pinsker]
pinsker_fun_p0_pos [prf, in infotheo.probability.pinsker]
pinsker_fun_p_eq [prf, in infotheo.probability.pinsker]
pinsker_fun_pos [prf, in infotheo.probability.pinsker]
pinsker_function_spec [def, in infotheo.probability.pinsker]
pinsker_function_spec' [def, in infotheo.probability.pinsker]
Pinsker_inequality [prf, in infotheo.probability.pinsker]
Pinsker_inequality_weak [prf, in infotheo.probability.pinsker]
PiSP_BEC0 [def, in infotheo.ecc_modern.ldpc_erasure]
PiSP_BEC0_Star_inv [prf, in infotheo.ecc_modern.stopping_set]
PiSP_BEC0_Star_inv_stable [prf, in infotheo.ecc_modern.stopping_set]
PiSP_BEC0S_Star_inv [prf, in infotheo.ecc_modern.stopping_set]
pmf [def, in infotheo.toy_examples.expected_value_variance_ordn]
pmf [def, in infotheo.toy_examples.expected_value_variance]
pmf01 [prf, in infotheo.toy_examples.expected_value_variance_ordn]
pmf01 [prf, in infotheo.toy_examples.expected_value_variance]
pmf1_Pf [prf, in infotheo.information_theory.source_coding_vl_converse]
pmf1_Pf' [prf, in infotheo.information_theory.source_coding_vl_converse]
pmf_ge0 [prf, in infotheo.toy_examples.expected_value_variance_ordn]
pmf_ge0 [prf, in infotheo.toy_examples.expected_value_variance]
PN [def, in infotheo.information_theory.source_coding_vl_converse]
PN_sum1 [prf, in infotheo.information_theory.source_coding_vl_converse]
point [def, in infotheo.probability.convex]
point_S1 [prf, in infotheo.probability.convex]
point_Scaled [prf, in infotheo.probability.convex]
poly_decoding [file, in infotheo.ecc_classic.poly_decoding]
poly_def_lead_coef [prf, in infotheo.lib.poly_ext]
poly_ext [file, in infotheo.lib.poly_ext]
poly_rV_0 [prf, in infotheo.lib.poly_ext]
poly_rV_0_inv [prf, in infotheo.lib.poly_ext]
polynomial_rcs [prf, in infotheo.ecc_classic.cyclic_code]
pos_evar_index [prf, in infotheo.robust.weightedmean]
pos_of_bitseq [def, in infotheo.lib.natbin]
pos_of_bitseq_nseq_false [prf, in infotheo.lib.natbin]
pos_of_bitseq_rev [prf, in infotheo.lib.natbin]
pos_of_bitseq_up [prf, in infotheo.lib.natbin]
pos_var_dist [prf, in infotheo.probability.variation_dist]
post_prob_uniform_checksubsum [prf, in infotheo.ecc_modern.checksum]
post_prob_uniform_cst [def, in infotheo.information_theory.pproba]
post_prob_uniform_kernel [prf, in infotheo.information_theory.pproba]
post_prob_uniformF [prf, in infotheo.information_theory.pproba]
post_prob_uniformT [prf, in infotheo.information_theory.pproba]
post_probE [prf, in infotheo.information_theory.pproba]
powR2D [prf, in infotheo.lib.realType_ln]
powR2sum [prf, in infotheo.lib.realType_ln]
powRK [prf, in infotheo.lib.realType_ln]
powRrM' [prf, in infotheo.lib.realType_ln]
pproba [file, in infotheo.information_theory.pproba]
pq_is_rs [prf, in infotheo.lib.realType_ext]
Pr [def, in infotheo.probability.proba]
Pr_1 [abbrev, in infotheo.probability.proba]
Pr_bigcup [prf, in infotheo.probability.proba]
Pr_bigcup_incl_excl [prf, in infotheo.probability.proba]
Pr_cplt [prf, in infotheo.probability.proba]
Pr_cPr_gt0 [prf, in infotheo.probability.proba]
Pr_diff [abbrev, in infotheo.probability.proba]
Pr_DMC_fst [prf, in infotheo.information_theory.channel]
Pr_DMC_out [prf, in infotheo.information_theory.channel]
Pr_DMC_rV_prod [prf, in infotheo.information_theory.channel]
Pr_domin_setI [prf, in infotheo.probability.proba]
Pr_domin_setX [abbrev, in infotheo.probability.proba]
Pr_domin_setXN [prf, in infotheo.probability.proba]
pr_eq_set [abbrev, in infotheo.probability.proba]
pr_eq_set1 [abbrev, in infotheo.probability.proba]
pr_eq_setE [abbrev, in infotheo.probability.proba]
pr_eq_unit [prf, in infotheo.probability.proba]
Pr_fdist_cond [prf, in infotheo.probability.proba]
Pr_fdist_fst [prf, in infotheo.probability.proba]
Pr_fdist_prod [prf, in infotheo.probability.proba]
Pr_fdist_prod_of_rV [prf, in infotheo.probability.proba]
Pr_fdist_prod_of_rV1 [prf, in infotheo.probability.proba]
Pr_fdist_prod_of_rV2 [prf, in infotheo.probability.proba]
Pr_fdist_proj23_domin [prf, in infotheo.probability.proba]
Pr_fdist_snd [prf, in infotheo.probability.proba]
Pr_fdistA [prf, in infotheo.probability.proba]
Pr_fdistAC [prf, in infotheo.probability.proba]
Pr_fdistC12 [prf, in infotheo.probability.proba]
Pr_fdistmap [prf, in infotheo.probability.proba]
Pr_fdistmap_RV2 [prf, in infotheo.probability.proba]
Pr_fdistX [prf, in infotheo.probability.proba]
Pr_ge0 [prf, in infotheo.probability.proba]
pr_geq [def, in infotheo.probability.proba]
Pr_gt0P [abbrev, in infotheo.probability.proba]
pr_in [def, in infotheo.probability.proba]
pr_in1 [prf, in infotheo.probability.proba]
pr_in_comp [abbrev, in infotheo.probability.proba]
pr_in_comp' [prf, in infotheo.probability.proba]
pr_in_comp_image [prf, in infotheo.probability.proba]
pr_in_domin_RV2 [prf, in infotheo.probability.proba]
pr_in_pair_setT [prf, in infotheo.probability.proba]
pr_in_pairA [prf, in infotheo.probability.proba]
pr_in_pairAC [prf, in infotheo.probability.proba]
pr_in_pairC [prf, in infotheo.probability.proba]
pr_in_pairCA [prf, in infotheo.probability.proba]
Pr_incl [abbrev, in infotheo.probability.proba]
pr_inE [prf, in infotheo.probability.proba]
pr_inE' [prf, in infotheo.probability.proba]
Pr_inter_eq [abbrev, in infotheo.probability.proba]
Pr_jcPr_gt0 [prf, in infotheo.probability.jfdist_cond]
Pr_jcPr_unit [prf, in infotheo.probability.jfdist_cond]
Pr_le1 [prf, in infotheo.probability.proba]
pr_leq [def, in infotheo.probability.proba]
Pr_lt1P [abbrev, in infotheo.probability.proba]
Pr_of_cplt [abbrev, in infotheo.probability.proba]
pr_S [prf, in infotheo.robust.weightedmean]
pr_S_gt0 [prf, in infotheo.robust.weightedmean]
Pr_set0 [prf, in infotheo.probability.proba]
Pr_set0P [prf, in infotheo.probability.proba]
Pr_set1 [prf, in infotheo.probability.proba]
Pr_setC [prf, in infotheo.probability.proba]
Pr_setD [prf, in infotheo.probability.proba]
Pr_setI [prf, in infotheo.probability.proba]
Pr_setT [prf, in infotheo.probability.proba]
Pr_setTX [prf, in infotheo.probability.proba]
Pr_setU [prf, in infotheo.probability.proba]
Pr_to_cplt [prf, in infotheo.probability.proba]
Pr_TS_1 [prf, in infotheo.information_theory.typ_seq]
Pr_union [abbrev, in infotheo.probability.proba]
Pr_union_disj [abbrev, in infotheo.probability.proba]
Pr_union_eq [abbrev, in infotheo.probability.proba]
Pr_XsetT [prf, in infotheo.probability.proba]
prec_node [def, in infotheo.ecc_modern.ldpc_algo]
pred_of_setK [prf, in infotheo.ecc_modern.degree_profile]
prefix [def, in infotheo.information_theory.kraft]
prefix_cat [prf, in infotheo.information_theory.kraft]
prefix_code [def, in infotheo.information_theory.kraft]
prefix_code_strong [def, in infotheo.information_theory.kraft]
prefix_codeP [prf, in infotheo.information_theory.kraft]
prefix_common [prf, in infotheo.information_theory.kraft]
prefix_cons [prf, in infotheo.information_theory.kraft]
prefix_implies_kraft_cond [prf, in infotheo.information_theory.kraft]
prefix_leq_size [prf, in infotheo.information_theory.kraft]
prefix_modn [prf, in infotheo.information_theory.kraft]
prefix_nil [prf, in infotheo.information_theory.kraft]
prefix_rcons [prf, in infotheo.information_theory.kraft]
prefix_refl [prf, in infotheo.information_theory.kraft]
prefix_same_size [prf, in infotheo.information_theory.kraft]
prefix_take [prf, in infotheo.information_theory.kraft]
prefixP [prf, in infotheo.information_theory.kraft]
prefixW [prf, in infotheo.information_theory.kraft]
preimage_add_ker [prf, in infotheo.probability.convex]
preimage_preserves_convex_hull [prf, in infotheo.probability.convex]
preimage_subset_convex_hull [prf, in infotheo.probability.convex]
preimC [def, in infotheo.information_theory.channel_code]
preimC_Cal_E [prf, in infotheo.information_theory.channel_coding_direct]
preimg_set1 [prf, in infotheo.probability.proba]
preimsetX [prf, in infotheo.lib.ssr_ext]
preimsetX2 [prf, in infotheo.lib.ssr_ext]
prepend [def, in infotheo.information_theory.kraft]
prim_root_not_uroot_on [prf, in infotheo.lib.dft]
primitive_is_principal [prf, in infotheo.lib.dft]
primitive_uroot_neq0 [prf, in infotheo.lib.dft]
Prob [mod, in infotheo.lib.realType_ext]
Prob.mk [def, in infotheo.lib.realType_ext]
Prob.O1 [prf, in infotheo.lib.realType_ext]
Prob.p [def, in infotheo.lib.realType_ext]
prob0 [def, in infotheo.lib.realType_ext]
prob1 [def, in infotheo.lib.realType_ext]
prob_chain_rule [prf, in infotheo.probability.proba]
prob_divrposxxy [prf, in infotheo.lib.realType_ext]
prob_ge0 [prf, in infotheo.lib.realType_ext]
prob_gt0 [prf, in infotheo.lib.realType_ext]
prob_invn [prf, in infotheo.lib.realType_ext]
prob_invprob [def, in infotheo.lib.realType_ext]
prob_le1 [prf, in infotheo.lib.realType_ext]
prob_lt1 [prf, in infotheo.lib.realType_ext]
prob_magnify_self [prf, in infotheo.probability.convex]
prob_trichotomy [prf, in infotheo.lib.realType_ext]
prob_trichotomy' [prf, in infotheo.lib.realType_ext]
proba [file, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_AddMagma [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_AddSemigroup [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_AddUMagma [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_BaseAddMagma [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_BaseAddUMagma [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_BaseZmodule [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_ChoiceBaseAddMagma [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_ChoiceBaseAddUMagma [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_Nmodule [def, in infotheo.probability.proba]
proba_RV_of__canonical__Algebra_Zmodule [def, in infotheo.probability.proba]
proba_RV_of__canonical__choice_Choice [def, in infotheo.probability.proba]
proba_RV_of__canonical__eqtype_Equality [def, in infotheo.probability.proba]
proba_RV_of__canonical__GRing_ComPzRing [def, in infotheo.probability.proba]
proba_RV_of__canonical__GRing_ComPzSemiRing [def, in infotheo.probability.proba]
proba_RV_of__canonical__GRing_Lmodule [def, in infotheo.probability.proba]
proba_RV_of__canonical__GRing_LSemiModule [def, in infotheo.probability.proba]
proba_RV_of__canonical__GRing_PzRing [def, in infotheo.probability.proba]
proba_RV_of__canonical__GRing_PzSemiRing [def, in infotheo.probability.proba]
probadd_eq0 [prf, in infotheo.lib.realType_ext]
probadd_neq0 [prf, in infotheo.lib.realType_ext]
probConvex [mod, in infotheo.probability.convex]
probConvex.avg_probE [prf, in infotheo.probability.convex]
probConvex.convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
probConvex.HB_unnamed_factory_117 [def, in infotheo.probability.convex]
probConvex.HB_unnamed_mixin_119 [def, in infotheo.probability.convex]
probConvex.Itv_def__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
probConvex.Itv_def__canonical__convex_OrderedConvexSpace [def, in infotheo.probability.convex]
probcplt [def, in infotheo.lib.realType_ext]
probdivrnnm [def, in infotheo.lib.realType_ext]
probfdist [def, in infotheo.probability.fdist]
probinvn [def, in infotheo.lib.realType_ext]
probK [prf, in infotheo.lib.realType_ext]
probKC [prf, in infotheo.lib.realType_ext]
probmul_eq1 [prf, in infotheo.lib.realType_ext]
probmulr [def, in infotheo.lib.realType_ext]
probset [def, in infotheo.probability.necset]
probset_neq0 [prf, in infotheo.probability.necset]
Prod [def, in infotheo.ecc_modern.ldpc_erasure]
Prod1 [prf, in infotheo.ecc_modern.ldpc_erasure]
prod__canonical__convex_OrderedConvexSpace [def, in infotheo.probability.convex]
Prod_Bit [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_colFnext_Bit [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_colFNext_mxSum_stopset [prf, in infotheo.ecc_modern.stopping_set]
Prod_colFNextD1_mxSum_stopset [prf, in infotheo.ecc_modern.stopping_set]
Prod_cons [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_cons_Bit [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_cons_Star [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_cons_starletter [prf, in infotheo.ecc_modern.ldpc_erasure]
prod_dist_inde_rv [abbrev, in infotheo.probability.proba]
prod_dist_inde_RV [prf, in infotheo.probability.proba]
prod_dist_inde_RV_rV [prf, in infotheo.probability.proba]
prod_dist_inde_rv_vec [abbrev, in infotheo.probability.proba]
Prod_dominates_Joint [prf, in infotheo.probability.fdist]
Prod_erase_Star [prf, in infotheo.ecc_modern.stopping_set]
Prod_filter_Star [prf, in infotheo.ecc_modern.ldpc_erasure]
prod_gt0_inv [prf, in infotheo.lib.bigop_ext]
Prod_map_not_Star [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_mxStar_col_Star [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_nseq_not_blank [prf, in infotheo.ecc_modern.ldpc_erasure]
prod_rV [def, in infotheo.lib.ssralg_ext]
prod_rVK [prf, in infotheo.lib.ssralg_ext]
Prod_starblank_is_Star [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_StarE [prf, in infotheo.ecc_modern.ldpc_erasure]
Prod_starletter [prf, in infotheo.ecc_modern.ldpc_erasure]
prod_types [def, in infotheo.probability.bayes]
prod_types_app [prf, in infotheo.probability.bayes]
prod_types_neq [prf, in infotheo.probability.bayes]
prod_types_out [prf, in infotheo.probability.bayes]
prod_vals [def, in infotheo.probability.bayes]
prod_vals' [def, in infotheo.probability.bayes]
prod_vals_eq [prf, in infotheo.probability.bayes]
prod_vals_eqP [prf, in infotheo.probability.bayes]
prod_vals_set_vals [prf, in infotheo.probability.bayes]
prodA [def, in infotheo.probability.fdist]
prodAC [def, in infotheo.probability.fdist]
prodr_gt0 [prf, in infotheo.lib.realType_ext]
prodrRVE [prf, in infotheo.probability.proba]
product_rule [prf, in infotheo.probability.proba]
product_rule_cond [prf, in infotheo.probability.proba]
product_ruleC [prf, in infotheo.probability.jfdist_cond]
PrX_fst [prf, in infotheo.probability.proba]
PrX_snd [prf, in infotheo.probability.proba]
ps [def, in infotheo.toy_examples.expected_value_variance_tuple]
Psets [def, in infotheo.ecc_modern.max_subset]
PsetsU [prf, in infotheo.ecc_modern.max_subset]
push_init [def, in infotheo.ecc_modern.ldpc_algo]
push_init_spec [prf, in infotheo.ecc_modern.ldpc_algo_proof]
put_back [def, in infotheo.information_theory.entropy]
put_backK [prf, in infotheo.information_theory.entropy]
put_front [def, in infotheo.information_theory.entropy]
put_front_inj [prf, in infotheo.information_theory.entropy]
put_front_perm [def, in infotheo.information_theory.entropy]