O (Global Index)
| 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 |
O
o_PI [def, in infotheo.information_theory.channel_coding_direct]o_PI_2 [prf, in infotheo.information_theory.channel_coding_direct]
occ_co_occ [prf, in infotheo.information_theory.jtypes]
oimg [def, in infotheo.ecc_classic.decoding]
Omega [def, in infotheo.ecc_classic.grs]
one_minus_X_neq0 [prf, in infotheo.ecc_classic.poly_decoding]
onem_div [prf, in infotheo.lib.realType_ext]
onem_divrxxy [prf, in infotheo.lib.realType_ext]
onem_eq0 [prf, in infotheo.lib.realType_ext]
onem_eq1 [prf, in infotheo.lib.realType_ext]
onem_le [prf, in infotheo.lib.realType_ext]
onem_lt [prf, in infotheo.lib.realType_ext]
onem_neq0 [prf, in infotheo.lib.realType_ext]
onem_oprob [prf, in infotheo.lib.realType_ext]
onem_prob [prf, in infotheo.lib.realType_ext]
onem_probR_ge0 [prf, in infotheo.probability.convex]
onemE [prf, in infotheo.lib.realType_ext]
open_interval_convex [prf, in infotheo.probability.convex]
open_norm_subball [prf, in infotheo.lib.derive_ext]
open_unit_interval_convex [prf, in infotheo.probability.convex]
oplus_conv_cset_is_convex [prf, in infotheo.probability.necset]
oplus_conv_set [def, in infotheo.probability.necset]
oplus_conv_set_monotone [prf, in infotheo.probability.necset]
oplus_conv_set_neq0 [prf, in infotheo.probability.necset]
oplus_convC_set [prf, in infotheo.probability.necset]
oplus_convmm_cset [prf, in infotheo.probability.necset]
oplus_convmm_set_hull [prf, in infotheo.probability.necset]
opp_RV_unif [prf, in infotheo.probability.proba]
OppositeOrderedConvexSpace [mod, in infotheo.probability.convex]
OppositeOrderedConvexSpace.A_of_TK [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.avg [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.avg1 [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.avgA [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.avgC [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.avgI [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.choice_Choice__to__choice_hasChoice [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.choice_Choice__to__eqtype_hasDecEq [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.convex_isConvexSpace__to__convex_isConvexSpace0 [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.eqopp_le [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.HB_unnamed_factory_83 [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.HB_unnamed_factory_88 [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.HB_unnamed_mixin_86 [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.HB_unnamed_mixin_87 [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.HB_unnamed_mixin_90 [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.leopp [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.leopp_trans [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.leoppR [prf, in infotheo.probability.convex]
OppositeOrderedConvexSpace.mkOpp [constr, in infotheo.probability.convex]
OppositeOrderedConvexSpace.OppositeOrderedConvexSpace_oppT__canonical__choice_Choice [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.OppositeOrderedConvexSpace_oppT__canonical__convex_ConvexSpace [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.OppositeOrderedConvexSpace_oppT__canonical__eqtype_Equality [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace.oppT [ind, in infotheo.probability.convex]
OppositeOrderedConvexSpace.T [abbrev, in infotheo.probability.convex]
OppositeOrderedConvexSpace.T [abbrev, in infotheo.probability.convex]
OppositeOrderedConvexSpace.unbox_oppT [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace_oppT__canonical__convex_OrderedConvexSpace [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace_oppT__canonical__Order_POrder [def, in infotheo.probability.convex]
OppositeOrderedConvexSpace_oppT__canonical__Order_Preorder [def, in infotheo.probability.convex]
oppr_const_RV [prf, in infotheo.probability.proba]
opprRVE [prf, in infotheo.probability.proba]
OProb [mod, in infotheo.lib.realType_ext]
OProb.Exports [mod, in infotheo.lib.realType_ext]
OProb.Exports.eqtype_Equality__to__eqtype_hasDecEq [def, in infotheo.lib.realType_ext]
OProb.Exports.HB_unnamed_factory_2 [def, in infotheo.lib.realType_ext]
OProb.Exports.HB_unnamed_factory_5 [def, in infotheo.lib.realType_ext]
OProb.Exports.HB_unnamed_mixin_7 [def, in infotheo.lib.realType_ext]
OProb.Exports.oprob [abbrev, in infotheo.lib.realType_ext]
OProb.Exports.OProb_t__canonical__eqtype_Equality [def, in infotheo.lib.realType_ext]
OProb.Exports.OProb_t__canonical__eqtype_SubEquality [def, in infotheo.lib.realType_ext]
OProb.Exports.OProb_t__canonical__eqtype_SubType [def, in infotheo.lib.realType_ext]
OProb.O1 [def, in infotheo.lib.realType_ext]
OProb.Op1 [proj, in infotheo.lib.realType_ext]
OProb.p [proj, in infotheo.lib.realType_ext]
OProb.t [rec, in infotheo.lib.realType_ext]
oprob_divrposxxy [prf, in infotheo.lib.realType_ext]
oprob_gt0 [prf, in infotheo.lib.realType_ext]
oprob_lt1 [prf, in infotheo.lib.realType_ext]
oprob_neq0 [prf, in infotheo.lib.realType_ext]
oprob_neq1 [prf, in infotheo.lib.realType_ext]
oprob_of_r_of_pq [def, in infotheo.lib.realType_ext]
oprob_of_s_of_pq [def, in infotheo.lib.realType_ext]
oprob_onemK [prf, in infotheo.lib.realType_ext]
oprob_to_real [abbrev, in infotheo.lib.realType_ext]
oprobadd_gt0 [prf, in infotheo.lib.realType_ext]
oprobadd_neq0 [prf, in infotheo.lib.realType_ext]
oprobcplt [def, in infotheo.lib.realType_ext]
oprobmulr [def, in infotheo.lib.realType_ext]
ord0E [prf, in infotheo.toy_examples.expected_value_variance_ordn]
ord1 [def, in infotheo.toy_examples.expected_value_variance_ordn]
ord1 [prf, in infotheo.lib.ssr_ext]
ord1E [prf, in infotheo.toy_examples.expected_value_variance_ordn]
ord2 [def, in infotheo.toy_examples.expected_value_variance_ordn]
ord2 [prf, in infotheo.lib.ssr_ext]
ord2E [prf, in infotheo.toy_examples.expected_value_variance_ordn]
ord3 [prf, in infotheo.lib.ssr_ext]
ord_eq_dec [def, in infotheo.probability.bayes]
ord_of_kind [def, in infotheo.ecc_modern.ldpc_algo]
Order_Le_isPOrder__to__Order_isDuallyPreorder [def, in infotheo.probability.convex]
Order_Le_isPOrder__to__Order_isDuallyPreorder__95 [def, in infotheo.probability.convex]
Order_Le_isPOrder__to__Order_Preorder_isDuallyPOrder [def, in infotheo.probability.convex]
Order_Le_isPOrder__to__Order_Preorder_isDuallyPOrder__93 [def, in infotheo.probability.convex]
Order_POrder__to__choice_hasChoice [def, in infotheo.probability.convex]
Order_POrder__to__eqtype_hasDecEq [def, in infotheo.probability.convex]
Order_POrder__to__Order_isDuallyPreorder [def, in infotheo.probability.convex]
Order_POrder__to__Order_Preorder_isDuallyPOrder [def, in infotheo.probability.convex]
OrderedConvexSpace [abbrev, in infotheo.probability.convex]
OrderedConvexSpace [mod, in infotheo.probability.convex]
OrderedConvexSpace.axioms_ [rec, in infotheo.probability.convex]
OrderedConvexSpace.choice_hasChoice_mixin [proj, in infotheo.probability.convex]
OrderedConvexSpace.class [proj, in infotheo.probability.convex]
OrderedConvexSpace.clone [abbrev, in infotheo.probability.convex]
OrderedConvexSpace.convex_isConvexSpace0_mixin [proj, in infotheo.probability.convex]
OrderedConvexSpace.copy [abbrev, in infotheo.probability.convex]
OrderedConvexSpace.eqtype_hasDecEq_mixin [proj, in infotheo.probability.convex]
OrderedConvexSpace.Exports [mod, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace__to__choice_Choice [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace__to__convex_ConvexSpace [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace__to__eqtype_Equality [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace__to__Order_POrder [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace__to__Order_Preorder [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace_class__to__choice_Choice_class [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace_class__to__convex_ConvexSpace_class [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace_class__to__eqtype_Equality_class [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace_class__to__Order_POrder_class [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.convex_OrderedConvexSpace_class__to__Order_Preorder_class [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.join_convex_OrderedConvexSpace_between_convex_ConvexSpace_and_Order_POrder [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.join_convex_OrderedConvexSpace_between_convex_ConvexSpace_and_Order_Preorder [def, in infotheo.probability.convex]
OrderedConvexSpace.Exports.orderedConvType [abbrev, in infotheo.probability.convex]
OrderedConvexSpace.on [abbrev, in infotheo.probability.convex]
OrderedConvexSpace.on_ [abbrev, in infotheo.probability.convex]
OrderedConvexSpace.Order_isDuallyPreorder_mixin [proj, in infotheo.probability.convex]
OrderedConvexSpace.Order_Preorder_isDuallyPOrder_mixin [proj, in infotheo.probability.convex]
OrderedConvexSpace.pack_ [def, in infotheo.probability.convex]
OrderedConvexSpace.phant_clone [def, in infotheo.probability.convex]
OrderedConvexSpace.phant_on_ [def, in infotheo.probability.convex]
OrderedConvexSpace.sort [proj, in infotheo.probability.convex]
OrderedConvexSpace.type [rec, in infotheo.probability.convex]
OrderedConvexSpaceElpiOperations [mod, in infotheo.probability.convex]
out_entropy_dist_ub [prf, in infotheo.information_theory.error_exponent]
output_type_out_entropy [prf, in infotheo.information_theory.jtypes]
output_type_out_fdist [prf, in infotheo.information_theory.jtypes]
OutType [mod, in infotheo.information_theory.jtypes]
OutType.d [def, in infotheo.information_theory.jtypes]
OutType.f [def, in infotheo.information_theory.jtypes]
OutType.f0 [prf, in infotheo.information_theory.jtypes]
OutType.f1 [prf, in infotheo.information_theory.jtypes]
OutType.P [def, in infotheo.information_theory.jtypes]