Shift identity (p. 290) — Φ(ω, s) = L(ω, δ₁) + P(δ₁) Φ(T_{δ₁} ω, s′)

In the setting of Karlin's deterministic model ($\Omega$ Hausdorff, $D$ nonempty compact Hausdorff, $L \ge 0$ continuous on $\Omega \times D$, $(\delta, \omega) \mapsto T_\delta\,\omega$ continuous, $P > 0$ continuous, $\omega_1 = \omega$, $\omega_n = T_{\delta_{n-1}}\,\omega_{n-1}$, $P_n(s) = \prod_{i=1}^{n-1} P(\delta_i)$), let $\omega \in \Omega$ and let $s = (\delta_1, \delta_2, \dots)$ be a strategy whose yield series $\sum_{n} L(\omega_n, \delta_n) P_n(s)$ converges. Write $s' = (\delta_2, \delta_3, \dots)$ for the shifted strategy. Then

The identity splits off the first stage: after the first decision, the remaining yield is the yield of the shifted strategy from the next state, scaled by $P(\delta_1)$. It is the step from which the functional equation (2) is derived.

Formalization Note The shift is fun k => s (k + 1). The paper states the identity inside a maximum over $s$; this item is the pointwise identity for each $s$. Summability of the series for this particular $s$ is assumed; it follows from the uniform convergence (1) and is needed because Lean's tsum of a non-summable series is $0$. The model's standing hypotheses (continuity, compactness, joint continuity of $T$ as in Theorem 1) are kept as in every item of the mission.