BanditRLProof.TsallisFiniteArmIIDUniformSuboptimalBoostRefinedRegret

A concrete corruption process that leaves the best arm unchanged and adds the same nonnegative reward boost to every other arm at every round.

noncomputable def uniformSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (epsilon : Real) (hepsilon : 0 <= epsilon) : FiniteArmIIDHistoryAdaptiveRewardShiftSource K where

The uniform suboptimal-arm boost has the exact deterministic envelope budget `(T+1) * (# suboptimal arms) * epsilon`.

theorem finiteArmIIDHistoryAdaptiveRewardCorruptionBudget_uniformSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (epsilon : Real) (hepsilon : 0 <= epsilon) : finiteArmIIDHistoryAdaptiveRewardCorruptionBudget model horizon (uniformSuboptimalRewardBoostSource model epsilon hepsilon) = (((horizon + 1 : Nat) : Real)) * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * epsilon

The explicit scalar regime in which the coefficient-aware refined theorem is used for the uniform suboptimal-arm boost.

noncomputable def finiteArmIIDUniformSuboptimalBoostRefinedRegime {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (epsilon : Real) : Prop

Natural scalar conditions for the uniform suboptimal-arm boost imply the coefficient-aware refined corruption window.

theorem finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow_uniformSuboptimalRewardBoostSource {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (epsilon : Real) (hepsilon : 0 <= epsilon) (hhorizon : 25 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) ^ 2 <= (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) (hepsilonGap : epsilon * ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real)) <= 1) (hcorruptionLower : 25 * ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real)) * (Real.log ((2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) ^ 2)) + 2) <= (((horizon + 1 : Nat) : Real)) * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * epsilon) : finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow model horizon (uniformSuboptimalRewardBoostSource model epsilon hepsilon)

The named uniform-boost refined regime supplies the model-facing compact corruption window without exposing its three clauses separately.

theorem finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow_uniformSuboptimalRewardBoostSource_of_refinedRegime {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (epsilon : Real) (hepsilon : 0 <= epsilon) (hregime : finiteArmIIDUniformSuboptimalBoostRefinedRegime model horizon epsilon) : finiteArmIIDHistoryAdaptiveRefinedCorruptionWindow model horizon (uniformSuboptimalRewardBoostSource model epsilon hepsilon)

A total explicit bound: use the refined square-root branch inside its coefficient-aware window and the logarithmic additive-budget branch everywhere else. In particular, the fallback covers zero and small corruption.

noncomputable def finiteArmIIDUniformSuboptimalBoostAllRegimeBound {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (epsilon : Real) : Real

Refined local regret for the concrete corruption process that uniformly boosts every suboptimal arm by `epsilon` at every round. The corruption budget is exposed explicitly rather than through the abstract source envelope.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDUniformSuboptimalBoostRewardLawRegret_le_refinedLocalExplicit {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)) (epsilon : Real) (hepsilon : 0 <= epsilon) (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) (hhorizon : 25 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) ^ 2 <= (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) (hepsilonGap : epsilon * ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real)) <= 1) (hcorruptionLower : 25 * ((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real)) * (Real.log ((2 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * (((Finset.univ : Finset (Fin K)).erase model.bestArm).sum (fun arm => 1 / ((model.gap arm : Rat) : Real))) ^ 2)) + 2) <= (((horizon + 1 : Nat) : Real)) * (((Finset.univ : Finset (Fin K)).erase model.bestArm).card : Real) * epsilon) : letI : Nonempty (Fin K)

Uniform suboptimal-arm boost regret for every nonnegative `epsilon` and finite horizon. The theorem selects the refined local branch when its named regime holds and otherwise falls back to the compiled logarithmic theorem.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDUniformSuboptimalBoostRewardLawRegret_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)) (epsilon : Real) (hepsilon : 0 <= epsilon) (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)