Module infotheo.probability.convex_equiv

# Equivalence of Convexity Definitions Documented in: - R. Affeldt, J. Garrigue, T. Saikawa. Formal adventures in convex and conical spaces. CICM 2020 In this file, we prove equivalences between various axiomatizations of convex spaces: - one with a binary operator and binary laws (`convType` of `convex.v`) - ones with an n-ary operator + Bonchi's axiomatization [Bonchi 2017] + Beaulieu's axiomatization [Beaulieu PhD 2008] + (and three others) The n-ary laws and their logical dependencies are listed in `Module NaryConvLaws`. The equivalences between n-ary theories are provided as Hierarchy-Builder structures and factories: ``` naryConvOpType == type with an n-ary convex opreator (mixin hasNaryConvOp) <&>_d f == notation for the operator of naryConvOpType naryConvType == type with n-ary convex theory in Bonchi's style (mixin isNaryConvexSpace) Module NaryConvexSpaceTheory == proofs that an naryConvType satisfies all the laws isNaryBeaulieuConvexSpace == HB factory for Beaulieu's axiomatization isNary( BaryMapConst | BarypartIdem | ProjPartConst )ConvexSpace == HB factories for three other combinations of the laws ``` The equivalence between `convType` and `naryConvType` is given as following modules: ``` BinToNary, NaryToBin == mutual instantiations between the two structures BinToNaryToBin, NaryToBinToNary == proofs that these constructions cancel each other, i.e., they are essentially the same structure a <& p &> b == binary instance of the <&>_ operator, provided by NaryToBin ``` The instance in `NaryToBin` is exported, i.e., `Check (T : naryConvType R) : convType R.` succeeds. Some combinations of the laws are strictly weaker. They are illustrated in modules `counterexamples_*` at the end of this file.