(154)–(155), §D.3.2, p. 59 — U_{k,n} ≥ U_{k,n+1}, with W^IRS.FH = U_{1,0}, W^IRS.V-Zero = U_{K,T}, U_{k+1,0} = U_{k,T}

The model is the Bayesian bandit of §2.1: arms $a \in \mathcal A = \{1,\dots,K\}$ (0-based in Lean, $K \ge 1$), reward laws $\mathcal R_a(\theta_a)$, conjugate priors $\mathcal P_a(y_a)$, the Bayesian update $\mathcal U_a$, and the outcome law $\mathcal I(y)$ under which the arms are independent, $\theta_a \sim \mathcal P_a(y_a)$, and the rewards of arm $a$ are i.i.d. $\mathcal R_a(\theta_a)$ given $\theta_a$. The standing assumptions of §2.1 hold: $\mathcal U_a(y_a,r)$ is the Bayes posterior after observing $r$, the update maps are measurable, and $\mathbb E_{y_a}|R_{a,1}| < \infty$ for every belief $y_a$ (3).

Fix a horizon $T$ and a belief vector $y$, and let $U_{k,n}$ ($k \in \mathcal A$, $0 \le n \le T$) be the quantities (154): the expected best allocation of $T$ pulls when arms $a < k$ earn their actual cumulative payoffs $S_a(n_a)$, arm $k$ earns $S_k$ on its first $n$ pulls and $\hat\mu_{k,T-1}$ on each further pull, and arms $a > k$ earn $\hat\mu_{a,T-1}$ per pull. Then

and

Chaining these gives $W^{IRS.FH}(T,y) \ge W^{IRS.V\text{-}Zero}(T,y)$, the second inequality of (57).

Formalization Note Arms are 0-based, so the paper's $U_{1,0}$ is Ukn 0 0 and $U_{K,T}$ is Ukn (K-1) T. The page prints the coefficient of $(n_k - n)^+$ as $\hat\mu_{a,T-1}$; it is $\hat\mu_{k,T-1}$ (cf. (158)).