BanditRLProof.TsallisFiniteArmIIDTimeVaryingSuboptimalBoostRegret

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

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

Exact deterministic corruption mass of a time-varying suboptimal-arm boost through the inclusive horizon.

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

The source envelope budget is exactly the finite time-and-arm boost sum.

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

The coefficient-aware refined regime for a time-varying suboptimal-arm boost budget.

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

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

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

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

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

Scheduled half-Tsallis regret for every deterministic nonnegative time-varying suboptimal reward boost and every finite horizon. The theorem selects the refined or logarithmic branch and requires no caller window proof.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDTimeVaryingSuboptimalBoostRewardLawRegret_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 : 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)