Take any family $(S_i)_{i∈I}$ such that each $S_i$ is a convex set of functions $f : ℕ→[0,1]$ where $\sum_{k∈ℕ} f(k) = 1$. By "convex" we mean that for any $f,g∈S_i$ and any $a,b∈[0,1]$ such that $a+b=1$ we have $a·f+b·g∈S_i$. By AC (axiom of choice) there is a choice function for $S$. But I get a feeling that AC can be eliminated. Can it?
If I am not mistaken, we can construct a $g : ℕ→[0,1]$ uniquely definable from $S_i$ such that each finite prefix of $g$ agrees with some member of $S_i$, say by inductively defining $g(k)$ to be $\max(\frac12(p+q),q-2^{-k})$ where $p,q$ are the $\inf,\sup$ of the interval of possible values of $f(k)$ for $f∈S_i$ that extends $g↾ℕ_{<k}$ (it is an interval due to convexity). But we may not have $g∈S_i$ (there is a simple counter-example), so this does not work.
So is AC actually necessary here? If so, can it be eliminated if we have some stronger condition than convexity? For instance, what if we require that $S_i$ is closed under weighted combination, meaning that for every $w : S_i→[0,1]$ satisfying $\sum_{f∈S_i} w(f) = 1$ we have $h∈S_i$ where $h : ℕ→[0,1]$ given by $h(k) = \sum_{f∈S_i} ( w(f)·f(k) )$? My counter-example for the $g$ above does not work for this stronger condition, but I am still unable to prove that $g∈S_i$ without using AC...