JAO equation (34) for a two-class MDP: the reward collected under a planting exceeds the reference reward by at most times the plays of the planted pair
ProvedBanditAlgorithm.jao_two_class_reward_le_reference_plus_planted_plays_two_valuedThe two-class planted gadget. The MDP is given by its defining equations rather than through an auxiliary definition. The data are a class map , an escape map , a return map and a navigation map , and satisfies: the reward is the class, ; from a class- state every action goes to the class- state with probability and to the class- state otherwise; from a class- state every action goes to the class- state with probability and stays at otherwise. Every row is supported on two distinct states whose masses sum to , so the transition function is pinned down completely. The reference MDP is the same shape with . For and this is JAO Figure 3 with ; for it is the composite of Figure 4, its class- states being the .
The whole of JAO Section 6 is run at this level of generality, on the composite MDP itself rather than on the collapsed two-state MDP they pass to on p. 1583. That reduction is not available as an inequality between regrets: the simulating policy would have to be produced before the planting is chosen, and it sees neither which copy the composite is in nor which of the actions was played. Working with the class in place of the state avoids it, and no step of the argument is lost.
Throughout, the initial state is arbitrary and of either class.
On the two-valuedness hypothesis. The statement carries explicitly. It is not decoration: the row equations above only constrain states of class and of class , so without it a state of neither class has a completely unconstrained transition row and an arbitrarily large reward, and the conclusion fails outright from such an initial state. An earlier version of this node omitted it and has been deprecated.
Statement. For , every horizon , every policy and every initial state ,
where is the expectation under the planted MDP and that under the reference MDP, both run against the same policy from the same initial state, and counts the rounds in which the planted pair is played.
This is equation (34) of JAO (p. 1583) in the form the rest of the argument consumes, but obtained by a different and shorter route. Write for the probability that the state of round has class . Since the reward is the class indicator, the total expected reward is . Conditioning on a single step and using that the escape probability is off the planted pair and on it, while the return probability is everywhere,
with the probability that round plays the planted pair. The reference obeys the same recursion with and the same initial value , so the difference satisfies and . Summing that over telescopes, because , and gives
using , which follows from the recursion by induction. JAO instead bound by a stochastic-domination coupling between the two MDPs; the telescoping identity removes that step entirely, and it is also what makes the statement work from an arbitrary initial state, since the two recursions start from the same value whatever is.
import Mathlib.Data.Real.Sqrt import Mathlib.Analysis.SpecialFunctions.Log.Basic import Definitions.Def_UCRL2ConfidenceSets open MeasureTheory ProbabilityTheory
theorem BanditAlgorithm.jao_two_class_reward_le_reference_plus_planted_plays_two_valued {S A : ℕ}
(δ ε : ℝ) (hδ0 : 0 < δ) (hδ : δ ≤ 1 / 3) (hε0 : 0 < ε) (hεδ : ε ≤ δ)
(ρ : Fin S → ℝ) (up down : Fin S → Fin S) (nav : Fin S → Fin A → Fin S)
(hρ01 : ∀ s, ρ s = 0 ∨ ρ s = 1)
(sStar : Fin S) (bStar : Fin A) (M M₀ : FiniteMDP S A)
(hstar : ρ sStar = 0)
(hrM : ∀ s b, M.r s b = ρ s)
(hrow0M : ∀ s b, ρ s = 0 →
ρ (up s) = 1 ∧ ρ (nav s b) = 0 ∧ up s ≠ nav s b ∧
(M.P s b (up s) : ℝ) = δ + (if (s, b) = (sStar, bStar) then ε else 0) ∧
(M.P s b (nav s b) : ℝ) = 1 - δ - (if (s, b) = (sStar, bStar) then ε else 0))
(hrow1M : ∀ s b, ρ s = 1 →
ρ (down s) = 0 ∧ down s ≠ s ∧
(M.P s b (down s) : ℝ) = δ ∧ (M.P s b s : ℝ) = 1 - δ)
(hrM₀ : ∀ s b, M₀.r s b = ρ s)
(hrow0M₀ : ∀ s b, ρ s = 0 →
ρ (up s) = 1 ∧ ρ (nav s b) = 0 ∧ up s ≠ nav s b ∧
(M₀.P s b (up s) : ℝ) = δ ∧
(M₀.P s b (nav s b) : ℝ) = 1 - δ)
(hrow1M₀ : ∀ s b, ρ s = 1 →
ρ (down s) = 0 ∧ down s ≠ s ∧
(M₀.P s b (down s) : ℝ) = δ ∧ (M₀.P s b s : ℝ) = 1 - δ)
(T : ℕ) (π : MDPPolicy S A) (s₀ : Fin S) :
(∫ h, mdpTrajectoryReward M h ∂(mdpMeasure M (mdpStateDirac s₀) π T))
≤ (∫ h, mdpTrajectoryReward M₀ h ∂(mdpMeasure M₀ (mdpStateDirac s₀) π T))
+ (ε / (2 * δ))
* ∫ h, (mdpVisitCount h T sStar bStar : ℝ)
∂(mdpMeasure M (mdpStateDirac s₀) π T) := by
sorry