BanditRLProof.DelayedFeedback.ActiveAllocation

Arms outside the current active set in Algorithm 5.

def inactiveArms {K : Nat} (active : Finset (Fin K)) : Finset (Fin K)

Algorithm 5 line 15 assigns the residual mass equally to active arms.

noncomputable def activeEqualShare {K : Nat} (active : Finset (Fin K)) (inactiveProbability : Fin K → ℝ) : ℝ

Full probability vector obtained from externally maintained probabilities on eliminated arms and equal residual mass on active arms.

noncomputable def delayedSAPOProbability {K : Nat} (active : Finset (Fin K)) (inactiveProbability : Fin K → ℝ) (i : Fin K) : ℝ

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

theorem delayedSAPOProbability_of_active {K : Nat} (active : Finset (Fin K)) (inactiveProbability : Fin K → ℝ) {i : Fin K} (hi : i ∈ active) : delayedSAPOProbability active inactiveProbability i = activeEqualShare active inactiveProbability

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

theorem delayedSAPOProbability_of_inactive {K : Nat} (active : Finset (Fin K)) (inactiveProbability : Fin K → ℝ) {i : Fin K} (hi : i ∉ active) : delayedSAPOProbability active inactiveProbability i = inactiveProbability i

The residual active-arm share is nonnegative when eliminated-arm mass does not exceed one.

theorem activeEqualShare_nonneg {K : Nat} (active : Finset (Fin K)) (inactiveProbability : Fin K → ℝ) (hmass : (∑ i ∈ inactiveArms active, inactiveProbability i) ≤ 1) : 0 ≤ activeEqualShare active inactiveProbability

Every coordinate of the line-15 allocation is nonnegative under the source-side residual-mass and inactive-coordinate hypotheses.

theorem delayedSAPOProbability_nonneg {K : Nat} (active : Finset (Fin K)) (inactiveProbability : Fin K → ℝ) (hinactive : ∀ i ∈ inactiveArms active, 0 ≤ inactiveProbability i) (hmass : (∑ i ∈ inactiveArms active, inactiveProbability i) ≤ 1) (i : Fin K) : 0 ≤ delayedSAPOProbability active inactiveProbability i

With at least one active arm, the equal-residual allocation has total mass exactly one.

theorem sum_delayedSAPOProbability_eq_one {K : Nat} (active : Finset (Fin K)) (inactiveProbability : Fin K → ℝ) (hactive : active.Nonempty) : ∑ i, delayedSAPOProbability active inactiveProbability i = 1