(Single Resource) dynamic program: $V_t(x)$ satisfies the printed recursion and boundary conditions

Let $(\lambda,\rho)$ be a Markov chain choice model, $r\in\mathbb R^n$ revenues and $T$ the number of periods. The value functions $V_t(x)$ of the (Single Resource) dynamic program satisfy the boundary conditions $V_{T+1}(x)=0$ for all $x$ and $V_t(0)=0$ for $t=1,\dots,T$, and for $t=1,\dots,T$ and $x\ge 1$,

This is the first line of the (Single Resource) display: with probability $P_{j,S}$ a customer buys product $j$, earning $r_j$ and leaving $x-1$ units, and otherwise capacity $x$ carries over to period $t+1$. It confirms that the rearranged recursion used to define $V_t$ is the dynamic program as printed.

Formalization Note $V_t(x)$ is value M r T t x, defined through the rearranged second line of the display; this theorem states that it satisfies the first line. The maximum is Finset.sup' over all subsets of $N$.