Module infotheo.probability.necset

# Semi-complete semilattice structures and non-empty convex sets ``` neset T == the type of non-empty sets over T x%:ne == try to infer whether x : set T is neset T (TODO: worth moving to a dedicated file?) x <| p |>: Y == (fun y => x <| p |> y) @` Y X :<| p |>: Y == \bigcup_(x in X) (x <| p |>: Y) semiLattType == type of (finitary) semilattice semiCompSemiLattType == type of semicomplete semilattice, or infinitary semilattice which may come without a bottom element, provides an infinitary operator |_| : neset T -> T with the following axioms (inherits from semiLattice): 1. |_| [set x] = x 2. |_| (\bigcup_(i in s) f i) = |_| (|_| @` (f @` s)) 3. x [+] y = |_| [set x; y] {Biglub_morph U -> V} == Homomorphism between semicomplete semilattices ``` ``` semiLattConvType == semilattice convex space: This structure is a combination of convex space and semilattice structures with the distributive law of convex operation over lattice operation. This is the algebra carried by the interface of combined choice monads, which is described by MonadAltProb in monae. Although semilattice convex space is what precisely corresponds to MonadAltProb, we prefer the easiness of its completion (semicomplete semilattice convex space, the next module after this one) when defining our instance of MonadAltProb in monae (gcm_model.v, altprob_model.v). semiCompSemiLattConvType == Semicomplete semilattice convex space: a combination of convex space and semicomplete semilattice structures with the distributive law of convex operation over lattice operation; this is the algebra carried by the combined choice monad, which is described in monae (files gcm_model.v and altprob_model.v), extends semiCompSemiLattType and convType with the following axiom: 3. x <| p |> |_| I = |_| ((fun y => x <| p |> y) @` I) ``` ``` {Biglub_affine U -> V} == Homomorphism between semicomplete semilattice convex spaces necset T == the type of non-empty convex sets over T, the object part of the third adjunction that appears in the definition of the combined choice monad ``` Structures on necset: - convex space structure on necset (necset_convType A, instance of convType) with elements of type necset A and with operator `X <| p |> Y = {x<|p|>y | x \in X, y \in Y}` (Notation: {necset A}) - semicomplete semilattice structure on necset, instance of semiCompSemiLattType with elements of type necset A and with operator `|_| X = hull (bigsetU X idfun)` - the combined structure on necset, instance of semiCompSemiLattConvType with elements of type necset A ``` necset_join, necset_bind == elementary definition of the multiplication and bind operations of the combined choice monad ``` ``` Section technical_corollaries == proofs of some subtle lemmas in the literature ```