Library ALEA.RandomList
Fixpoint choose A (l : list A) : distr A :=
match l with
| nil => distr_null A
| cons hd tl => Mchoice ([1/](length l)) (Munit hd) (choose tl)
end.
Lemma choose_uniform : forall A (d : A) (l : list A) f,
mu (choose l) f == sigma (fun i => ([1/](length l)) * f (nth i l d)) (length l).
Lemma In_nth : forall A (x:A) l, In x l -> exists i, (i < length l)%nat /\ nth i l x = x.
Lemma choose_le_Nnth :
forall A (l:list A) x f alpha,
In x l ->
alpha <= f x ->
[1/](length l) * alpha <= mu (choose l) f.