Winning measure-game strategies bound inner and outer measure

Fix a winning I strategy $\sigma$. A binary word p is acceptable if its bits are legal positive replies when I follows $\sigma$; the full game history $\psi (p)$ is uniquely reconstructed by F4. At acceptable p let f(p) be the current bound, and at unacceptable words let f(p)=0. Then $f(\mathrm{\varnothing })=v$, $0\le f\le 1$, and $(f(p0)+f(p1))\mathrm{/}2\ge f(p)$: at acceptable p the two child values equal the prescribed h_0,h_1, including zero for illegal replies, and F1 gives the inequality. At unacceptable p both children are unacceptable and all three values are zero. Summing over words of length n gives by induction ${\sum }_{\mathrm{\mid }p\mathrm{\mid }=n}{2}^{-n}f(p)\ge v$.

Let C_n be the clopen union of acceptable length-n cylinders. The cylinders are disjoint of measure $2^{-n}$ by F2, so step 1.1 and $f\le 1$ give $\nu (C_n)\ge v$. They decrease, and continuity from above F2 applies with first measure at most one. Thus closed $C={\bigcap }_n{C}_n$ has measure at least v. Every branch in C reconstructs a full legal $\sigma$-play and lies in E, by winningness. Therefore ${\nu }_{\mathrm{i}\mathrm{n}}(E)\ge \nu (C)\ge v$.

The I implication is established by step 2.1. For the second implication independently fix a winning II strategy $\tau$ and rational $\delta >0$. At an acceptable binary history p with constructed legal $\tau$-history $\psi (p)$ and bound v_p, define u_e to be the infimum of h_e over legal rational pairs h whose $\tau$ response is e, with infimum of the empty set set to one. Then $(u_0+u_1)\mathrm{/}2\le v_p$. Otherwise choose rational h_e satisfying $0\le h_e<u_e$ if u_e>0, and h_e=0 if u_e=0, close enough from below that their average still exceeds v_p; F3 supplies these approximants, all in [0,1]. This pair is legal. Its $\tau$ response must have h_e>0 by F1, hence u_e>0 and h_e<u_e, contradicting the defining infimum. This proves the inequality even at a zero u_e.

Start with acceptable empty p, bound v and empty history. For an acceptable p of length n, declare pe acceptable precisely when u_e<1. Then the defining set for that infimum is nonempty, and contains a pair with selected value $h_e<u_e+\delta 2^{-n-1}$. Choose the least rational-pair code with this property and response e; append that actual pair and response to define $\psi (pe)$. These selected responses are positive and their bounds rational. F4 performs the length recursion; excluded nodes have no acceptable descendants. This is a prescribed least-code recursion, not a selection of arbitrary real moves.

Set f(p)=v_p at acceptable nodes and f(p)=1 elsewhere. For acceptable p of length n, each included child has value at most $u_e+\delta 2^{-n-1}$ by step 4.1, and each excluded child has value $1=u_e$, so also satisfies that bound. Hence step 3.1 gives $(f(p0)+f(p1))\mathrm{/}2\le f(p)+\delta 2^{-n-1}$. At unacceptable p both child values are one, so the inequality still holds. Induction, starting at f(empty)=v, now gives

The sets U_n increase. Outside their open union U, every prefix is acceptable, so step 4.1 reconstructs a full legal $\tau$-play with that bit outcome. Since $\tau$ wins, the outcome is outside E; thus $E\subseteq U$. Continuity from below F2 and step 5.1 give $\nu (U)\le v+\delta$, hence ${\nu }_{\mathrm{o}\mathrm{u}\mathrm{t}}(E)\le v+\delta$. This holds for every positive rational $\delta$. If ${\nu }_{\mathrm{o}\mathrm{u}\mathrm{t}}(E)>v$, rational density F3 gives $0<\delta <{\nu }_{\mathrm{o}\mathrm{u}\mathrm{t}}(E)-v$, a contradiction. Therefore ${\nu }_{\mathrm{o}\mathrm{u}\mathrm{t}}(E)\le v$, completing the second implication. QED.