BanditRLProof.DelayedFeedback.Elimination

Inputs read by Algorithm 5 line 7 when it processes one newly available feedback item. This is deliberately an elimination snapshot rather than a claim that the full Delayed SAPO state machine has already been implemented.

structure DelayedSAPOEliminationSnapshot (K : Nat) where

Arms selected by the strict elimination test in Algorithm 5 line 7.

noncomputable def eliminated {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) : Finset (Fin K)

Active set after Algorithm 5 line 8 removes every arm selected by line 7.

noncomputable def remainingActive {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) : Finset (Fin K)

No declaration docstring is present; use the chapter context and exact statement below.

theorem mem_eliminated_iff {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) (i : Fin K) : i ∈ snapshot.eliminated ↔ i ∈ snapshot.active ∧ snapshot.ucbStar < snapshot.empiricalMean i - (9 : ℝ) * snapshot.empiricalWidth i

No declaration docstring is present; use the chapter context and exact statement below.

theorem mem_remainingActive_iff {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) (i : Fin K) : i ∈ snapshot.remainingActive ↔ i ∈ snapshot.active ∧ snapshot.empiricalMean i - (9 : ℝ) * snapshot.empiricalWidth i ≤ snapshot.ucbStar

The two source conditions used in the deterministic core of Lemma D.9: the empirical mean of the optimal arm lies in its good-event confidence interval, and the source's `ucbStar` remains an upper certificate for the optimal mean. The event probability establishing these fields is a separate concentration obligation.

structure OptimalArmSurvivalCertificate {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) (mean : Fin K → ℝ) (optimal : Fin K) : Prop where

Deterministic core of source Lemma D.9: on the relevant stochastic good-event projections, Algorithm 5's strict line-7 test cannot eliminate the certified optimal arm.

theorem optimal_mem_remainingActive_of_certificate {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) (mean : Fin K → ℝ) (optimal : Fin K) (certificate : OptimalArmSurvivalCertificate snapshot mean optimal) : optimal ∈ snapshot.remainingActive

Consequently the post-elimination active set is nonempty. This closes the exact nonemptiness premise required by Algorithm 5 line 15's residual allocation.

theorem remainingActive_nonempty_of_certificate {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) (mean : Fin K → ℝ) (optimal : Fin K) (certificate : OptimalArmSurvivalCertificate snapshot mean optimal) : snapshot.remainingActive.Nonempty

Under the same optimal-arm survival certificate, the probability vector computed after line 8 and line 15 has total mass exactly one. EAP still has to establish coordinate nonnegativity and the inactive-mass upper bound.

theorem sum_delayedSAPOProbability_after_elimination_eq_one {K : Nat} (snapshot : DelayedSAPOEliminationSnapshot K) (mean : Fin K → ℝ) (optimal : Fin K) (certificate : OptimalArmSurvivalCertificate snapshot mean optimal) (inactiveProbability : Fin K → ℝ) : ∑ i, delayedSAPOProbability snapshot.remainingActive inactiveProbability i = 1