BanditRLProof.TsallisFiniteArmIIDPreviousActionGatedSuboptimalBoostRegret

A concrete history-adaptive corruption source. At successor time `n+1`, the suboptimal-arm boost is active exactly when the action observed at time `n` equals `triggerArm`. The best arm is never shifted.

noncomputable def previousActionGatedSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (triggerArm : Fin K) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) : FiniteArmIIDHistoryAdaptiveRewardShiftSource K where

The deterministic envelope of the previous-action-gated source has the same exact double finite-sum budget as its ungated time-varying schedule.

theorem finiteArmIIDHistoryAdaptiveRewardCorruptionBudget_previousActionGatedSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (triggerArm : Fin K) (horizon : Nat) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) : finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon (previousActionGatedSuboptimalRewardBoostSource model triggerArm boost hboost) = finiteArmIIDTimeVaryingSuboptimalBoostBudget model horizon boost

The time-varying named regime supplies the compact refined window for the history-adaptive previous-action-gated source.

theorem finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow_previousActionGatedSuboptimalRewardBoostSource_of_refinedRegime {K : Nat} (model : FiniteBanditModel K) (triggerArm : Fin K) (horizon : Nat) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) (hregime : finiteArmIIDTimeVaryingSuboptimalBoostRefinedRegime model horizon boost) : finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow model horizon (previousActionGatedSuboptimalRewardBoostSource model triggerArm boost hboost)

Scheduled half-Tsallis regret for a concrete source whose successor boost depends on the previous sampled action. The theorem covers every finite horizon and internally selects the refined or logarithmic branch.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDPreviousActionGatedSuboptimalBoostRewardLawRegret_le_allRegimes {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (triggerArm : Fin K) (boost : Nat -> Fin K -> Real) (hboost : forall t arm, 0 <= boost t arm) (hsuboptimal : ((Finset.univ : Finset (Fin K)).erase model.bestArm).Nonempty) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (hgapLeOne : forall arm, arm ≠ model.bestArm -> ((model.gap arm : Rat) : Real) <= 1) (horizon : Nat) : letI : Nonempty (Fin K)