BanditRLProof.TsallisFiniteArmIIDArmDependentSuboptimalBoostRegret

A stationary but arm-dependent corruption process that leaves the best arm unchanged and adds a prescribed nonnegative boost to every other arm.

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

The arm-dependent suboptimal boost has exact deterministic envelope budget `(T+1) * sum_(a != best) boost(a)`.

theorem finiteArmIIDHistoryAdaptiveRewardCorruptionBudget_armDependentSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (boost : Fin K -> Real) (hboost : forall arm, 0 <= boost arm) : finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon (armDependentSuboptimalRewardBoostSource model boost hboost) = (((horizon + 1 : Nat) : Real)) * ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum boost

The coefficient-aware refined regime for an arm-dependent boost budget.

noncomputable def finiteArmIIDArmDependentSuboptimalBoostRefinedRegime {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (boost : Fin K -> Real) : Prop

The named arm-dependent refined regime supplies the existing model-facing compact corruption window after the exact budget rewrite.

theorem finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow_armDependentSuboptimalRewardBoostSource_of_refinedRegime {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (boost : Fin K -> Real) (hboost : forall arm, 0 <= boost arm) (hregime : finiteArmIIDArmDependentSuboptimalBoostRefinedRegime model horizon boost) : finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow model horizon (armDependentSuboptimalRewardBoostSource model boost hboost)

Total regret bound for arm-dependent boosts: the refined local expression inside its named regime and the logarithmic additive-budget expression on the complement.

noncomputable def finiteArmIIDArmDependentSuboptimalBoostAllRegimeBound {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (boost : Fin K -> Real) : Real

Scheduled half-Tsallis regret for every nonnegative arm-dependent suboptimal reward boost and every finite horizon. The result automatically selects the refined or logarithmic branch and requires no caller window proof.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDArmDependentSuboptimalBoostRewardLawRegret_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)) (boost : Fin K -> Real) (hboost : forall arm, 0 <= boost 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)